Structures and Tarski's Definition of Truth

Intuition Beginner

The previous unit built a grammar: it said which strings of symbols count as legal terms and legal formulas, but it never said what any of them mean. A formula like "for-all $x$, $x<S(x)$" was just a well-formed string. Whether it is true is not a question the grammar can answer, because the grammar never said what $<$ means, what $S$ does, or even what objects $x$ ranges over. This unit supplies the missing half: meaning.

To give a formula meaning, you first pick a world for it to talk about. A world here is a collection of objects plus a fixed reading of every symbol in the language. Choose the whole numbers as your objects, read $0$ as the number zero, read $S$ as "add one," read $<$ as the usual "less than," and suddenly the string "for-all $x$, $x<S(x)$" makes a definite claim: every whole number is below its successor. In that world the claim is true. Pick a different world and it might be false.

The technical name for such a world is a structure. The technical name for the rule that decides, given a structure, whether a formula comes out true is Tarski's definition of truth. The rule works by walking the formula from the inside out, exactly the way you read an arithmetic expression. Once meaning is pinned down this precisely, you can finally ask the central question of logic: does what is provable match what is true in every world? Syntax was one half; this is the other.

Visual Beginner

A structure is a world: a bag of objects with a meaning attached to each symbol. The diagram shows a small one — the numbers $0,1,2,3,\dots$ with their usual readings — and how a formula gets evaluated against it from the inside out.

   STRUCTURE (a world for the language {0, S, +, <}):

      objects:   0   1   2   3   4   ...
      0  reads as   the object 0
      S  reads as   "add one":   0->1, 1->2, 2->3, ...
      +  reads as   ordinary addition
      <  reads as   ordinary "less than"

   EVALUATING a formula inside out:

      Formula:   ( S(0) < S(S(0)) )      "is 1 < 2 ?"

         step 1   read the names (terms):
                     S(0)      -> 1
                     S(S(0))   -> 2
         step 2   check the relation:
                     is  1 < 2  in this world?   YES
         result:  the formula is TRUE in this world

Read it bottom-up. First the terms (the names) are turned into actual objects of the world: $S(0)$ becomes the object $1$, $S(S(0))$ becomes the object $2$. Only then is the relation $<$ checked against those objects. The formula is true here because $1$ really is less than $2$ in this world.

expression	what the world turns it into	true here?
$S(0)$	the object $1$	(it is a name, not a claim)
$S(0)<S(S(0))$	the claim "$1<2$"	yes
$S(0)<0$	the claim "$1<0$"	no
for-all $x$, $x<S(x)$	"every object is below its successor"	yes

Change the world and the answers change. Truth is always truth in a structure.

Worked example Beginner

We work in one fixed world: the objects are the whole numbers $0,1,2,3,\dots$, with $0$ read as zero, $S$ read as "add one," $+$ read as ordinary addition, and $<$ read as ordinary "less than." The task: decide whether the sentence "for-all $x$, ($x<S(x)$)" is true in this world, and then whether "for-all $x$, ($x+0$) $=x$" is true, working each out by hand.

Step 1. Take the first sentence. The phrase "for-all $x$" tells us to test the inside claim "$x<S(x)$" for every object in the world, one at a time.

Step 2. Try $x=0$. The term $S(0)$ is read as "$0$ add one," which is the object $1$. The claim becomes "$0<1$." In this world $0$ is below $1$, so the claim holds for $x=0$.

Step 3. Try $x=5$. The term $S(5)$ is "$5$ add one," the object $6$. The claim becomes "$5<6$," which holds. Every object behaves the same way: an object is always below its add-one. So no object fails the inside claim.

Step 4. Because the inside claim holds for every object, the "for-all" sentence is true in this world.

Step 5. Now the second sentence "for-all $x$, ($x+0$) $=x$." Test the inside claim. Take $x=4$: the term $4+0$ is read as ordinary addition, giving $4$, and the claim "$4=4$" holds. The same happens for every object, since adding zero changes nothing in this world. So this sentence is also true.

What this tells us: a "for-all" sentence is checked by sweeping over every object of the world and confirming the inside claim each time, and a name like $x+0$ is first turned into an actual object before any relation or equality is checked. The truth of a sentence is decided entirely by the world you chose; the next sections turn this sweeping procedure into a precise recursive rule.

Check your understanding Beginner

Formal definition Intermediate+

