How to prove $\vdash\neg P\to (P\to Q)$?

I am trying to prove,

$$\vdash\neg P\to (P\to Q)$$

where $$P$$ and $$Q$$ are arbitrary but otherwise fixed formulas.

The only axioms and rule of inference that I can use are,

$$\color{crimson}{\text{Axiom 1.}}\ P\to (Q\to P)$$

$$\color{crimson}{\text{Axiom 2.}}\ (S\to (P\to Q))\to((S\to P)\to (S\to Q))$$

$$\color{crimson}{\text{Axiom 3.}}\ (\neg Q\to\neg P)\to(P\to Q)$$

$$\color{crimson}{\text{Rule of Inference.}}$$ Modus Ponens.

I know that in Angelo Margaris's book First Order Mathematical Logic there is a proof (page 53) but as I have mentioned here, the dot notation seems very confusing and translating them to the nested parentheses notation seems very difficult to me. So, I am trying on my own to prove the result.

Can anyone help?

• Can you use modus nullens? – fleablood Sep 15 '16 at 17:44
• @fleablood: No. – user170039 Sep 15 '16 at 17:45
• -P -> (-Q->-P) axiom1. (-Q->-P)->(P->Q)axiom 2. -P->(P->Q) mp. And... wait what's that mark in the beginning mean? – fleablood Sep 15 '16 at 17:55
• Can we use --P =P? – fleablood Sep 15 '16 at 18:04
• (+1 for stating your rules and axioms up front). Do you have the Deduction Theorem available? – hmakholm left over Monica Sep 15 '16 at 18:26

Abbreviate $$a = \lnot P$$, $$b = \lnot Q \to \lnot P$$, and $$c = P \to Q$$. Then

$$\color{crimson}{\text{1.}}\ a\to b \color{crimson}{\ \ \ \text{by axiom 1}}$$

$$\color{crimson}{\text{2.}}\ b\to c \color{crimson}{\ \ \ \text{by axiom 3}}$$

and we need to deduce $$a \to c$$. The thing that ultimately is going to produce this is

$$\color{crimson}{\text{3.}}\ (a \to (b \to c)) \to ((a \to b) \to (a \to c)) \color{crimson}{\ \ \ \text{by axiom 2}}$$

Note that we're already very close: we just need to deduce $$a \to (b \to c)$$ from $$b \to c$$ and apply modus ponens twice. So

$$\color{crimson}{\text{4.}}\ (b\to c) \to (a \to (b \to c)) \color{crimson}{\ \ \ \text{by axiom 1}}$$

$$\color{crimson}{\text{5.}}\ a \to (b \to c) \color{crimson}{\ \ \ \text{by modus ponens on 2 and 4}}$$

And, as promised, we finish by applying modus ponens twice.

$$\color{crimson}{\text{6.}}\ (a \to b) \to (a \to c) \color{crimson}{\ \ \ \text{by modus ponens on 3 and 5}}$$

$$\color{crimson}{\text{7.}}\ a \to c \color{crimson}{\ \ \ \text{by modus ponens on 1 and 6}}$$

• Wait... at first glance it looked like you encoded a proof of {(A$\to$B), (B$\to$C)} $\vdash$ (A$\to$C) in this proof. Except, we'd have to interpret 1. and 2. as assumptions. Then again, I feel proving that rule a bit unnecessary for this system, since ((A$\to$B)$\to$((C$\to$A)$\to$(C$\to$B))) is 3 condensed detachments away from the axioms, or only a few more steps if we use substitution and detachment. – Doug Spoonwood Sep 15 '16 at 23:17

First off, let's recast those schema as well-formed formulas. This makes substitutions mechanical and less error-prone. Or more easily corrected when errors occur.

Axiom 1 (P$\to$(Q$\to$P))

Axiom 2 ((S$\to$(P$\to$Q))$\to$((S$\to$P)$\to$(S$\to$Q)))

Axiom 3 (($\neg$Q$\to$$\negP)\to(P\toQ)) We want to get to (\negP\to(P\toQ)). If we look at Axiom 3, it's consequent matches the consequent of the target formula. So, how do we get rid of (\negQ\to$$\lnot$P) and put $\lnot$P in front of (P$\to$Q)? Or can we do one of those two?

Well, were it the case that (P$\to$Q) was a theorem, then Axiom 1 would allow us to put any formula, such as $\neg$P, in front of (P$\to$Q). Axiom 1 can also get used to infer any consequent of some formula $\omega$ if the antecedent of $\omega$ can get derived from Axiom 1 by substitution. Axiom 2 "tells" us that if we have some S in front of a conditional $\chi$, we can transfer S to the front of the antecedent of $\chi$ and the front of the consequent of $\chi$. I use $\alpha$/$\beta$ to indicate that $\alpha$ gets substituted with $\beta$. When I write $\alpha$ * $\beta$, both $\alpha$ and $\beta$ indicate equiform formulas. Thus, putting that all together...

