Soundness

Theorem 1. (Soundness Theorem) Let \(\Gamma\) be a set of formulas, \(\varphi\) be a formula. Then \[\Gamma \vdash \varphi \implies \Gamma \models \varphi\] (Alternative form: If \(\Gamma\) is satisfiable, then \(\Gamma\) is consistent.)

Proof. We show by induction that any formula \(\varphi\) deducible from \(\Gamma\) is logically implied by \(\Gamma\).

1. \(\varphi \in \Lambda\). By the Main Lemma, \(\models \varphi\), so \(\Gamma \models \varphi\).
2. \(\varphi \in \Gamma\). Then trivially \(\Gamma \models \varphi\).
3. \(\varphi\) is obtained by modus ponens from \(\psi\) and \(\psi \to \varphi\). By IH, \(\Gamma \models \psi\), and \(\Gamma \models (\psi \to \varphi)\). Thus, \(\Gamma \models \varphi\).

■

Lemma 2. Any generalization of a valid formula is valid: \(\models \theta \iff \models \forall x \theta\).

Lemma 3. \(\Gamma; \alpha \models \beta \iff \Gamma \models \alpha \to \beta\).

Lemma 4. (Main Lemma) Every logical axiom is valid. (Logical axioms are implied by anything.)

Proof. By Lemma 2 and Lemma 3, we only need to prove the following cases:

(#3) \(\{\forall x (\alpha \to \beta), \forall x \alpha\} \models \forall x \beta\).

(#4) \(\alpha \models \forall x \alpha\), if \(x\) does not occur free in \(\alpha\).

(#5) \(\mathfrak{A}\) satisfies \(x=x\) with \(s\) iff \(s(x) = s(x)\). (Trivial.)

(#1) Any tautology is valid. (If \(\emptyset \models_t \alpha\), then \(\emptyset \models \alpha\).)

(#6) \(\{x = y, \alpha\} \models \alpha'\), where \(\alpha\) is atomic and \(\alpha'\) is obtained from \(\alpha\) by replacing \(x\) in zero or more (but not necessarily all) places by \(y\).

(#2) \(\forall x \varphi \to \varphi^x_t\) is valid, where \(t\) is substitutable for \(x\) in \(\varphi\).

Assume that \(t\) is substitutable for \(x\) in \(\varphi\). Assume that \(\models_\mathfrak{A} \forall x \varphi[s]\). For any \(d\) in \(|\mathfrak{A}|\), \[\models_\mathfrak{A} \varphi[s(x|d)]\] Let \(d = \bar{s}(t)\), \[\models_\mathfrak{A} \varphi[s(x|\bar{s}(t))]\] By the substitution lemma, \[\models_\mathfrak{A} \varphi^x_t[s]\]

■

Lemma 5. \(\bar{s}(u^x_t) = \overline{s(x | \bar{s}(t))}(u)\).

Proof. (By induction on the term \(t\).)

Lemma 6. (Substitution Lemma) If the term \(t\) is substitutable for the variable \(x\) in the wff \(\varphi\), then \[\models_\mathfrak{A} \varphi^x_t[s] \iff \models_\mathfrak{A} \varphi[s(x|\bar{s}(t))]\]

Proof. (By induction on the wff \(\varphi\).)

Corollary 7. If \(\vdash (\varphi \leftrightarrow \psi)\), then \(\varphi\) and \(\psi\) are logically equivalent.

Corollary 8. If \(\varphi'\) is an alphabetic variant of \(\varphi\), then \(\varphi\) and \(\varphi'\) are logically equivalent.