Fix a first-order language $\mathcal{L}$ with its constant, function, and relation symbols and arities 42.01.03 pending. A structure (model) $\mathfrak{A}$ for $\mathcal{L}$ consists of a nonempty set $|\mathfrak{A}|=A$, the universe (domain), together with an interpretation: a designated element $c^{\mathfrak{A}}\in A$ for each constant symbol $c$; an $n$-ary operation $f^{\mathfrak{A}}:A^n\to A$ for each $n$-place function symbol $f$; and an $n$-ary relation $P^{\mathfrak{A}}\subseteq A^n$ for each $n$-place relation symbol $P$ ^{[Enderton §2.2]}. When $\mathcal{L}$ has equality, $=$ is interpreted as genuine identity on $A$, never as a chosen relation. Canonical examples: a group is a structure for $\{\cdot ,{}^{-1},e\}$; an ordered field is one for $\{+,\cdot ,<,0,1\}$; the standard model of arithmetic is $\mathfrak{N}=(\mathbb{N};0,S,+,\cdot ,<)$ with the usual readings; a graph is a structure for $\{E\}$ with $E^{\mathfrak{A}}$ a symmetric irreflexive relation.

A variable assignment in $\mathfrak{A}$ is a function $s:V\to A$ from the variables into the universe. The value of a term $\bar{s}(t)=t^{\mathfrak{A}}[s]$ is defined by recursion on terms, the recursion licensed by unique readability 42.01.03 pending: $\bar{s}(x)=s(x)$, $\bar{s}(c)=c^{\mathfrak{A}}$, and $\bar{s}(f{t}_1\cdots t_n)=f^{\mathfrak{A}}(\bar{s}(t_1),\dots ,\bar{s}(t_n))$. This is exactly the unique homomorphism out of the term algebra extending $s$.

Tarski's satisfaction relation $\mathfrak{A}\models \phi [s]$ ("$\mathfrak{A}$ satisfies $\phi$ with assignment $s$") is defined by recursion on $\phi$ ^{[Tarski 1933]}:

$$\begin{array}{rl}\mathfrak{A}\models (P{t}_1\cdots t_n)[s]& ⟺(\bar{s}(t_1),\dots ,\bar{s}(t_n))\in P^{\mathfrak{A}},\\ \mathfrak{A}\models (t_1=t_2)[s]& ⟺\bar{s}(t_1)=\bar{s}(t_2),\\ \mathfrak{A}\models (\neg \phi )[s]& ⟺\mathfrak{A}/\models \phi [s],\\ \mathfrak{A}\models (\phi \to \psi )[s]& ⟺\mathfrak{A}/\models \phi [s]\text{ or }\mathfrak{A}\models \psi [s],\\ \mathfrak{A}\models (\forall x\phi )[s]& ⟺\text{for every }a\in A,\mathfrak{A}\models \phi [s(x|a)],\end{array}$$

where $s(x|a)$ is the assignment agreeing with $s$ except at $x$, where it returns $a$. The existential clause follows from $\exists x\phi :=\neg \forall x\neg \phi$: satisfaction holds iff some $a\in A$ has $\mathfrak{A}\models \phi [s(x|a)]$. A sentence $\sigma$ (no free variables) has $\mathfrak{A}\models \sigma [s]$ independent of $s$, so one writes $\mathfrak{A}\models \sigma$ and calls $\mathfrak{A}$ a model of $\sigma$ ^{[Enderton §2.2]}.

For a set $\Gamma$ of formulas, semantic (logical) consequence $\Gamma \models \phi$ holds iff every structure $\mathfrak{A}$ and assignment $s$ with $\mathfrak{A}\models \gamma [s]$ for all $\gamma \in \Gamma$ also has $\mathfrak{A}\models \phi [s]$. A formula is valid ($\models \phi$) iff satisfied in every structure under every assignment; $\phi$ and $\psi$ are logically equivalent iff $\models \phi \leftrightarrow \psi$. A relation $R\subseteq A^n$ is definable in $\mathfrak{A}$ (with parameters $\bar{b}$) iff $R=\{\bar{a}\in A^n:\mathfrak{A}\models \phi [\bar{a},\bar{b}]\}$ for some formula $\phi$.

Counterexamples to common slips Intermediate+

• "The universe can be empty." By convention the universe of a structure is nonempty. The standard quantifier laws — for instance $\forall x\phi \to \exists x\phi$ — fail over an empty domain, where $\forall x\phi$ is vacuously true and $\exists x\phi$ is false. The nonemptiness convention keeps classical validities intact.

