Soundness Theorem for Hilbert Proof System for Predicate Logic
Theorem
Let $\mathscr H$ be instance 1 of a Hilbert proof system for predicate logic.
Let $\mathrm{PL}$ be the formal semantics of structures for predicate logic.
Then $\mathscr H$ is a strongly sound proof system for $\mathrm{PL}$:
Proof
By Modus Ponendo Ponens for Semantic Consequence in Predicate Logic, the sole rule of inference of $\mathscr H$ preserves $\mathrm{PL}$-semantic consequence.
By definition a $\mathscr H$-provable consequence $\FF \vdash_{\mathscr H} \mathbf A$ means that $\mathbf A$ is a theorem of $\map {\mathscr H} \FF$.
It is to be shown that the semantic consequence $\FF \models_{\mathrm{PL}} \mathbf A$ holds.
Suppose that $\AA$ is a structure for $\mathrm{PL}$ such that $\AA \models_{\mathrm{PL}} \FF$.
- By Axioms of Hilbert Proof System Instance 1 for Predicate Logic are Tautologies, the axioms of $\mathscr H$ are tautologies
- By hypothesis, the extra axioms $\FF$ of $\map {\mathscr H} \FF$ are also valid in $\AA$
Therefore all axioms of $\map {\mathscr H} \FF$ are valid in $\AA$.
Since $\AA$ was arbitrary, it follows that all axioms of $\map {\mathscr H} \FF$ are semantic consequences of $\FF$.
By Modus Ponendo Ponens for Semantic Consequence in Predicate Logic, the sole rule of inference of $\mathscr H$ preserves $\mathrm{PL}$-semantic consequence.
Therefore every theorem of $\map {\mathscr H} \FF$ is a semantic consequences of $\FF$.
Thus, since $\mathbf A$ is a $\map {\mathscr H} \FF$-theorem:
- $\FF \models_{\mathrm{PL}} \mathbf A$
as desired.
$\blacksquare$
Sources
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\text{II}.10$ Formal Proofs: Lemma $\text{II}.10.5$