Soundness Theorem for Hilbert Proof System

Theorem

Let $\mathscr H$ be instance 1 of a Hilbert proof system.

Let $\mathrm{BI}$ be the formal semantics of boolean interpretations.

Then $\mathscr H$ is a sound proof system for $\mathrm{BI}$:

Every $\mathscr H$-theorem is a tautology.

Proof

Recall the axioms of $\mathscr H$:

			Axiom $1$:		\(\ds \mathbf A \implies \paren {\mathbf B \implies \mathbf A} \)
			Axiom $2$:		\(\ds \paren {\mathbf A \implies \paren {\mathbf B \implies \mathbf C} } \implies \paren {\paren {\mathbf A \implies \mathbf B} \implies \paren {\mathbf A \implies \mathbf C} } \)
			Axiom $3$:		\(\ds \paren {\neg \mathbf B \implies \neg \mathbf A} \implies \paren {\mathbf A \implies \mathbf B} \)

That these are tautologies is shown on, respectively:

True Statement is implied by Every Statement

Self-Distributive Law for Conditional

Work In Progress In particular: See Talk:Self-Distributive Law for Conditional for Lord_Farin's take on this You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{WIP}} from the code.

Rule of Transposition

That Modus Ponens infers tautologies from tautologies is shown on:

Modus Ponendo Ponens

Since:

All axioms of $\mathscr H$ are tautologies;

All rules of inference of $\mathscr H$ preserve tautologies

it is guaranteed that every formal proof in $\mathscr H$ results in a tautology.

That is, all $\mathscr H$-theorems are tautologies.

$\blacksquare$

Sources

• 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.): $\S 3.6$: Theorem $3.37$