• "$=$ is just another relation symbol the structure may interpret freely." In a language with equality, ${=}^{\mathfrak{A}}$ is forced to be the identity on $A$. A structure interpreting $=$ as a coarser equivalence is not a model in this sense; quotient by the equivalence first.

• "$\Gamma \models \phi$ means $\phi$ is valid." It means $\phi$ holds in every model of $\Gamma$, a restricted class. $\{\forall xPx\}\models Pc$ holds though $Pc$ is satisfied in many structures where it is false. Validity is the case $\Gamma =\varnothing$.

• "Definability is the same as the relation being there." Every structure carries countless relations on its universe; only those carved out by a formula are definable. In $(\mathbb{N};+)$ the ordering $<$ is definable ($x<y$ iff $\exists z(z\ne 0\wedge x+z=y)$), but in a bare set with no symbols no nontrivial relation is definable, since every permutation is an automorphism.

Key theorem with proof Intermediate+

The signature theorem of the semantics layer is the substitution lemma: it reconciles the syntactic operation of substituting a term for a variable — defined in 42.01.03 pending — with the semantic operation of changing the assignment. It is the hinge that makes the quantifier clause cooperate with instantiation, and the precise statement is the reason the substitutability ("free for") side condition was isolated syntactically.

Theorem (Substitution lemma). Let $\mathfrak{A}$ be a structure, $s$ an assignment, $\phi$ a formula, $x$ a variable, and $t$ a term that is substitutable for $x$ in $\phi$. First, for every term $u$, $\overline{s}\left(u_t^x\right)=\overline{s(x|\bar{s}(t))}(u)$. Second, $$ \mathfrak{A} \models \varphi^x_t[s] \quad\Longleftrightarrow\quad \mathfrak{A} \models \varphi\big[s(x,|,\bar s(t))\big]. $$ In particular, for a sentence the value $\bar{s}(t)$ does not depend on $s$ ^{[Enderton §2.2]}.

Proof. The term clause is an induction on $u$ using unique readability 42.01.03 pending. If $u=x$, then $u_t^x=t$ and $\bar{s}(t)=\overline{s(x|\bar{s}(t))}(x)$ since the modified assignment returns $\bar{s}(t)$ at $x$. If $u=y\ne x$ or $u=c$, substitution does nothing and the modified assignment agrees with $s$ on $y$ (resp. on constants), so both sides equal $\bar{s}(u)$. If $u=f{u}_1\cdots u_n$, then $u_t^x=f(u_1{)}_t^x\cdots (u_n{)}_t^x$, and applying $f^{\mathfrak{A}}$ to the inductive hypotheses for the $u_i$ gives the claim.

Now induct on $\phi$. For atomic $\phi =P{u}_1\cdots u_n$: ${\phi }_t^x=P(u_1{)}_t^x\cdots (u_n{)}_t^x$, and by the term clause $\bar{s}((u_i{)}_t^x)=\overline{s(x|\bar{s}(t))}(u_i)$, so the tuple checked against $P^{\mathfrak{A}}$ is identical on both sides; the equality atom is the same with $P^{\mathfrak{A}}$ replaced by identity. The clauses $\neg \psi$ and $(\psi \to \chi )$ follow from the inductive hypothesis, since substitution distributes over connectives and substitutability is inherited by subformulas.

The quantifier clause $\phi =\forall y\psi$ is where substitutability is used. If $y=x$, then $x$ is not free in $\phi$, so ${\phi }_t^x=\phi$, and the modified assignment $s(x|\bar{s}(t))$ agrees with $s$ on every variable free in $\phi$; both sides are equivalent to $\mathfrak{A}\models \phi [s]$. If $y\ne x$, substitutability forces $y\notin \mathrm{FV}(t)$ whenever $x\in \mathrm{FV}(\psi )$, so $\overline{s(y|a)}(t)=\bar{s}(t)$ for every $a$. Then ${\phi }_t^x=\forall y{\psi }_t^x$, and $$ \mathfrak{A} \models (\forall y,\psi^x_t)[s] \Leftrightarrow \forall a,\big(\mathfrak{A} \models \psi^x_t[s(y|a)]\big) \Leftrightarrow \forall a,\big(\mathfrak{A} \models \psi[s(y|a)(x|\bar s(t))]\big), $$ the last step by the inductive hypothesis applied to $\psi$ and assignment $s(y|a)$, using $\overline{s(y|a)}(t)=\bar{s}(t)$. Because $y\ne x$, the two modifications commute: $s(y|a)(x|\bar{s}(t))=s(x|\bar{s}(t))(y|a)$, so the right side is $\mathfrak{A}\models (\forall y\psi )[s(x|\bar{s}(t))]$, as required. $\square$

