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:
- $\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}
- $\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?
Not quite. First off, instead of using the abbreviated form for the axioms, you'll need to use the full form which satisfies the definition of a well-formed formula. Why? Because you will inevitably end up referring to either instantiations of those axiom schema, or substitutions of those axiom, and either of those require the use of the full form.
Also, it's not entirely clear if you use axiom schema or axioms and have a rule of substitution for those axioms. If you use axiom schema, then you need to show that any instantiation of the axiom schema is sound. If you use axioms, then you need to show that the use of the rule of (uniform) substitution is sound.