Axiomatic proof of $⊢(a→b)→(¬b→¬a)$ without using the deduction theorem

Question

I'm trying to prove : $⊢(a→b)→(¬b→¬a)$ , or the contrapositive as a wff, using the following 6 axioms, the Hypothetical Syllogism rule, and Modus Ponens.

L1. β→(α→β)
L2. (φ→(α→β))→((φ→α)→(φ→β))
L3. ((¬α)→(¬β))→(β→α)
L4. φ→φ
L5. (¬(¬φ))→φ
L6. φ→(¬(¬φ))

This would be a rather simple proof if I could use deduction or assumptions, but I'm trying to prove axiomatically.

My first thought was to play around with L3, which would give me $((¬¬α)→(¬¬β))→(¬β→¬α)$, and then, I can get to $((¬¬α)→(¬¬β))→(α→β)$ using H.S., but I'm not at all sure this is the right direction.

I know I have all the needed axioms, and am probably skipping over something, and I'd really appreciate a boost in the right direction.

Also, if anyone knows what axiom system uses the 6 above, I'd really appreciate it, I've found a few similar ones (some of Hilbert with Lukasiewicz I think?)

Answer 1

You could let $x = ¬ \alpha$, and $y = ¬\beta$, which then you will get $(¬x \to ¬y)$, then to $(y \to x)$ from $L3$, which you can substitute back out to give you $(¬b \to ¬a)$, and then using H.S. to give you the proof.

This could be entirely wrong, though, and take this with a grain of salt.

Answer 2

With the Deduction Theorem, you can do this:

$1. \alpha \to \beta \ (A.)$

$2. \neg \neg \alpha \ (A.)$

$3. \neg \neg \alpha \to \alpha \ (L5)$

$4. \alpha \ (MP \ 2,3)$

$5. \beta \ (MP 1,4)$

$6. \beta \to \neg \neg \beta \ (L6)$

$7. \neg \neg \beta \ (MP \ 5,6)$

So now we have shown $\alpha \to \beta, \neg \neg \alpha \vdash \neg \neg \beta$

With the Deduction Theorem, this means $\alpha \to \beta \vdash \neg \neg \alpha \to \neg \neg \beta$

Given $L3$, we have $\vdash (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha)$

And so we have $\alpha \to \beta \vdash \neg \beta \to \neg \alpha$

Applying the Deduction Theorem once more, we thus have $\vdash (\alpha \to \beta) \to (\neg \beta \to \neg \alpha)$

Note how this whole proof is a bit of a meta-proof: "Given that we can derive [this] from [that], and [such] from [so], we can also derive [bla] from [bloo]". In fact, anytime we rely on the Deduction Theorem, it becomes a meta-proof.

Now, all of that is perfectly acceptable as a mathematical proof of derivability, but it seems you would like to see this as more of a purely formal proof. That is, rather than a proof that something is derivable, you would like to see an actual formal derivation. How to do that?

Well, here is one way to do this. First, let's take the above meta-proof, and make it into what many people would call a Natural Deduction proof where you can make and discharge assumptions through the use of subproofs. Please note that actual Natural Deduction systems typically use $\to \ Elim$ and $\to \ Intro$ as rules, but I use MP and DT (Deduction Theorem) as justifications instead so you can see the clear connection with the meta-proof I did above:

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$

$\fitch{ 1.}{ \fitch{ 2. \alpha \to \beta}{ \fitch{ 3. \neg \neg \alpha}{ 4. \neg \neg \alpha \to \alpha \qquad (L5)\\ 5. \alpha \qquad (MP \ 3,4)\\ 6. \beta \qquad (MP \ 2,5)\\ 7. \beta \to \neg \neg \beta \qquad (L6)\\ 8. \neg \neg \beta \qquad (MP \ 6,7) } \\ 9. \neg \neg \alpha \to \neg \neg \beta \qquad (DT \ 3-6)\\ 10. (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)\\ 11. \neg \beta \to \neg \alpha \qquad (MP \ 9,10)\\}\\ 12. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad (DT \ 2-9)\\ }$

Next I will show you a systematic way of converting this natural deduction style proof into an axiom system style proof. The basic idea is to 'collapse' and get rid of the subproofs, and we'll do this in an inside-out manner. In fact, we'll do this through a process I call 'conditionalization'. Again, this process is a completely systematic process, and you should be able to to write a bit of computer code to do this.