Corollary (coincidence lemma). If assignments $s,s^{\prime }$ agree on $\mathrm{FV}(\phi )$, then $\mathfrak{A}\models \phi [s]\iff \mathfrak{A}\models \phi [s^{\prime }]$. The proof is the same induction with no substitution; it is what makes truth of a sentence well defined.

Bridge. The substitution lemma is the foundational reason the syntactic substitution of 42.01.03 pending and the semantic assignment-shift describe the same operation, and this is exactly the fact that the soundness of the quantifier-instantiation axiom $\forall x\phi \to {\phi }_t^x$ rests on. It builds toward the deductive calculus 42.01.05 pending, whose quantifier rules are correct precisely when $t$ is substitutable for $x$ in $\phi$, and it appears again in the completeness theorem 42.01.06 pending, where Henkin's witnessing constants are instantiated through exactly this lemma. The argument generalises the term-algebra homomorphism property of 42.01.03 pending from pure syntax to its evaluation in a structure: term evaluation $\bar{s}$ is the unique homomorphism, and the lemma is its compatibility with substitution. The central insight is that substitution on the syntax and reassignment on the semantics are two presentations of one operation, intertwined by $\bar{s}$; putting these together, the substitutability condition that looked like a technicality in the syntax unit is the bridge that lets proof and truth be matched in the completeness theorem.

Exercises Intermediate+

Advanced results Master

The semantics fixed in the Formal definition supports four developments: the coincidence and isomorphism theorems that fix what satisfaction can and cannot see, the algebra of definable sets and its closure under the projection a quantifier induces, the automorphism-invariance of definability with the Galois connection it opens onto, and the elementary-class / reduct apparatus that frames the model theory to come.

Theorem 1 (coincidence and isomorphism). Satisfaction $\mathfrak{A}\models \phi [s]$ depends only on $s\upharpoonright \mathrm{FV}(\phi )$ (coincidence), so a sentence is true or false in $\mathfrak{A}$ outright. If $h:\mathfrak{A}\to \mathfrak{B}$ is an isomorphism then $\mathfrak{A}\models \phi [s]\iff \mathfrak{B}\models \phi [h\circ s]$ for every $\phi$ and $s$; in particular isomorphic structures are elementarily equivalent, $\mathfrak{A}\equiv \mathfrak{B}$ (they satisfy the same sentences) ^{[Hodges Ch. 1]}. The converse fails: $(\mathbb{Q};<)\equiv (\mathbb{R};<)$ as dense linear orders without endpoints, yet they are non-isomorphic, and the Löwenheim-Skolem phenomena make elementary equivalence strictly coarser than isomorphism at every infinite cardinality. Homomorphisms preserve only atomic positive formulas, embeddings preserve quantifier-free formulas, and isomorphisms preserve all first-order formulas; this preservation ladder is the organising fact of the homomorphism theory.

Theorem 2 (the Boolean algebra of definable sets, closed under projection). For fixed $\mathfrak{A}$ and a tuple of parameters, the family ${\mathrm{Def}}_n(\mathfrak{A})$ of definable subsets of $A^n$ is a Boolean subalgebra of the power set: it contains $\varnothing$ and $A^n$, and is closed under union, intersection, and complement, mirroring $\vee ,\wedge ,\neg$ on the defining formulas ^{[Marker Ch. 1]}. Beyond the Boolean operations it is closed under the projection induced by an existential quantifier: if $R\subseteq A^{n+1}$ is definable by $\phi (\bar{x},y)$, then $\{\bar{a}:\exists b(\bar{a},b)\in R\}$ is definable by $\exists y\phi$. Quantifier alternation thus measures the projective complexity of definable sets, and a structure admitting quantifier elimination is one where every definable set is already quantifier-free definable — the property that makes $(\mathbb{R};+,\cdot ,<)$ o-minimal and $(\mathbb{C};+,\cdot )$ strongly minimal, the engines of geometric model theory.

