2
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ 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$. $\endgroup$ – Mauro ALLEGRANZA Sep 25 '18 at 14:19
  • 1
    $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA Sep 25 '18 at 14:21
  • $\begingroup$ Updated with truth tables. $\endgroup$ – user525966 Sep 25 '18 at 14:25
  • $\begingroup$ @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$" $\endgroup$ – user525966 Sep 25 '18 at 14:26
  • 1
    $\begingroup$ Perfect......... $\endgroup$ – Mauro ALLEGRANZA Sep 25 '18 at 14:40
-2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – user525966 Sep 25 '18 at 20:07
  • $\begingroup$ @user525966 A→(B→A) is not a wff, presuming that A and B are wffs, no. Were it the case that such were a wff, then we could substitute each instance of A with A→(B→A) yielding A→(B→A)→(B→A→(B→A)), which is not uniquely readable, and thus not well-formed. $\endgroup$ – Doug Spoonwood Sep 25 '18 at 20:10
  • $\begingroup$ 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)))$ $\endgroup$ – user525966 Sep 25 '18 at 20:12
  • 1
    $\begingroup$ I mean I understand but I don't see where it fits into proving the soundness property of the system, I thought these concepts of which you speak are already built into the system by definition. Where in my proof would I need to add more and what exactly? I don't understand what's technically missing $\endgroup$ – user525966 Sep 25 '18 at 21:06
  • 1
    $\begingroup$ "any substitution of any the axioms is sound OR prove that any instance of any of the axiom schema is also sound" What's the difference? Aren't the truth tables I posted proof that the axiom schemas are sound? $\endgroup$ – user525966 Sep 26 '18 at 1:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.