:Axiom 1 P/(($\neg$Q$\to$$\negP)\to(P\toQ)), Q/\negP * 1 1 (((\negQ\to$$\neg$P)$\to$(P$\to$Q))$\to$($\neg$P$\to$(($\neg$Q$\to$$\negP)\to(P\toQ)))) :1 * (Axiom 3\to2) 2 (\negP\to((\negQ\to$$\neg$P)$\to$(P$\to$Q)))

:Axiom 2 S/$\neg$P, P/($\neg$Q$\to$$\negP), Q/(P\toQ) * 3 3 ((\negP\to((\negQ\to$$\neg$P)$\to$(P$\to$Q)))$\to$(($\neg$P$\to$($\neg$Q$\to$$\negP))\to(\negP\to(P\toQ)))) :3 * (2\to4) 4 ((\negP\to(\negQ\to$$\neg$P))$\to$($\neg$P$\to$(P$\to$Q)))

:Axiom 1 P/$\neg$P, Q/$\neg$Q * 5

5 ($\neg$P$\to$($\neg$Q$\to$$\negP)) :4 * (5\to6) 6 (\negP\to(P\toQ)) The above is a bit of false history if read as indicating how I found this proof, but perhaps it also offers a bit more metalogical insight. 1) \lnot P \rightarrow (\lnot Q\rightarrow \lnot P) Axiom 1 2) (\lnot Q \rightarrow \lnot P)\rightarrow (P\rightarrow Q) Axiom 3. 3) [(\lnot Q \rightarrow \lnot P)\rightarrow (P\rightarrow Q)] \rightarrow \{[\lnot P \rightarrow (\lnot P\rightarrow \lnot Q)]\rightarrow [\lnot P \rightarrow(P\rightarrow Q)]\} Axiom 2. 4) [\lnot P \rightarrow (\lnot P\rightarrow \lnot Q)]\rightarrow [\lnot P \rightarrow(P\rightarrow Q)] Modus ponens. 2 and 3 combined. 5) \lnot P \rightarrow(P\rightarrow Q) Modus ponens 1 and 4 combined. ==== I originally mistated modus ponens. Which is A; (A \rightarrow B); \implies B whereas what I used was (A \rightarrow B);(B\rightarrow C)\implies (A \rightarrow C) which is similar but different. We can prove that I think: B \rightarrow C given so by axiom 2 (A \rightarrow B)\rightarrow (A \rightarrow C) (A \rightarrow B) given So A \rightarrow C: modus ponens. === As long as we are proving things I might as well prove modus nolens. A \rightarrow B; \lnot B. The (A \rightarrow B) \rightarrow (\lnot B \rightarrow \lnot A) Axiom 3 So \lnot B \rightarrow \lnot A modus ponens. So \lnot A. Modus ponens. Hence modus nolens is valid. Hey, this proving stuff is neat! But I am assuming it is given \lnot \lnot P = P. Is that a given? If not we must prove it before anything. What are we given as basic tautologies? Do we know P\rightarrow P, P \lor \lnot P etc? • Modus Ponens says that from \vdash(\alpha$$\to$$\beta) as well as \vdash$$\alpha$ we may infer $\vdash$$\beta. I believe you used from \vdash(\alpha$$\to$$\beta) as well as \vdash(\beta$$\to$$\gamma) we may infer \vdash(\alpha$$\to$$\gamma$) – Doug Spoonwood Sep 15 '16 at 18:10
• However, once you have $\alpha\to\beta$ and $\beta\to\gamma$, you can infer $\alpha\to(\beta\to\gamma)$ by A1 and MP, and then a suitable instance of A2 (and two more MP) allows you to reason from $\alpha\to(\beta\to\gamma)$ and $\alpha\to\beta$ to $\alpha\to\gamma$. – hmakholm left over Monica Sep 15 '16 at 18:34
• @HenningMakholm I'm not sure I follow. But, is your full proof more than six steps? – Doug Spoonwood Sep 15 '16 at 19:51
• I think I now have it in 4 steps. – fleablood Sep 15 '16 at 20:39
• I don't understand (3). How does it follow from Axiom 2? – user170039 Sep 16 '16 at 1:54

Hint: Use Axiom 1 in the form $\neg P \to (\neg Q \to \neg P)$ and Axiom 3.

• What is Axiom 4? – user170039 Sep 15 '16 at 17:45
• Dang. This is a weird phone app. I read the post and the app gave me no indication that someone had posted an answer 15 minutes earlier. I'm sorry I answered basically the same thing you did 19 minutes later. – fleablood Sep 15 '16 at 18:08
• @user170039 It was meant to be Axiom 3. – Luca Bressan Sep 15 '16 at 18:42
• It's slightly more involved than that. -P => (-Q=>-P) and (-Q => -P) => (P => Q) but we don't have a rule of inference that A=>B and B=>C means that A=>C. We have to prove that or incorporate a few more steps. – fleablood Sep 15 '16 at 21:05