Theorem 3 (automorphism invariance and the Galois connection). Every automorphism $h\in \mathrm{Aut}(\mathfrak{A})$ preserves every $\varnothing$-definable relation, and more generally fixes setwise every relation definable over a parameter set $B$ that $h$ fixes pointwise ^{[Hodges Ch. 1]}. This yields a Galois connection between subgroups of $\mathrm{Aut}(\mathfrak{A})$ and definably closed subsets of $A$: to a parameter set $B$ associate its pointwise stabiliser $\mathrm{Aut}(\mathfrak{A}/B)$, and to a subgroup $G$ associate the set fixed pointwise by $G$. For ${\aleph }_0$-categorical $\mathfrak{A}$ the Ryll-Nardzewski theorem makes the correspondence exact — the $\varnothing$-definable relations are precisely the $\mathrm{Aut}(\mathfrak{A})$-invariant ones — so the model-theoretic automorphism group recovers the definable structure, the precise analogue of the Galois group recovering the intermediate fields. This is the doorway from satisfaction to the model theory of 42.02.01 pending.

Theorem 4 (elementary classes, reducts, expansions). A class $\mathcal{K}$ of $\mathcal{L}$-structures is elementary (axiomatisable) iff it is the class $\mathrm{Mod}(T)$ of all models of some first-order theory $T$; it is basic elementary iff a single sentence suffices ^{[Hodges Ch. 2]}. Elementary classes are closed under isomorphism and ultraproducts, and a class closed under both elementary equivalence and ultraproducts is elementary (a corollary of compactness, co-produced as 42.01.02 pending). A reduct $\mathfrak{A}\upharpoonright {\mathcal{L}}_0$ forgets the interpretations of symbols outside a sublanguage ${\mathcal{L}}_0\subseteq \mathcal{L}$, keeping the universe; an expansion adds interpretations for new symbols. Reducts can strictly lose definable structure — $<$ is definable in $(\mathbb{N};+)$ but a bare $(\mathbb{N})$ defines nothing nontrivial — and the Beth definability and Craig interpolation theorems, products of completeness 42.01.06 pending, govern exactly when an expansion adds no new definable sets.

Synthesis. The substitution lemma is the foundational reason satisfaction and syntactic substitution are one operation, and putting these together it controls all four developments: it is exactly what makes the coincidence lemma and hence sentence-truth well defined, and the isomorphism theorem is its parameter-free shadow read across a structure map — the central insight that satisfaction sees a structure only up to isomorphism, never its identity. The algebra of definable sets generalises the propositional Boolean algebra of 42.01.01 pending from truth values to subsets of $A^n$, and the quantifier-as-projection clause is dual, across $\neg \forall \equiv \exists \neg$, to the universal quantifier as an intersection; this is exactly the syntactic prenex hierarchy of 42.01.03 pending read semantically as projective complexity. Automorphism invariance is the bridge from satisfaction to the Galois-theoretic heart of model theory, where the definable closure and the automorphism group determine each other, and the elementary-class apparatus is the frame in which compactness 42.01.02 pending and the completeness theorem 42.01.06 pending do their work. This is the semantic half of the architecture promised at the Beginner tier: a precise rule for truth in a world, built by recursion on the grammar of 42.01.03 pending, standing ready to be matched against deduction 42.01.05 pending by the completeness theorem 42.01.06 pending.

Full proof set Master

Proposition 1 (the coincidence lemma). If assignments $s,s^{\prime }$ into $\mathfrak{A}$ agree on every variable free in $\phi$, then $\bar{s}(t)=\overline{s^{\prime }}(t)$ for every subterm $t$ whose variables are free in $\phi$, and $\mathfrak{A}\models \phi [s]\iff \mathfrak{A}\models \phi [s^{\prime }]$.

