# Proving soundness property of a Hilbert system

Now that I have a better understanding of soundness, I'd like to try this again.

My goal is to prove that the classical Hilbert system has the soundness property:

$$\Gamma \vdash \varphi \implies \Gamma \models \varphi$$

For a set of wffs $$\Gamma$$ and wff $$\varphi$$.

This soundness property being "If $$\varphi$$ is provable from $$\Gamma$$, then $$\varphi$$ is also true under every interpretation where $$\Gamma$$ is satisfied (i.e. when all its propositions are true)."

We can induct on the length of the proof, which we denote as a sequence of wffs $$\varphi_1, \varphi_2, \varphi_3, ..., \varphi_n = \varphi$$.

We start with the case of $$n=1$$, where we only have a one-line proof $$\varphi_1$$. There are two cases:

1. $$\varphi$$ is an axiom of the Hilbert system. We can write out the truth tables and show that for every interpretation, the axiom is true.

Axiom I:

$$\begin{array}{|c|c|ccc|} \hline (A & \to & ( B & \to & A )) \\ \hline F & T & T & F & F \\ F & T & F & T & F \\ T & T & T & T & T \\ T & T & F & T & T \\ \hline \end{array}$$

Axiom II:

$$\begin{array}{|ccccc|c|ccccccc|} \hline ((A & \to & (B & \to & C)) & \to & ((A & \to & B) & \to & (A & \to & C))) \\ \hline F & T & F & T & F & T & F & T & F & T & F & T & F \\ F & T & F & T & T & T & F & T & F & T & F & T & T \\ F & T & T & F & F & T & F & T & T & T & F & T & F \\ F & T & T & T & T & T & F & T & T & T & F & T & T \\ T & T & F & T & F & T & T & F & F & T & T & F & F \\ T & T & F & T & T & T & T & F & F & T & T & T & T \\ T & F & T & F & F & T & T & T & T & F & T & F & F \\ T & T & T & T & T & T & T & T & T & T & T & T & T \\ \hline \end{array}$$

Axiom III:

$$\begin{array}{|ccc|c|ccccc|} \hline ((A & \to & B) & \to & (\neg & B & \to & \neg & A)) \\ \hline F & T & F & T & T & F & T & T & F \\ F & T & T & T & F & T & T & T & F \\ T & F & F & T & T & F & F & F & T \\ T & T & T & T & F & T & T & F & T \\ \hline \end{array}$$

1. $$\varphi$$ is a element of $$\Gamma$$. Since we only care about the situation where $$\Gamma$$ is satisfied, all elements of $$\Gamma$$ will be true.

Moving onto the case of $$n > 1$$, our inductive hypothesis is that $$\Gamma \models \varphi_k$$ holds for all $$1 \leq k < n$$ for all interpretations that satisfy $$\Gamma$$. It is possible that $$\varphi_n$$ is an axiom or an element of $$\Gamma$$, which are cases we've already covered. But since $$n > 1$$, we now look at a new possible case where $$\varphi_n$$ can be the result of modus ponens proven from two earlier wffs $$\varphi_i$$ and $$\varphi_j = \varphi_i \to \varphi_n$$ with indices $$i, j < n$$. By inductive hypothesis we know $$\Gamma \models \varphi_i$$ and $$\Gamma \models \varphi_j$$, i.e. $$\varphi_i$$ and $$\varphi_j$$ are both true in every interpretation where $$\Gamma$$ is satisfied.

Using truth tables:

$$\begin{array}{|c|ccc||c|} \hline \varphi_i & \varphi_i & \to & \varphi_n & \varphi_n\\ \hline F & F & T & F & F \\ F & F & T & T & T \\ T & T & F & F & F \\ T & T & T & T & T \\ \hline \end{array}$$

We see in the last case where $$\varphi_i$$ is true and when $$\varphi_i \to \varphi_n$$ is true, $$\varphi_n$$ is true as well. Thus modus ponens is sound, and we have covered all cases. This closes the inductive step.

Now we can conclude that if $$\varphi$$ is provable from $$\Gamma$$, then $$\varphi$$ is true in all interpretations where $$\Gamma$$ is satisfied.

Have I proven that the Hilbert system has the soundness property?

• Quite perfect... "By inductive hypothesis we know $\varphi_i,\varphi_j$ are both true." NO; we know that they are logical cons of $\Gamma$, i.e. that $\Gamma \vDash \varphi_i$ and $\Gamma \vDash \varphi_j$. – Mauro ALLEGRANZA Sep 25 '18 at 14:19
• Thus, because modus ponens is sound, we conclude that: in every int where all formulas of $\Gamma$ are true, also $\varphi_n$ must be true. – Mauro ALLEGRANZA Sep 25 '18 at 14:21
• Updated with truth tables. – user525966 Sep 25 '18 at 14:25
• @MauroALLEGRANZA Is that not saying the same thing? Or I guess if $\Gamma \models \varphi_i$ then is it incorrect to say $\varphi_i$ is true, period -- or would it have been better to say "true under every satisfiable interpretation of $\Gamma$" – user525966 Sep 25 '18 at 14:26
• Perfect......... – Mauro ALLEGRANZA Sep 25 '18 at 14:40

• I don't follow. Isn't something like $A \to (B \to A)$ already presuming that $A$ and $B$ are wffs? And what do you mean by sound instantiation? That seems like a very different thing. What do you mean by "full form"? What substitution rule? – user525966 Sep 25 '18 at 20:07
• When you substitute AFAIK you use parentheses, so it's like substituting each instance of $A$ with $(A \to (B \to A))$, so you'd get $(A \to (B \to A)) \to (B \to (A \to (B \to A)))$ – user525966 Sep 25 '18 at 20:12