Quantifier Truth-Value Model Checker

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 ∈ D : x is red }
⟦∀x P(x)⟧ = true  iff  ⟦P⟧ = D
⟦∃x P(x)⟧ = true  iff  ⟦P⟧ ≠ ∅
⟦¬∃x P(x)⟧ = true iff  ⟦P⟧ = ∅

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.

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.

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

⚠ Couldn't load the 3D engineThree.js failed to load from the CDN. Check your connection and reload.