Proof. The term claim is an induction on $t$: variables free in $\phi$ receive equal values by hypothesis, constants are assignment-independent, and the function clause propagates equality through $f^{\mathfrak{A}}$. For formulas, induct on $\phi$. Atomic $P{t}_1\cdots t_n$ and $t_1=t_2$: all variables occurring are free, so the term claim gives equal tuples, hence equal satisfaction. The clauses $\neg \psi$ and $\psi \to \chi$ are immediate, as $\mathrm{FV}(\neg \psi )=\mathrm{FV}(\psi )$ and $\mathrm{FV}(\psi \to \chi )=\mathrm{FV}(\psi )\cup \mathrm{FV}(\chi )$, so $s,s^{\prime }$ still agree on the relevant free variables of each subformula. For $\forall y\psi$: $\mathrm{FV}(\forall y\psi )=\mathrm{FV}(\psi )\setminus \{y\}$, so $s,s^{\prime }$ agree on $\mathrm{FV}(\psi )$ except possibly at $y$; but for each $a\in A$ the modified assignments $s(y|a)$ and $s^{\prime }(y|a)$ agree at $y$ (both give $a$) and on $\mathrm{FV}(\psi )\setminus \{y\}$, hence on all of $\mathrm{FV}(\psi )$, so by the inductive hypothesis $\mathfrak{A}\models \psi [s(y|a)]\iff \mathfrak{A}\models \psi [s^{\prime }(y|a)]$ for every $a$, and the two universal quantifications coincide. $\square$

Proposition 2 (substitution lemma, term and formula parts). For $t$ substitutable for $x$ in $\phi$: $\bar{s}(u_t^x)=\overline{s(x|\bar{s}(t))}(u)$ for every term $u$, and $\mathfrak{A}\models {\phi }_t^x[s]\iff \mathfrak{A}\models \phi [s(x|\bar{s}(t))]$.

Proof. The term part is the induction recorded in the Key theorem: bases $u\in \{x,y,c\}$ check directly, the function step propagates through $f^{\mathfrak{A}}$. For formulas, atomic cases inherit the term part by feeding the equal tuples into $P^{\mathfrak{A}}$ or identity. Connective cases pass through the inductive hypothesis with substitutability inherited by subformulas. The quantifier case $\forall y\psi$ splits on $y=x$ (substitution vacuous, both sides reduce to $\mathfrak{A}\models \phi [s]$ by coincidence) and $y\ne x$, where substitutability supplies $y\notin \mathrm{FV}(t)$ if $x\in \mathrm{FV}(\psi )$, hence $\overline{s(y|a)}(t)=\bar{s}(t)$ for all $a$; the inductive hypothesis applied to $\psi$ under $s(y|a)$ and the commuting of the two distinct modifications $s(y|a)(x|\bar{s}(t))=s(x|\bar{s}(t))(y|a)$ close the case. Substitutability is used at exactly this point, to keep $y$ out of $\mathrm{FV}(t)$ so that the value of $t$ is stable as $a$ varies. $\square$

Proposition 3 (isomorphisms preserve all first-order formulas). If $h:\mathfrak{A}\to \mathfrak{B}$ is an isomorphism, then $h(\bar{s}(t))=\overline{h\circ s}(t)$ for every term $t$, and $\mathfrak{A}\models \phi [s]\iff \mathfrak{B}\models \phi [h\circ s]$ for every formula $\phi$; consequently $\mathfrak{A}\equiv \mathfrak{B}$.

Proof. Term induction: $h(\bar{s}(x))=h(s(x))=\overline{h\circ s}(x)$; $h(c^{\mathfrak{A}})=c^{\mathfrak{B}}=\overline{h\circ s}(c)$; and $h(\bar{s}(f{t}_1\cdots t_n))=h(f^{\mathfrak{A}}(\bar{s}{t}_i))=f^{\mathfrak{B}}(h\bar{s}{t}_i)=f^{\mathfrak{B}}(\overline{h\circ s}{t}_i)=\overline{h\circ s}(f{t}_1\cdots t_n)$, using the homomorphism law for $f$ and the inductive hypothesis. Formula induction: atomic $P{t}_1\cdots t_n$ uses $(\bar{s}{t}_i)\in P^{\mathfrak{A}}\iff (h\bar{s}{t}_i)\in P^{\mathfrak{B}}$ (relation preservation) together with the term identity, and $t_1=t_2$ uses injectivity of $h$ to pass identity across. The clauses for $\neg$ and $\to$ are immediate. For $\forall y\psi$: $\mathfrak{A}\models \forall y\psi [s]$ iff for all $a\in A$, $\mathfrak{A}\models \psi [s(y|a)]$, iff (inductive hypothesis) for all $a$, $\mathfrak{B}\models \psi [(h\circ s)(y|h(a))]$; since $h$ is onto $B$, as $a$ ranges over $A$ the value $h(a)$ ranges over all of $B$, so this is iff for all $b\in B$, $\mathfrak{B}\models \psi [(h\circ s)(y|b)]$, i.e. $\mathfrak{B}\models \forall y\psi [h\circ s]$. A sentence has no free variables, so the assignment is immaterial and $\mathfrak{A}\models \sigma \iff \mathfrak{B}\models \sigma$ for all $\sigma$, giving $\mathfrak{A}\equiv \mathfrak{B}$. $\square$

