# 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$