[proofplan] We induct on the length of a formal proof. Given a proof $q_1, \ldots, q_n = p$ of $p$ from $S$, we show that every $q_i$ is valid in every $L$-structure $A$ that models $S$. The analysis splits by justification type: axioms are validated by checking each axiom scheme against the semantics of $L$-structures; hypotheses from $S$ are valid by definition of "model of $S$"; Modus Ponens preserves validity because implication in a structure matches the Tarski semantics; and Generalization preserves validity, the key step being a careful use of the Gen side condition (the generalised variable is not free in any hypothesis from $S$ used) to conclude that $(\forall x)\,r$ holds whenever $r$ does. Because $p$ is a sentence, validity in every model of $S$ is exactly $S \models p$. [/proofplan] [step:Set up the induction on proof length] Suppose $S \vdash p$. Fix a formal proof \begin{align*} \pi = q_1, q_2, \ldots, q_n \end{align*} of $p$ from $S$, with $q_n = p$. We prove by induction on $i \in \{1, \ldots, n\}$: **Induction claim.** For every $L$-structure $A$ with $A \models S$ and every variable assignment $s: \mathrm{Var} \to |A|$: \begin{align*} A \models q_i[s]. \end{align*} Here $A \models q_i[s]$ means "$q_i$ is satisfied in $A$ under the assignment $s$", as given by Tarski's inductive definition of satisfaction. The strengthening to arbitrary assignments $s$ (rather than fixing one) is necessary because the induction will encounter open formulas $q_i$ (those with free variables) even though $p$ itself is a sentence. Taking $i = n$ and recalling that $q_n = p$ is a sentence (so $A \models p[s]$ is independent of $s$) will give $A \models p$ for every model $A$ of $S$, i.e.\ $S \models p$. Each $q_i$ is justified by one of: (a) a logical axiom, (b) membership in $S$, (c) Modus Ponens from two earlier lines, or (d) Generalization from one earlier line. We handle each case. [/step] [step:Validate the logical axioms in every $L$-structure] Suppose $q_i$ is a logical axiom. We verify, scheme by scheme, that $q_i$ is valid — i.e.\ $A \models q_i[s]$ for every $L$-structure $A$ and every assignment $s$. **Propositional axioms.** These are formulas like \begin{align*} r \Rightarrow (s \Rightarrow r), \qquad (r \Rightarrow (s \Rightarrow t)) \Rightarrow ((r \Rightarrow s) \Rightarrow (r \Rightarrow t)), \end{align*} and the axioms for negation (e.g.\ $(\neg r \Rightarrow \neg s) \Rightarrow (s \Rightarrow r)$). Each is a tautology of propositional logic: it is true under every truth-assignment to its atomic sub-formulas. Tarski's satisfaction rules define the semantics of $\Rightarrow$ and $\neg$ on a structure $A$ to agree exactly with the propositional truth-functions. Therefore each propositional axiom is satisfied in every $L$-structure under every assignment. **Equality axioms.** The axioms for $=$ include: \begin{align*} x &= x, \\ (x_1 = y_1 \land \cdots \land x_n = y_n) &\Rightarrow f(x_1, \ldots, x_n) = f(y_1, \ldots, y_n) \quad \text{for each $n$-ary function symbol } f, \\ (x_1 = y_1 \land \cdots \land x_n = y_n) &\Rightarrow (R(x_1, \ldots, x_n) \Leftrightarrow R(y_1, \ldots, y_n)) \quad \text{for each relation symbol } R. \end{align*} In any $L$-structure $A$, the symbol $=$ is interpreted as **genuine equality** on the domain $|A|$ (this is built into the definition of an $L$-structure). Therefore: $x = x$ is satisfied because every element is equal to itself; the function-symbol axioms are satisfied because genuine equality is compatible with any function on $|A|$ (applying any function to equal inputs yields equal outputs); and the relation-symbol axioms are satisfied because genuine equality is a congruence for every relation. **Quantifier axioms.** These include schemes such as \begin{align*} (\forall x)\,r(x) &\Rightarrow r(t) \quad \text{for any term } t \text{ free for } x \text{ in } r, \\ (\forall x)(r \Rightarrow s) &\Rightarrow (r \Rightarrow (\forall x)\,s) \quad \text{if } x \text{ is not free in } r. \end{align*} For the first (the substitution axiom), if $A \models (\forall x)\,r(x)[s]$, then $r$ holds in $A$ under every $x$-variant of $s$; in particular under the variant that sends $x$ to the interpretation $t^A[s]$ of the term $t$. By the Substitution Lemma (a standard fact about Tarskian semantics: provided $t$ is free for $x$ in $r$, satisfaction of $r(t)$ under $s$ coincides with satisfaction of $r$ under the $x$-variant of $s$ sending $x$ to $t^A[s]$), we conclude $A \models r(t)[s]$. For the second axiom, suppose $A \models (\forall x)(r \Rightarrow s)[s]$ and $A \models r[s]$. Let $s'$ be any $x$-variant of $s$. Since $x$ is not free in $r$, the satisfaction $A \models r[s']$ is equivalent to $A \models r[s]$, which holds. By the premise, $A \models (r \Rightarrow s)[s']$, so $A \models s[s']$. Since $s'$ was an arbitrary $x$-variant, $A \models (\forall x)\,s[s]$. Each axiom scheme is valid. Hence $A \models q_i[s]$ for every $A$ and $s$, in particular for every model $A$ of $S$. [guided] We check each axiom scheme against the Tarskian definition of satisfaction in an $L$-structure. The fact that these are *axioms* rather than derived theorems means the check must be direct: we cannot appeal to any other provability result. **Propositional axioms.** Schemes like $r \Rightarrow (s \Rightarrow r)$ are tautologies — true under every propositional truth-assignment. In an $L$-structure $A$ with assignment $s$, the formula $r \Rightarrow (s \Rightarrow r)$ is satisfied according to the Tarski clauses for $\Rightarrow$, which compute the truth value exactly as classical propositional logic does. Since the formula is a tautology, it is satisfied regardless of the truth values of its atomic sub-formulas. Hence $A \models q_i[s]$. **Equality axioms.** The key observation is that **$=$ in an $L$-structure is interpreted as genuine identity on the domain $|A|$**, not as an arbitrary equivalence relation. This is a definitional choice of what we mean by "$L$-structure with equality"; it is what makes the equality axioms automatically valid. - $x = x$: for every assignment $s$, $s(x) = s(x)$ in $|A|$, which is trivially true. - Function congruence: if $s(x_1) = s(y_1), \ldots, s(x_n) = s(y_n)$ in $|A|$, then $f^A(s(x_1), \ldots, s(x_n)) = f^A(s(y_1), \ldots, s(y_n))$ by the functional nature of $f^A$. - Relation congruence: if $s(x_1) = s(y_1), \ldots$, then $R^A(s(x_1), \ldots)$ iff $R^A(s(y_1), \ldots)$ by genuine equality being compatible with any relation. **Quantifier axioms.** Two in particular deserve attention. The substitution axiom $(\forall x)\,r(x) \Rightarrow r(t)$ (for $t$ free for $x$ in $r$). Suppose $A \models (\forall x)\,r[s]$. Then by the Tarski clause for $\forall$, $A \models r[s']$ for every $x$-variant $s'$ of $s$ — in particular the $x$-variant sending $x$ to $t^A[s]$ (the interpretation of the term $t$ under $s$). The Substitution Lemma then says that $A \models r(t)[s]$ is equivalent to $A \models r[s']$ for this particular $s'$. Hence $A \models r(t)[s]$. (The side condition "$t$ free for $x$ in $r$" is exactly what is needed for the Substitution Lemma to apply without variable capture.) The commutation axiom $(\forall x)(r \Rightarrow s) \Rightarrow (r \Rightarrow (\forall x)\,s)$, with $x$ not free in $r$. Suppose $A \models (\forall x)(r \Rightarrow s)[s]$ and $A \models r[s]$. For every $x$-variant $s'$ of $s$, the premise gives $A \models (r \Rightarrow s)[s']$. Now **because $x$ is not free in $r$**, satisfaction of $r$ under $s'$ coincides with satisfaction of $r$ under $s$ (changing the value assigned to $x$ doesn't affect satisfaction of a formula in which $x$ doesn't appear free) — so $A \models r[s']$. Combining, $A \models s[s']$. Since $s'$ was arbitrary, $A \models (\forall x)\,s[s]$. Hence $A \models (r \Rightarrow (\forall x)\,s)[s]$. Notice how essential the side condition "$x$ not free in $r$" is: without it we couldn't transfer $A \models r[s]$ to $A \models r[s']$ for variants $s'$. Because every axiom is valid in every $L$-structure, in particular $A \models q_i[s]$ for every $A$ with $A \models S$. [/guided] [/step] [step:Validate hypotheses from $S$] Suppose $q_i \in S$. By assumption $A \models S$, meaning $A \models \varphi$ for every sentence $\varphi \in S$. Since $S$ is a set of **sentences**, $q_i$ has no free variables, so $A \models q_i$ independently of any assignment $s$. Hence $A \models q_i[s]$ for every assignment $s$. [/step] [step:Preserve validity under Modus Ponens] Suppose $q_i$ follows by Modus Ponens from two earlier lines $q_j = r$ and $q_k = r \Rightarrow q_i$, where $j, k < i$. By the inductive hypothesis, for every $L$-structure $A$ with $A \models S$ and every assignment $s$: \begin{align*} A \models r[s] \qquad \text{and} \qquad A \models (r \Rightarrow q_i)[s]. \end{align*} By the Tarski clause for $\Rightarrow$, $A \models (r \Rightarrow q_i)[s]$ means: if $A \models r[s]$ then $A \models q_i[s]$. The first hypothesis triggers the consequent: $A \models q_i[s]$. [guided] Modus Ponens is the syntactic rule "from $r$ and $r \Rightarrow q_i$, infer $q_i$". The semantic counterpart is: if $r$ holds in $A$ under $s$, and $r \Rightarrow q_i$ holds in $A$ under $s$ (meaning: $r[s] \Rightarrow q_i[s]$ as a truth-functional implication), then $q_i$ holds in $A$ under $s$. This is immediate from the Tarski clause defining satisfaction of $\Rightarrow$: $A \models (r \Rightarrow q_i)[s]$ iff $A \not\models r[s]$ or $A \models q_i[s]$. Given $A \models r[s]$, the first disjunct fails, so the second must hold: $A \models q_i[s]$. [/guided] [/step] [step:Preserve validity under Generalization via the free-variable side condition] Suppose $q_i = (\forall x)\,r$ is obtained by Generalization from an earlier line $q_j = r$ ($j < i$). Recall the Gen side condition: the variable $x$ must not be free in any hypothesis from $S$ used in deriving $q_j$ from $S$. Let $H \subseteq S$ denote this set of hypotheses actually used in the sub-proof $q_1, \ldots, q_j$. We claim: for every $L$-structure $A$ with $A \models S$ and every assignment $s$, \begin{align*} A \models (\forall x)\,r[s]. \end{align*} Let $A$ be an arbitrary model of $S$ and let $s$ be an arbitrary assignment. By the Tarski clause for $\forall$, we need to show $A \models r[s']$ for every $x$-variant $s'$ of $s$ (i.e.\ every assignment $s'$ agreeing with $s$ except possibly at $x$). Fix such an $s'$. By the inductive hypothesis applied to $q_j = r$, we have $A \models r[s']$ provided $A \models S$ (which holds). However, this inductive hypothesis is about $A$ modelling $S$, and validity of $q_j$ holds under the assignment $s'$ — the inductive hypothesis is stated uniformly over all assignments, so it applies in particular to $s'$. Hence $A \models r[s']$. Since $s'$ was an arbitrary $x$-variant of $s$, by the Tarski clause for $\forall$ we conclude $A \models (\forall x)\,r[s]$, as required. **Role of the Gen side condition.** The inductive hypothesis — that $q_j = r$ is satisfied in every model of $S$ under every assignment — is valid only because the proof of $r$ used hypotheses $H \subseteq S$ in which $x$ is not free. For hypotheses $\varphi \in H$, the statement "$A \models \varphi[s']$" does not depend on $s'(x)$ (since $x$ is not free in $\varphi$); hence the assumption $A \models \varphi$ (which is $A \models \varphi[s]$ for any $s$) transfers cleanly to any $x$-variant $s'$. If $x$ *were* free in some $\varphi \in H$, the statement "$A \models \varphi[s']$" could fail for some $x$-variant — but it doesn't, because of the Gen side condition. Moreover, since $S$ is a set of **sentences**, $x$ is automatically not free in any member of $S$; the Gen side condition is trivially satisfied for any $\varphi \in S$. This makes the argument especially clean for soundness from a sentence-set $S$. [guided] Generalization is the subtle case because the Tarski clause for $\forall$ quantifies over *all* $x$-variants of the ambient assignment, and we need to transfer "$r$ is satisfied under $s$" to "$r$ is satisfied under every $x$-variant of $s$". **What the Gen side condition buys us.** The Gen rule says: if $S \vdash r$ by a proof using hypotheses $H \subseteq S$ in which $x$ is not free, then $S \vdash (\forall x)\,r$. This side condition is exactly what makes the semantic version work. **The argument.** Let $A$ be an arbitrary model of $S$ and $s$ an arbitrary assignment. We want $A \models (\forall x)\,r[s]$, which by Tarski means $A \models r[s']$ for every $x$-variant $s'$ of $s$. Fix $s'$. By the inductive hypothesis — which states that $q_j$ is satisfied in every model of $S$ under every assignment — we have $A \models r[s']$. Done. **Where does the Gen side condition actually enter?** It enters in the **proof of the inductive hypothesis itself**, not visibly in this step. Specifically, the inductive hypothesis for $q_j = r$ is: "in every model of $S$, $r$ is satisfied under every assignment". For this to be true, the sub-proof producing $r$ must not "illegitimately pin down" the value of $x$. The Gen side condition — "$x$ not free in any hypothesis of $H$ used to derive $r$" — is precisely the syntactic guarantee that ensures the semantic uniformity over all $x$-variants. **Concrete illustration.** If we allowed Gen without the side condition, we could derive $\{P(x)\} \vdash (\forall x)\,P(x)$. Semantically, $\{P(x)\} \models (\forall x)\,P(x)$ is false: take $A = \mathbb{Z}$ with $P$ interpreted as "$x$ is even", and assignment $s(x) = 0$. Then $A \models P(x)[s]$ but $A \not\models (\forall x)\,P(x)$. The Gen side condition blocks this derivation: $x$ is free in the hypothesis $P(x) \in H$, so Gen is not applicable. **The sentence hypothesis saves us.** Because $S$ consists of sentences, no variable is free in any member of $S$. So the Gen side condition is *automatically* satisfied for any hypothesis drawn from $S$. In particular, whenever we attempt Gen on a sub-proof from $S$, it is always legal. This makes the Soundness proof for sentence-set $S$ straightforward at the Gen step — the subtlety is "absorbed" by the sentence hypothesis. **More carefully.** A rigorous proof of the inductive hypothesis at $q_j = r$ proceeds by the induction itself: axioms are valid for all $s'$; hypotheses $\varphi \in H \subseteq S$ are valid for all $s'$ (being sentences, their satisfaction doesn't depend on $s'$); Modus Ponens preserves universality over assignments; and Generalization preserves it by the argument of this step. Hence at every stage of the induction, "validity in every model of $S$ under every assignment" is a stable invariant. This is the precise reason the Soundness theorem holds. [/guided] [/step] [step:Conclude $S \models p$] We have shown by induction that $A \models q_i[s]$ for every $i \in \{1, \ldots, n\}$, every $L$-structure $A$ with $A \models S$, and every assignment $s$. In particular $A \models q_n[s] = A \models p[s]$ for every such $A$ and $s$. Since $p$ is a sentence, $A \models p[s]$ does not depend on $s$, so we write $A \models p$. Hence \begin{align*} A \models S \implies A \models p \qquad \text{for every } L\text{-structure } A, \end{align*} which is the definition of $S \models p$. This completes the proof. [/step]