Proposition 4 (automorphisms preserve definable relations). For every automorphism $h$ of $\mathfrak{A}$ and every relation $R$ definable over a parameter set $B$ fixed pointwise by $h$, $\bar{a}\in R\iff h(\bar{a})\in R$.

Proof. Apply Proposition 3 with $\mathfrak{B}=\mathfrak{A}$, so $h$ is an automorphism and $\mathfrak{A}\models \phi [s]\iff \mathfrak{A}\models \phi [h\circ s]$ for every formula and assignment. Let $R=\{\bar{a}:\mathfrak{A}\models \phi [\bar{a},\bar{b}]\}$ with parameters $\bar{b}$ from $B$. Since $h$ fixes $B$ pointwise, $h\circ (\bar{a},\bar{b})=(h\bar{a},\bar{b})$, so $\bar{a}\in R\iff \mathfrak{A}\models \phi [\bar{a},\bar{b}]\iff \mathfrak{A}\models \phi [h\bar{a},\bar{b}]\iff h\bar{a}\in R$. With $B=\varnothing$ this is invariance of $\varnothing$-definable relations under the full automorphism group, the source of the Galois connection between $\mathrm{Aut}(\mathfrak{A})$ and definable closure. $\square$

Proposition 5 (definable sets form a Boolean algebra closed under projection). The $B$-definable subsets of $A^n$ form a Boolean subalgebra of $\mathcal{P}(A^n)$, and the family of definable subsets of $A^{\bullet }$ is closed under coordinate projection.

Proof. If $R=\{\bar{a}:\mathfrak{A}\models \phi [\bar{a},\bar{b}]\}$ and $S=\{\bar{a}:\mathfrak{A}\models \psi [\bar{a},\bar{b}]\}$ are $B$-definable, then $A^n\setminus R$ is defined by $\neg \phi$, $R\cup S$ by $\phi \vee \psi$, and $R\cap S$ by $\phi \wedge \psi$; $\varnothing$ is defined by $x_1\ne x_1$ and $A^n$ by $x_1=x_1$. So ${\mathrm{Def}}_n^B(\mathfrak{A})$ is a Boolean subalgebra. For projection, let $R\subseteq A^{n+1}$ be defined by $\phi (\bar{x},y)$; its projection $\pi (R)=\{\bar{a}:\exists b(\bar{a},b)\in R\}$ satisfies $\bar{a}\in \pi (R)$ iff some $b$ has $\mathfrak{A}\models \phi [\bar{a},b]$ iff $\mathfrak{A}\models (\exists y\phi )[\bar{a}]$, so $\pi (R)$ is defined by $\exists y\phi$. Iterating, the alternation depth of the prefix bounds the projective complexity, and a structure with quantifier elimination collapses every such set to a quantifier-free-definable one. $\square$

Connections Master

• First-order languages: syntax and unique readability 42.01.03 pending is the grammar this unit interprets. Term evaluation $\bar{s}$ is exactly the unique homomorphism out of the absolutely free term algebra of 42.01.03 pending, the satisfaction relation is defined by the structural recursion that unique readability licenses there, and the substitutability ("free for") condition isolated syntactically in 42.01.03 pending is precisely the hypothesis of the substitution lemma proved here. That unit owns the pure grammar; this unit owns its meaning, the two meeting wherever a formula must be both parsed and evaluated.

• The deductive calculus for first-order logic, co-produced as 42.01.05 pending, is the syntactic counterpart whose quantifier-instantiation axiom $\forall x\phi \to {\phi }_t^x$ is sound exactly by the substitution lemma of this unit: the lemma converts the semantic instantiation at $\bar{s}(t)$ into the syntactic substitution ${\phi }_t^x$, so the calculus's rules preserve truth in every structure. Soundness of 42.01.05 pending is the routine half of the match this unit's semantics sets up.

• The completeness theorem for first-order logic, co-produced as 42.01.06 pending, is the reconciliation this unit is built toward: Gödel's theorem proves $\Gamma ⊢\phi \iff \Gamma \models \phi$, identifying the deductive turnstile of 42.01.05 pending with the semantic consequence $\models$ defined here. Henkin's construction builds a model out of syntax — a structure on equivalence classes of closed terms — whose satisfaction relation is computed by exactly the Tarskian recursion of this unit, and the witnessing constants are instantiated through the substitution lemma.

