Prove this propositional tautology using only axioms from Mendelson’s “Introduction to Mathematical Logic”

proof-theorypropositional-calculus

The result I wish to prove is (A -> (B -> C)) -> (B -> (A -> C))

Firstly does this have a name? I've been calling it "Swapping Hypothesis".

Secondly, I'm trying to find a proof of this only using the axioms from the book "Introduction to Mathematical Logic" by Mendelson. He gives three propositional axioms, here are 2 of those axioms

A1 (A -> (B -> A)
A2 ((A -> (B -> C)) -> ((A -> B) -> (A -> C))

The rule of proof is Given A and A -> B then B

The third axiom I do not believe is relevant.

I've already proved a couple of results, which may be of use:

(Theorem) (B -> C) -> ((A -> B) -> (A -> C))
(Rule) Given (A -> B) and (B -> C) then (A -> C) (Hypothetical Syllogism)

If you can do it without Deduction Theorem that would be great, but it's OK with Deduction also (as I think I can translate a proof with Deduction into a proof without fairly easily).

UPDATE Found answer here (T4):

https://math.stackexchange.com/a/1071904/123948

Best Answer

With the Deduction Theorem the proof practically writes itself.

The main heuristic is: Each time you need to prove something of the form $\cdots\to\cdots$, apply the Deduction Theorem. Once that won't get you any further, you'll have assumed $A\to(B\to C)$ and $B$ and $A$, and you need to prove $C$. But that is then just two applications of modus ponens away.

You can then begin to unfold the applications of the DT. Doing it mechanically, inside out, is guaranteed to work but will produce a rather large proof. There are shortcuts you can apply along the way, though -- for example, if a subtree of the inner proof doesn't need the assumption at all, you can just keep it unchanged and apply A1 to it at the point where it connects to something that does need the assumption.

Related Solutions

Logic – How to Prove Hilbert Style Proofs in Propositional Logic

Just as an example of how to use the Deduction Theorem, let me do b)

First, let's show that $X, X \rightarrow Y \vdash Y$:

$X$ Premise
$X \rightarrow Y$ Premise
$Y$ MP 1,2

OK, so we have $X, X \rightarrow Y \vdash Y$

By the Deduction Theorem, we thus have $X \vdash (X \rightarrow Y) \rightarrow Y$

And applying the Deduction Thorem on that, we get $\vdash X \rightarrow ((X \rightarrow Y) \rightarrow Y)$

Now, the others aren't quite so easy, but here are some useful derivations thay may help:

Let's prove: $\phi \to \psi, \psi \to \chi, \phi \vdash \chi$:

$\phi \to \psi$ Premise
$\psi \to \chi$ Premise
$\phi$ Premise
$\psi$ MP 1,3
$\chi$ MP 2,4

By the Deduction Theorem, this gives us Hypothetical Syllogism (HS): $\phi \to \psi, \psi \to \chi \vdash \phi \to \chi$

Now let's prove the general principle that $\neg \phi \vdash (\phi \to \psi)$:

$\neg \phi$ Premise
$\neg \phi \to (\neg \psi \to \neg \phi)$ Axiom1
$\neg \psi \to \neg \phi$ MP 1,2
$(\neg \psi \to \neg \phi) \to (\phi \to \psi)$ Axiom3
$\phi \to \psi$ MP 3,4

With the Deduction Theorem, this means $\vdash \neg \phi \to (\phi \to \psi)$ (Duns Scotus Law)

Let's use Duns Scotus to show that $\neg \phi \to \phi \vdash \phi$

$\neg \phi \to \phi$ Premise
$\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))$ (Duns Scotus Law)
$(\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))) \to ((\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi)))$ Axiom2
$(\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi))$ MP 2,3
$\neg \phi \to \neg (\neg \phi \to \phi)$ MP 1,4
$(\neg \phi \to \neg (\neg \phi \to \phi)) \to ((\neg \phi \to \phi) \to \phi)$ Axiom3
$(\neg \phi \to \phi) \to \phi$ MP 5,6
$\phi$ MP 1,7

By the Deduction Theorem, this means $\vdash (\neg \phi \to \phi) \to \phi$ (Law of Clavius)

Using Duns Scotus and the Law of Clavius, we can now show that $ \neg \neg \phi \vdash \phi$:

$\neg \neg \phi$ Premise
$\neg \neg \phi \to (\neg \phi \to \phi)$ Duns Scotus
$\neg \phi \to \phi$ MP 1,2
$(\neg \phi \to \phi) \to \phi$ Law of Clavius
$\phi$ MP 3,4

By the Deduction Theorem, this also means that $\vdash \neg \neg \phi \to \phi$ (DN Elim)

Now we can prove $\vdash \phi \to \neg \neg \phi$ (DN Intro) as well:

$\neg \neg \neg \phi \to \neg \phi$ (DN Elim)
$(\neg \neg \neg \phi \to \neg \phi) \to (\phi \to \neg \neg \phi)$ Axiom 3
$\phi \to \neg \neg \phi$ MP 1,2

Now we can derive Modus Tollens: $\phi \to \psi, \neg \psi \vdash \neg \phi$:

$\phi \to \psi$ Premise
$\neg \psi$ Premise
$\neg \neg \phi \to \phi$ DN Elim
$\neg \neg \phi \to \psi$ HS 1,3
$\psi \to \neg \neg \psi$ DN Intro
$\neg \neg \phi \to \neg \neg \psi$ HS 4,5
$(\neg \neg \phi \to \neg \neg \psi) \to (\neg \psi \to \neg \phi)$ Axiom3
$\neg \psi \to \neg \phi$ MP 6,7
$\neg \phi$ MP 2,8

By the Deduction Theorem this gives us $\phi \to \psi \vdash \neg \psi \to \neg \phi$ (Contraposition)

And if we apply the Deduction Theorem on Contradiction, we get $\vdash (\phi \to \psi) \to (\neg \psi \to \neg \phi)$.

Finally, we can prove $\phi \to \psi, \neg \phi \to \psi \vdash \psi$:

$\phi \to \psi$ Premise
$\neg \phi \to \psi$ Premise
$\neg \psi \to \neg \phi$ Contraposition 1
$\neg \psi \to \psi$ HS 2,3
$(\neg \psi \to \psi) \to \psi$ Law of Clavius
$\psi$ MP 4,5

Now we can apply the Deduction Theorem twice, and get:

$\vdash (\phi \to \psi) \to ((\neg \phi \to \psi) \to \psi)$

Axiomatic Proof Without Using Deduction Theorem

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

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

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.

Best Answer

Related Solutions

Logic – How to Prove Hilbert Style Proofs in Propositional Logic

Axiomatic Proof Without Using Deduction Theorem

Related Question