Trying to prove soundness property of propositional logic (Hilbert)

Question

So for starters I want to prove that propositional logic is sound, using a Hilbert system such as Łukasiewicz's.

This system comes with three axioms:

$A \to (B \to A)$

$(A \to (B \to C)) \to ((A \to B) \to (A \to C))$

$(\lnot A \to \lnot B) \to (B \to A)$

And one rule of inference (modus ponens):

$P, (P \to Q) \vdash Q$

To prove soundness I need to show that:

$A \vdash B \implies A \vDash B$

Axiom 1:

$A = \top, B = \top$:

$\top \to (\top \to \top) = \top \to \top = \top$

$A = \top, B = \bot$:

$\top \to (\bot \to \top) = \top \to \top = \top$

$A = \bot, B = \top$:

$\bot \to (\top \to \bot) = \bot \to \bot = \top$

$A = \bot, B = \bot$:

$\bot \to (\bot \to \bot) = \bot \to \top = \top$

And then similar idea for the other two axioms (which I'm not showing here for space purposes since the second axiom has $8$ cases and then the third axiom has $4$ cases again)... but all cases come out $\top$ over all possible inputs of $\top$ and $\bot$ for the propositional variables.

So each axiom is always a true statement, i.e. a tautology (given our definitions/truth tables for $\top$, $\bot$, $\to$, and $\lnot$).

Now I am a little stuck. We still need to show $A \vdash B \implies A \vDash B$, which I believe means we have to somehow show that modus ponens always allows us to derive true deductions, but then somehow using our result that we have true axioms in the form of tautologies.

Answer 1

You're almost there. Yes, you need to show that Modus Ponens is a valid inference scheme, but that is easy: whenever $P$ is true, and $P \rightarrow Q$ is true, then indeed it must be the case that $Q$ is true.

Ok, but how do you show that if $A \rightarrow B$ (I assume $A$ is a set of assumptions?), then $A \Rightarrow B$? Well, since $A \rightarrow B$, there is a sequence of statements, where each statement is either an element of $A$, or an instance of one of the axioms, or the result of the application of Modus Ponens to two earlier statements in the sequence, and where the last statement in the sequence is statement $B$. What you want to do, is to show, by strong induction on the steps in this sequence, that each statement in this sequence is a logical consequence of $A$

Answer 2

$$A \vdash B \implies A \vDash B$$

Make sure you are certain about what this actually means: "For every propositional proof $P$, for every valuation of the propositional variables, when the valuation makes the assumptions of $P$ true, then the valuation also makes the conclusion of $P$ true." Also note that $B$ is not necessarily a propositional variable, it is an expression containing multiple propositional variables, and $A$ is a set of such expressions.

So the normal manner to prove statements of the form "For every proof $A \vdash B$, stuff" is to proceed by inductive construction of proofs. So to construct a proof, you have 1 base case:

• $A \vdash A$

and you have 2 recursive cases:

• The last step of the proof is an instantiation of an axiom schema, and the inductive assumption the soundness of the rest of the proof is irrelevant
• The last step of the proof is an invocation of modus ponens

In this case, we can assume some $A \vdash X$ is sound and $A \vdash X \to B$ is sound. That is , we can assume for every valuation of propositional variables, whenever every $A$ evaluates to true, so does $X$ and $X \to B$.

We have to establish that for every valuation of propositional variables, whenever every $A$ valuates to true, so does $B$. So write down all 4 cases for $X$ true/false and $B$ true/false. Cross out the cases that contradict the inductive assumptions. If what is left is only cases where $B$ is true then you've established the second recursive case.