• The model theory of first-order structures, co-produced as 42.02.01 pending, takes definability, elementary equivalence, automorphisms, reducts, and elementary classes — all introduced semantically here — as its primitive objects. The Galois connection between $\mathrm{Aut}(\mathfrak{A})$ and definable closure previewed in Theorem 3, the projection-closure of definable sets driving quantifier elimination, and the elementary-class apparatus of Theorem 4 are the entry points of that development, which compactness 42.01.02 pending and Löwenheim-Skolem turn into the structure theory of models.

Historical & philosophical context Master

The recursive definition of truth is due to Alfred Tarski, whose Pojęcie prawdy w językach nauk dedukcyjnych (1933, German translation 1935, English The Concept of Truth in Formalized Languages 1956) gave the first rigorous account of the satisfaction relation between an infinite sequence of objects and a formula, with truth for sentences obtained as satisfaction by every sequence ^{[Tarski 1933]}. Tarski formulated the material-adequacy condition (Convention T: an acceptable truth predicate must entail every instance of the schema "$\phi$ is true if and only if $\phi$") and proved that the truth predicate of a sufficiently rich language is not definable within that language — the undefinability theorem, the semantic sibling of Gödel's incompleteness results.

The notion of a structure as a domain with interpreted symbols crystallised in the model-theoretic tradition that runs from Leopold Löwenheim (1915) and Thoralf Skolem (1920) through the explicit semantics of first-order logic. Tarski and Robert Vaught's "Arithmetical extensions of relational systems" (1957) fixed elementary equivalence and elementary substructure, and the textbook satisfaction definition was standardised by Tarski's school and by Abraham Robinson. Definability and the connection between the automorphism group of a structure and its definable sets — the model-theoretic Galois correspondence — were developed by Robinson, by Roland Fraïssé, and systematised in the model theory of Wilfrid Hodges ^{[Hodges Ch. 2]} and the textbook treatment of David Marker ^{[Marker Ch. 1]}, with the ${\aleph }_0$-categorical case sharpened by the Ryll-Nardzewski theorem (Engeler, Ryll-Nardzewski, and Svenonius, independently, around 1959).

Bibliography Master

@book{enderton2001logic,
  author    = {Enderton, Herbert B.},
  title     = {A Mathematical Introduction to Logic},
  edition   = {2},
  publisher = {Harcourt/Academic Press},
  year      = {2001}
}

@incollection{tarski1933truth,
  author    = {Tarski, Alfred},
  title     = {The Concept of Truth in Formalized Languages},
  booktitle = {Logic, Semantics, Metamathematics},
  publisher = {Oxford University Press},
  year      = {1956},
  note      = {Polish original 1933, German translation 1935},
  pages     = {152--278}
}

@book{hodges1993modeltheory,
  author    = {Hodges, Wilfrid},
  title     = {Model Theory},
  series    = {Encyclopedia of Mathematics and its Applications},
  volume    = {42},
  publisher = {Cambridge University Press},
  year      = {1993}
}

@book{marker2002modeltheory,
  author    = {Marker, David},
  title     = {Model Theory: An Introduction},
  series    = {Graduate Texts in Mathematics},
  volume    = {217},
  publisher = {Springer},
  year      = {2002}
}

@article{tarskivaught1957,
  author  = {Tarski, Alfred and Vaught, Robert L.},
  title   = {Arithmetical extensions of relational systems},
  journal = {Compositio Mathematica},
  volume  = {13},
  year    = {1957},
  pages   = {81--102}
}

@article{lowenheim1915,
  author  = {L\"{o}wenheim, Leopold},
  title   = {\"{U}ber M\"{o}glichkeiten im Relativkalk\"{u}l},
  journal = {Mathematische Annalen},
  volume  = {76},
  year    = {1915},
  pages   = {447--470}
}

@article{skolem1920,
  author  = {Skolem, Thoralf},
  title   = {Logisch-kombinatorische Untersuchungen \"{u}ber die Erf\"{u}llbarkeit oder Beweisbarkeit mathematischer S\"{a}tze},
  journal = {Skrifter utgit av Videnskapsselskapet i Kristiania},
  year    = {1920}
}