Tarski's definition — how formulas come alive in structures
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.
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.
Select a first-order formula and a structure, then watch Tarski's recursive definition in action. The evaluation tree shows how truth values propagate upward from atomic formulas through connectives and quantifiers, step by step.
Choose a structure and formula, then step through Tarski's recursive evaluation. Truth values propagate from atomic formulas up through quantifiers.
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.
Given a first-order sentence, check which of several small structures satisfy it. A green checkmark means the structure is a model of the sentence; a red X means it is not. The same sentence can be true in some structures and false in others -- this is the heart of model theory.
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.
Play an EF game between two small structures. The Spoiler picks an element in one structure, and you (the Duplicator) must respond with a "matching" element in the other. After each round, the chosen elements must preserve all atomic relations. If you can always respond successfully, the two structures are indistinguishable by sentences of that quantifier depth.
Play as Duplicator in a 3-round EF game. Spoiler picks an element in one structure; you pick a matching element in the other. Win by preserving all atomic relations.
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.