# I am defeated by the following propositional logic axiomatic proof:

I'm being asked to show:

 (¬P → P) → P


I'm allowed the following three axioms and Modus Ponens:

 (Ax1) (φ → (ψ → φ))

(Ax2) ((φ → (ψ → θ)) → ((φ → ψ) → (φ → θ)))

(Ax3) ((¬φ → ¬ψ) → (ψ → φ))


No deduction theorem or anything like that. The only thing I can use is what I just proved:

 P → P


At this point in the book, the axioms have only just been introduced, so we have to prove this from scratch or using P → P. Because the question is given so early on, it can't be that hard, but somehow I've gotten completely tangled.

My idea was that the formula to be proved has to come at the end of an instance of A2. In particular, we're going to need:

 ((¬P → P) → (ψ → P))  → (((¬P → P) → ψ) (¬P → P) → P))


But I can't find anything to put in place of ψ that is any more obvious how to prove than this formula itself. I got excited when I realised I could get:

(¬P → P) → (P → P)


using the following reasoning:

1. P → P
2. P → P → ((¬P → P) → (P → P))
3. (¬P → P) → (P → P)


So, if the second antecedent was

(¬P → P) → (P → P)


with (P → P) in place of ψ, then I'd be able to drop the one easily with Modus Ponens once I find a way to drop the initial antecedent. But if ψ is (P → P), then we must have:

 (¬P → P) → ((P → P) → P)


as our first antecedent. I have not been able to find a way to prove this formula so that we can drop it with Modus Ponens, and so I'm stuck. Any ideas?

• Please use MathJax for formatting your questions. Oct 26, 2022 at 18:46