OK, so the first thing we're going to do is to conditionalize the inner subproof. That is, note how lines 4 through 8 from this inner subproof are all dependent upon the assumption $\neg \neg \alpha$ on line 3. So we are going to take those lines, and make them the consequent of a conditional whose antecedent is that assumption $\neg \neg \alpha$.

In fact, we should conditionalize the assumption on line 3 itself. And since the resulting statement $\neg \neg \alpha \to \neg \neg \alpha$ is no longer an assumption of a subproof (since we're completely getting rid of that subproof), we'll have to show how we can actually infer that statement. Fortunately, we have axiom $L4$ to justify this in 1 step.

(Note: For any system that does not have axiom $L4$, please know that you can also derive this in 5 steps from axioms $L1 $and $L2$. Indeed, most axiom systems have axioms $L1$ and $L2$, and therefore do not have $L4$, as it is not really needed. Same goes for axiom $L5$ and $L6$ for that manner; your book or instructor has added those just for convenience, but in the professional literature there is no axiom system that uses all axioms 1 through 6, as axioms 1 through 3 already forms a comeplte system. And that system is known as the Lukasiewicz system, though some refer to it as the (or 'a' Hilbert system.)

As we conditionalize the statements on lines 4 through 8, the justifications for them are no longer valid. So for those statements too we'll need to show how we can derive them. However, the way they are derived currently will tell us exactly how to derive their conditionalized version, and I'll show how to do that later on. For now, let's change any Modus Ponens (MP) justification into a 'Conditionalized Modus Ponens' (C-MP), and we will justify any line that is a direct instantiation of an axiom with a 'Conditionalized Axiom' justification. So, for example, the conditionalization of line 7, which was originally an instantiation of $L6$, will now be justified using 'Conditionalized $L6$' (C-L6) instead. Below is the result of all this:

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$

$\fitch{ 1.}{ \fitch{ 2. \alpha \to \beta}{ 3. \neg \neg \alpha \to \neg \neg \alpha \qquad (L4)\\ 4. \neg \neg \alpha \to ( \neg \neg \alpha \to \alpha) \qquad (C-L5)\\ 5. \neg \neg \alpha \to \alpha \qquad (C-MP \ 3,4)\\ 6. \neg \neg \alpha \to \beta \qquad (C-MP \ 2,5)\\ 7. \neg \neg \alpha \to (\beta \to \neg \neg \beta) \qquad (C-L6)\\ 8. \neg \neg \alpha \to \neg \neg \beta \qquad (C-MP \ 6,7)\\ 9. \neg \neg \alpha \to \neg \neg \beta \qquad (DT \ 3-8)\\ 10. (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)\\ 11. \neg \beta \to \neg \alpha \qquad MP \ 9,10\\}\\ 12. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad \to Intro \ 2-9\\ }$

Now, a little more general house-keeping before I show how to do things like C-MP and C-L6:

Note how line 9 is a copy of line 8, so we can remove that now. On the other hand, we do want to conditionalize any statements that exist outside (before) the original subproof, but that were references inside the subproof that we are currently collapsing (think about it this way: when inside a subproof we make reference to a statement outside that subproof, we are in effect pulling that statement into the subproof (reiteration is what you would use to explicitly formalize that), and given that the conditionaliziation process is really conditionalizing the whole process that is going on inside a subproof, we need to conditionalize those referred statements as well. In this case: since we use line 2 in a MP on line 6, we'll need conditionalize it, and for that we can use axiom $L1$. So (updating line reference numbers as well):

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$

$\fitch{ 1.}{ \fitch{ 2. \alpha \to \beta}{ 3. (\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta)) \qquad (L1)\\ 4. \neg \neg \alpha \to (\alpha \to \beta) \qquad (MP \ 2,3)\\ 5. \neg \neg \alpha \to \neg \neg \alpha \qquad (L4)\\ 6. \neg \neg \alpha \to ( \neg \neg \alpha \to \alpha) \qquad (C-L5)\\ 7. \neg \neg \alpha \to \alpha \qquad (C-MP \ 5,6)\\ 8. \neg \neg \alpha \to \beta \qquad (C-MP \ 4,7)\\ 9. \neg \neg \alpha \to (\beta \to \neg \neg \beta) \qquad (C-L6)\\ 10. \neg \neg \alpha \to \neg \neg \beta \qquad (C-MP \ 8,9)\\ 11. (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)\\ 12. \neg \beta \to \neg \alpha \qquad (MP \ 10,11)\\}\\ 13. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad (DT \ 2-12)\\ }$

Also, just to avoid some unnecessary work, note that the only reason for lines 5 and 6 was to obtain line 7 ... but line 7 is an immediate application of axiom $L5$. So, we can simplify (if you ever write a program for the conversion process that I am going through here, you can make these kinds of simplifications optional, for they require some intelligence ... but without these simplifications, the conversion process is purely algorithmic):

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$

$\fitch{ 1.}{ \fitch{ 2. \alpha \to \beta}{ 3. (\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta)) \qquad (L1)\\ 4. \neg \neg \alpha \to (\alpha \to \beta) \qquad (MP \ 2,3)\\ 5. \neg \neg \alpha \to \alpha \qquad (L5)\\ 6. \neg \neg \alpha \to \beta \qquad (C-MP \ 4,5)\\ 7. \neg \neg \alpha \to (\beta \to \neg \neg \beta) \qquad (C-L6)\\ 8. \neg \neg \alpha \to \neg \neg \beta \qquad (C-MP \ 6,7)\\ 9. (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)\\ 10. \neg \beta \to \neg \alpha \qquad MP \ 8,9\\}\\ 11. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad \to Intro \ 2-10\\ }$

OK, but how are we going to obtain lines 6, 7, and 8? Well, there are basically two kinds of inferences we are doing: the conditionalized version of Modus Ponens (i.e. C-MP), or the conditionalization of an instance of some axiom (such as C-L6)

Let's first show how to do Conditionalized Modus Ponens, which will always look like this:

$1. \phi \to (\alpha \to \beta)$

$2. \phi \to \alpha$

$3. \phi \to \beta (C-MP \ 1,2)$

Well, the axiom $L2$ is ready made for this! In fact, this is of course not a conincidence, and is the very reason why most axiom systems contain axiom $L2$! OK, so we can just do:

$1. \phi \to (\alpha \to \beta)$

$2. \phi \to \alpha$

$3. (\phi \to (\alpha \to \beta)) \to ((\phi \to \alpha) \to (\phi \to \beta)) (L2)$

$4. (\phi \to \alpha) \to (\phi \to \beta) \qquad (MP \ 1,3)$

$5 \phi \to \beta \qquad (MP \ 2,4)$

Conditionalizing a single statement (such as the instance of an axiom) is even simpler, and for that we use the tailor-made axiom $L1$. For example, if we have statement $\psi$, and we want to conditionalize it with statement $phi$, we can simply do:

$1. \psi$

$2. \psi \to (\phi \to \psi) \qquad (L1)$

$3. \phi \to \psi \quad (MP \ 1,2)$

OK, so applying this process to lines 6,7, and 8, we get:

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$

$\fitch{ 1.}{ \fitch{ 2. \alpha \to \beta}{ 3. (\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta)) \qquad (L1)\\ 4. \neg \neg \alpha \to (\alpha \to \beta) \qquad (MP \ 2,3)\\ 5. \neg \neg \alpha \to \alpha \qquad (L5)\\ 6. (\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)) \qquad (L2)\\ 7. (\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta) \qquad (MP \ 4,6)\\ 8. \neg \neg \alpha \to \beta \qquad (MP \ 5,7)\\ 9. \beta \to \neg \neg \beta \qquad (L6)\\ 10. (\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \qquad (L1)\\ 11. \neg \neg \alpha \to (\beta \to \neg \neg \beta) \qquad (MP \ 9,10)\\ 12. (\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))) \qquad (L2)\\ 13. (\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)) \qquad (MP \ 11,12)\\ 14. \neg \neg \alpha \to \neg \neg \beta \qquad (MP \ 8,13)\\ 15. (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)\\ 16. \neg \beta \to \neg \alpha \qquad (MP \ 14,15)\\}\\ 17. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad (DT \ 2-16)\\ }$

