Theorem (Soundness of Natural Deduction): If $\Gamma \vdash \phi$ in natural deduction, then $\Gamma \models \phi$.

We prove by induction on the structure of the natural deduction derivation that every derivable sequent is semantically valid.

Base Cases (Axioms):

1. Assumption: If $\phi \in \Gamma$, then trivially any model satisfying $\Gamma$ satisfies $\phi$.

Inductive Cases (Inference Rules):

We show that each inference rule preserves semantic validity. Assume all premises are semantically valid; we prove the conclusion is semantically valid.

$\land$-Introduction:

By inductive hypothesis, $\Gamma \models \phi$ and $\Gamma \models \psi$. For any model $\mathcal{M}$ with $\mathcal{M} \models \Gamma$, we have $\mathcal{M} \models \phi$ and $\mathcal{M} \models \psi$, hence $\mathcal{M} \models \phi \land \psi$. Therefore $\Gamma \models \phi \land \psi$.

$\land$-Elimination:

By inductive hypothesis, $\Gamma \models \phi \land \psi$. For any model $\mathcal{M}$ with $\mathcal{M} \models \Gamma$, we have $\mathcal{M} \models \phi \land \psi$, which implies $\mathcal{M} \models \phi$. Therefore $\Gamma \models \phi$.

$\to$-Introduction (Conditional Proof):

By inductive hypothesis, $\Gamma, \phi \models \psi$. We must show $\Gamma \models \phi \to \psi$.

Let $\mathcal{M}$ be any model with $\mathcal{M} \models \Gamma$. We must show $\mathcal{M} \models \phi \to \psi$.

Case 1: If $\mathcal{M} \not\models \phi$, then $\mathcal{M} \models \phi \to \psi$ by definition of implication.

Case 2: If $\mathcal{M} \models \phi$, then $\mathcal{M} \models \Gamma, \phi$. By the inductive hypothesis $\Gamma, \phi \models \psi$, we have $\mathcal{M} \models \psi$. Therefore $\mathcal{M} \models \phi \to \psi$.

In both cases, $\mathcal{M} \models \phi \to \psi$, so $\Gamma \models \phi \to \psi$.

$\to$-Elimination (Modus Ponens):

By inductive hypothesis, $\Gamma \models \phi$ and $\Gamma \models \phi \to \psi$. For any model $\mathcal{M}$ with $\mathcal{M} \models \Gamma$:

• $\mathcal{M} \models \phi$
• $\mathcal{M} \models \phi \to \psi$

By the semantics of implication, $\mathcal{M} \models \psi$. Therefore $\Gamma \models \psi$.

$\forall$-Introduction:

By inductive hypothesis, $\Gamma \models \phi$. We must show $\Gamma \models \forall x \, \phi$.

Let $\mathcal{M}$ be any model with $\mathcal{M} \models \Gamma$, and let $s$ be any variable assignment. Since $x$ is not free in $\Gamma$, the truth of $\Gamma$ in $\mathcal{M}$ is independent of the assignment to $x$.

For any value $a$ in the domain, let $s'$ be the assignment that agrees with $s$ except possibly at $x$, where $s'(x) = a$. We still have $\mathcal{M} \models \Gamma[s']$ (since $x$ not free in $\Gamma$).

By the inductive hypothesis $\Gamma \models \phi$, we have $\mathcal{M} \models \phi[s']$. Since this holds for arbitrary $a$, we have $\mathcal{M} \models \forall x \, \phi[s]$.

$\forall$-Elimination:

By inductive hypothesis, $\Gamma \models \forall x \, \phi$. For any model $\mathcal{M}$ with $\mathcal{M} \models \Gamma$ and assignment $s$:

$\mathcal{M} \models \forall x \, \phi[s]$ means for all values $a$, $\mathcal{M} \models \phi[s[x \mapsto a]]$.

In particular, for $a = t^\mathcal{M}[s]$ (the interpretation of term $t$), we have $\mathcal{M} \models \phi[s[x \mapsto t^\mathcal{M}[s]]]$, which equals $\mathcal{M} \models \phi[x/t][s]$ (by substitution lemma).

Therefore $\Gamma \models \phi[x/t]$.

Cases for $\lor$, $\exists$, $\neg$ follow similar patterns.

Conclusion: Every inference rule preserves semantic validity. By induction on derivation structure, if $\Gamma \vdash \phi$ has a derivation, then $\Gamma \models \phi$. This completes the soundness proof.