# How to prove this propositional tautology using only axioms from Mendelson's “Introduction to Mathematical Logic”

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

• The 'law of commutation' is one of the names. – Doug Spoonwood May 21 at 13:03
• Have you proved the Deduction Theorem? Then it is very straightforward. – Henning Makholm May 21 at 14:32
• If the third axiom is $(\neg A\to\neg B)\to(B\to A)$ then it does actually have new consequences that can be written using only $\to$ -- such as Pierce's law $((P\to Q)\to P)\to P$. But what you're aiming for here doesn't need it. – Henning Makholm May 21 at 14:35
• Thanks @HenningMakholm I'll update my question. – samthebest May 21 at 14:41

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.

• Yeah, got there in the end (on paper), at least 15 lines, and quite deep nesting. I'll write it up and post it at some point. – samthebest May 21 at 18:05