Soundness Theorem for Hilbert Proof System for Predicate Logic

From ProofWiki
Jump to navigation Jump to search

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}$:

Every $\mathscr H$-provable consequence is a $\mathrm{PL}$-semantic consequence.


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