Phew! ... though that was only the first subproof conversion. Now we have to do the next subproof conversion. Since what we'll be doing here is really the same process as what we just did, I'll just show the result (the statements in blue are the conditionalizations of sentences 4 through 16 (as with the previous conversion, conditionalizing sentences 2 and 3 is unnecessary to get to 4):

$\color{blue}{1. (\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta)) \qquad (L1)}$

$2. \neg \neg \alpha \to \alpha \qquad (L5)$

$3. (\neg \neg \alpha \to \alpha) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to \alpha)) \qquad (L1)$

$\color{blue}{4. (\alpha \to \beta) \to (\neg \neg \alpha \to \alpha) \qquad (MP \ 2,3)}$

$5. (\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)) \qquad (L2)$

$6. ((\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta))) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)))) \qquad (L1)$

$\color{blue}{7. (\alpha \to \beta) \to ((\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta))) \qquad (MP \ 5,6)}$

$8. ((\alpha \to \beta) \to ((\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)))) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta)) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)))) \qquad (L2)$

$9. ((\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta))) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta))) \qquad (MP \ 7,8)$

$\color{blue}{10. (\alpha \to \beta) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)) \qquad (MP \ 1,9)}$

$11.((\alpha \to \beta) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta))) \to (((\alpha \to \beta) \to (\neg \neg \alpha \to \alpha)) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to \beta))) \qquad (L2)$

