Quantifier Truth-Value Model Checker (2D)

Quantified Sentence

Quantifier

Predicate P(x)

Domain size |D| 10

Evaluation

∃x [Blue(x)]

TRUE

Satisfying / |D|

0 / 10

P(x) holds for

How it works

This is model-theoretic (truth-conditional) semantics: the standard tool formal semanticists (Montague, Heim & Kratzer) use to define what a sentence means by defining exactly when it is true. A model M = (D, I) is a domain D of individuals plus an interpretation function I assigning each predicate the subset of D it holds of:

[[Red]] = { x in D : x is red }
[[forall x P(x)]] = true  iff  [[P]] = D
[[exists x P(x)]] = true  iff  [[P]] != empty
[[not exists x P(x)]] = true iff  [[P]] = empty

Each object in the scene is an individual in the domain D, with independently-assigned color, shape and size — its full "characteristic function" over every predicate. Choosing a predicate computes [[P]], the extension (the exact subset of D satisfying it) — those objects light up with a glowing ring. Choosing a quantifier then checks that extension against D itself to decide truth, exactly as the formulas above specify — no approximation, the same test runs for any domain size. This 2D version lays every individual out flat on a plane you can pan (drag) and zoom (scroll/pinch) instead of orbiting a 3D scene — the underlying model and truth conditions are identical.

Quantifier — picks which of the three truth conditions above is evaluated.
Predicate P(x) — picks the property whose extension [[P]] is computed over the domain.
Domain size |D| — resizes the model; a universal claim gets harder to keep true as |D| grows.
Randomize domain — redraws every individual's color/shape/size, so [[P]] (and the truth value) changes live.
Drag / scroll — pan and zoom the 2D view; it never affects the model, only how you look at it.

Satisfies P(x) — glowing ring Does not satisfy P(x)

drag to pan · scroll to zoom