1
$\begingroup$

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.

$\endgroup$

2 Answers 2

1
$\begingroup$

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$

$\endgroup$
10
  • $\begingroup$ First paragraph: Are we assuming that any formula $P$, $P \to Q$, etc, are built up from the axioms we just proved were true? If the axioms are true then as long as we keep plugging them into each other (no matter how deep), they'll always be true, so $P, P \to Q \vdash Q$ becomes $\top, \top \to \top \vdash \top$? $\endgroup$
    – user525966
    Sep 10, 2018 at 6:47
  • $\begingroup$ Second paragraph: Is what you're discussing here the "deduction theorem"? I'm not sure what's being described here exactly or what/why we need to prove it? If we've shown the axioms are true and the inference rule always yields true statements, what more are we missing exactly? $\endgroup$
    – user525966
    Sep 10, 2018 at 6:49
  • $\begingroup$ I found this proofwiki.org/wiki/Soundness_Theorem_for_Hilbert_Proof_System which suggests the axioms and modus ponens thing are all we need to show in order to prove soundness? $\endgroup$
    – user525966
    Sep 10, 2018 at 10:04
  • $\begingroup$ @user525966 First paragraph: No, the $P$'s and $Q$'s here can be anything, because they can come form the assumption set $A$. Indeed, the $P$'s and $Q$'s need not be tautologies. But what is true, is that if $P$ and $P \rightarrow Q$ are assumed to be true, then $Q$ has to be true as well, which is easily verified by a truth-table. $\endgroup$
    – Bram28
    Sep 10, 2018 at 15:46
  • $\begingroup$ @user525966 Second paragraph: No, this is not about the deduction theorem, but rather about the fact that you need to show that the last line ($B$) in your derivation $A \vdash B$ is a logical consequence of $A$. This actually requires a proof (and a strong inductive proof on the steps in the derivation is the way to go) ... it's not hard, but without it, it cannot be considered a proof. Indeed, I condiser the proof on that ProofWiki to be incomplete. $\endgroup$
    – Bram28
    Sep 10, 2018 at 15:49
1
$\begingroup$

$$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.

$\endgroup$
2
  • $\begingroup$ So A, B, etc, are these technically formulas (in terms of "data type" to use a software analogy) $\endgroup$
    – user525966
    Sep 10, 2018 at 20:36
  • $\begingroup$ @user525966 Yes, that is a good way of putting it. And $A$ is actually a set of formulas. $\endgroup$
    – DanielV
    Sep 11, 2018 at 1:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .