[proofplan] We prove the two directions separately. The **forward direction** $(S \vdash p \Rightarrow S \models p)$ is Soundness: every semantic model of the premises respects the finitely many deduction rules and axioms used in a formal proof, so conclusions of a proof are satisfied in every model. The **backward direction** $(S \models p \Rightarrow S \vdash p)$ is the content of the theorem. We argue by contrapositive: assuming $S \not\vdash p$, we show $S \not\models p$ by exhibiting a model of $S$ that refutes $p$. The key tool is the [Model Existence Lemma](/theorems/1486): we prove $S \cup \{\neg p\}$ is consistent (using $S \not\vdash p$ plus the Deduction Theorem and Axiom 3), hence has a model, which is a model of $S$ in which $p$ fails. [/proofplan] [step:Forward direction $S \vdash p \Rightarrow S \models p$ via Soundness] We show that every theorem of $S$ holds in every model of $S$. Let $A$ be a model of $S$, i.e., $A \models q$ for every $q \in S$. A formal proof of $p$ from $S$ is a finite sequence $q_1, q_2, \dots, q_n = p$ where each $q_i$ is either (i) a premise from $S$, (ii) a logical axiom of predicate calculus, or (iii) obtained from preceding $q_j, q_k$ by modus ponens or generalisation. We show by induction on $i$ that $A \models q_i$. **(i) Premises.** If $q_i \in S$, then $A \models q_i$ by hypothesis. **(ii) Logical axioms.** The axioms of predicate calculus (propositional axioms, equality axioms, and quantifier axioms) are tautologies: they hold in every structure, hence $A \models q_i$. **(iii) Inference rules.** - *Modus ponens:* $q_i$ is obtained from $q_j$ and $q_k = (q_j \Rightarrow q_i)$ with $j, k < i$. By the inductive hypothesis, $A \models q_j$ and $A \models q_j \Rightarrow q_i$. By the semantic definition of implication, $A \models q_i$. - *Generalisation:* $q_i = (\forall x)\, r$ is obtained from $r$ when $x$ is a variable not free in any premise of $S$ used so far. Soundness of generalisation — essentially, "what is proved without restriction on $x$ is true for all $x$" — gives $A \models (\forall x)\, r$. In particular, $A \models q_n = p$. Since $A$ was an arbitrary model of $S$, this shows $S \models p$. [/step] [step:Backward direction $S \models p \Rightarrow S \vdash p$ by contrapositive] We prove the contrapositive: if $S \not\vdash p$, then $S \not\models p$. Assume $S \not\vdash p$. [claim:The set $S \cup \{\neg p\}$ is consistent] [proof] Suppose, for contradiction, $S \cup \{\neg p\} \vdash \bot$. By the **Deduction Theorem**, $S \vdash \neg p \Rightarrow \bot$. By definition (or by propositional axiom), $\neg p \Rightarrow \bot$ is precisely $\neg\neg p$. Thus $S \vdash \neg\neg p$. By **Axiom 3 of the predicate calculus** (double negation elimination), $\vdash \neg\neg p \Rightarrow p$, and hence by modus ponens $S \vdash p$ — contradicting the assumption $S \not\vdash p$. Therefore $S \cup \{\neg p\}$ is consistent. [/proof] [/claim] By the [Model Existence Lemma](/theorems/1486), every consistent set of sentences has a model. Applying this to $S \cup \{\neg p\}$, there exists an $L$-structure $A$ with \begin{align*} A &\models q \text{ for every } q \in S, & A &\models \neg p. \end{align*} In particular, $A$ is a model of $S$ with $A \not\models p$. Hence $S \not\models p$, which is the contrapositive of the backward direction. [guided] We argue by contrapositive: to show that $S \models p$ implies $S \vdash p$, we prove that $S \not\vdash p$ implies $S \not\models p$. Exhibiting a model of $S$ in which $p$ fails then completes the argument. **Why contrapositive?** Direct proof of $S \models p \Rightarrow S \vdash p$ would require, starting from a semantic statement ("$p$ holds in every model"), constructing a syntactic object (a formal proof). There is no direct way to manufacture a proof from models. The contrapositive flips the direction: from a **lack** of proof, build a **counterexample model**. And we already have a machine for building models — the Model Existence Lemma. **Step A: Consistency of $S \cup \{\neg p\}$.** Assume $S \not\vdash p$. We claim $S \cup \{\neg p\}$ is consistent. Suppose not: $S \cup \{\neg p\} \vdash \bot$. The **Deduction Theorem** — which states $T \cup \{r\} \vdash s$ if and only if $T \vdash r \Rightarrow s$ — gives \begin{align*} S \vdash \neg p \Rightarrow \bot. \end{align*} The sentence $\neg p \Rightarrow \bot$ is, by definition of negation in predicate calculus, exactly $\neg\neg p$. So $S \vdash \neg\neg p$. Now apply **Axiom 3 of the predicate calculus** (double negation elimination): $\vdash \neg\neg p \Rightarrow p$. Modus ponens gives $S \vdash p$. This contradicts our standing assumption $S \not\vdash p$. Therefore $S \cup \{\neg p\}$ must be consistent. **Step B: A model of $S \cup \{\neg p\}$ exists.** The [Model Existence Lemma](/theorems/1486) guarantees: every consistent set of sentences has a model. Since $S \cup \{\neg p\}$ is consistent, there is an $L$-structure $A$ with \begin{align*} A &\models q \text{ for every } q \in S, & A &\models \neg p, \end{align*} that is, $A$ is a model of $S$ in which $p$ fails. **Step C: Conclude.** The existence of $A$ refutes $S \models p$: not every model of $S$ satisfies $p$, since $A$ itself does not. Hence $S \not\models p$, which is the desired contrapositive conclusion. **Summary of dependencies.** The backward direction relies on three tools: (i) the Deduction Theorem (syntactic), (ii) Axiom 3 of the predicate calculus / classical logic (syntactic), and (iii) the Model Existence Lemma (the deep theorem). Constructive logics lacking Axiom 3 would still satisfy Soundness but not Completeness in this form. [/guided] [/step] [step:Combine the two directions] The forward direction (Step 1) gives $S \vdash p \Rightarrow S \models p$, and the backward direction (Step 2) gives $S \models p \Rightarrow S \vdash p$. Together, \begin{align*} S \vdash p &\iff S \models p. \end{align*} This completes the proof of Gödel's Completeness Theorem. [/step]