Tarski's definition — how formulas come alive in structures
When is a formula true in a structure? Tarski's answer is a recipe you can run by hand, and these demos run it in front of you, then turn it into a game.
Pick a structure and a formula, then step through the evaluation tree. Watch the green and red truth values climb from the atomic formulas at the leaves up to the root.
Choose a structure and formula, then step through Tarski's recursive evaluation. Truth values propagate from atomic formulas up through quantifiers.
Alfred Tarski's definition of truth is one of the great achievements of 20th-century logic. It answers a deceptively simple question: what does it mean for a formula to be true in a structure? The notation M ⊧ φ[a] says that structure M satisfies formula φ under assignment a, and this relation is defined by recursion on the complexity of φ.
Atomic formulas are checked directly against the interpretation of relation and function symbols. Negation ¬ flips the truth value, conjunction ∧ and disjunction ∨ combine truth values in the expected way. The universal quantifier ∀x requires truth for every element of the domain, while the existential quantifier ∃x requires at least one witness. A structure that makes a sentence true is called a model of that sentence.
Key insight: Truth in a structure is not a matter of opinion or interpretation -- it is determined mechanically by Tarski's recursion. Each quantifier ∀x or ∃x checks every element or finds one witness, and the truth of the whole formula is built up from these atomic checks.
Pick a sentence and see which of the five structures satisfy it. A green checkmark marks a model; a red X marks a structure where the sentence fails.
Select a sentence and see which structures are its models (green) and which are not (red).
Key insight: A single sentence can carve the universe of structures into two classes: its models (where it is true) and its non-models (where it is false). Model theory studies these classes and the structures that inhabit them.
Press Start Game. Spoiler picks an element in one chain, and you, as Duplicator, answer with an element of the other. Keep the order between your picks matching in every round to win.
Play as Duplicator in a 2-round EF game. Spoiler picks an element in one structure; you pick a matching element in the other. Win by preserving all atomic relations.
The Ehrenfeucht-Fraïssé game gives us a remarkable tool for understanding when two structures are indistinguishable by first-order sentences up to a given quantifier depth. Two structures satisfy the same sentences of quantifier rank k if and only if Duplicator can win the k-round EF game between them.
Key insight: The EF game captures elementary equivalenceat bounded quantifier depth. Two structures satisfy the same sentences of quantifier rank k if and only if Duplicator has a winning strategy in the k-round game. This game-theoretic characterization makes it possible to prove that certain properties cannot be expressed in first-order logic.
Spot a mistake or have an idea?