$12. ((\alpha \to \beta) \to (\neg \neg \alpha \to \alpha)) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to \beta)) \qquad (MP \ 10,11)$

$\color{blue}{13. (\alpha \to \beta) \to (\neg \neg \alpha \to \beta) \qquad (MP \ 4,12)}$

$14.\beta \to \neg \neg \beta \qquad (L6)$

$15.(\beta \to \neg \neg \beta) \to ((\alpha \to \beta) \to (\beta \to \neg \neg \beta)) \qquad (L1)$

$\color{blue}{16. (\alpha \to \beta) \to (\beta \to \neg \neg \beta) \qquad (MP \ 14,15)}$

$17.(\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \qquad (L1)$

$18.((\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta))) \to ((\alpha \to \beta) \to ((\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)))) \qquad (L1)$

$\color{blue}{19. (\alpha \to \beta) \to ((\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta))) \qquad (MP \ 17,18)}$

$20.((\alpha \to \beta) \to ((\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)))) \to (((\alpha \to \beta) \to (\beta \to \neg \neg \beta)) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)))) \qquad (L2)$

$21.((\alpha \to \beta) \to (\beta \to \neg \neg \beta)) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta))) \qquad (MP \ 19,20)$

$\color{blue}{22. (\alpha \to \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \qquad (MP \ 16,21)}$

$23.(\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))) \qquad (L2)$

$24.((\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)))) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))))) \qquad (L1)$

$\color{blue}{25. (\alpha \to \beta) \to ((\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)))) \qquad (MP \ 23,24)}$

$26.((\alpha \to \beta) \to ((\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))))) \to (((\alpha \to \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta))) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))))) \qquad (L2)$

$27.((\alpha \to \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta))) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)))) \qquad (MP \ 25,26)$

$\color{blue}{28. (\alpha \to \beta) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))) \qquad MP \ 22,27}$

$29.((\alpha \to \beta) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)))) \to ((\neg \neg \alpha \to \neg \neg \beta) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)) \qquad (L2)$

$30.(\neg \neg \alpha \to \neg \neg \beta) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta) \qquad (MP \ 28,29)$

$\color{blue}{31. (\alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta) \qquad (MP \ 13,30)}$

$32.(\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)$

$33.((\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) ) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha))) \qquad (L1)$

$\color{blue}{34. (\alpha \to \beta) \to ((\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha)) \qquad (MP \ 32, 33)}$

$35. ((\alpha \to \beta) \to ((\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha))) \to (( (\alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)) \to ((\alpha \to \beta) \to (\neg \beta \to \neg \alpha))) \qquad (L2) $

$36. ( (\alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)) \to ((\alpha \to \beta) \to (\neg \beta \to \neg \alpha)) \qquad (MP \ 34,35)$

$\color{blue}{37. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad MP \ 31,36}$

OK! So what have we learned? That doing derivations in this system is not fun!! And that is why we use the Deduction Theorem to do a meta-proof of provability instead. And if you want the actual derivation, you can always systematically re-construct it from the meta-proof.