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?

  • $\begingroup$ Can you use modus nullens? $\endgroup$ – fleablood Sep 15 '16 at 17:44
  • $\begingroup$ @fleablood: No. $\endgroup$ – user170039 Sep 15 '16 at 17:45
  • $\begingroup$ -P -> (-Q->-P) axiom1. (-Q->-P)->(P->Q)axiom 2. -P->(P->Q) mp. And... wait what's that mark in the beginning mean? $\endgroup$ – fleablood Sep 15 '16 at 17:55
  • $\begingroup$ Can we use --P =P? $\endgroup$ – fleablood Sep 15 '16 at 18:04
  • $\begingroup$ (+1 for stating your rules and axioms up front). Do you have the Deduction Theorem available? $\endgroup$ – 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}}$

  • $\begingroup$ 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. $\endgroup$ – 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$$\neg$P)$\to$(P$\to$Q))

We want to get to ($\neg$P$\to$(P$\to$Q)). If we look at Axiom 3, it's consequent matches the consequent of the target formula. So, how do we get rid of ($\neg$Q$\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$$\neg$P)$\to$(P$\to$Q)), Q/$\neg$P * 1

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

:1 * (Axiom 3$\to$2)

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

:Axiom 2 S/$\neg$P, P/($\neg$Q$\to$$\neg$P), Q/(P$\to$Q) * 3

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

:3 * (2$\to$4)

4 (($\neg$P$\to$($\neg$Q$\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$$\neg$P))

:4 * (5$\to$6)

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

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?

  • 1
    $\begingroup$ 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$) $\endgroup$ – Doug Spoonwood Sep 15 '16 at 18:10
  • $\begingroup$ 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$. $\endgroup$ – hmakholm left over Monica Sep 15 '16 at 18:34
  • $\begingroup$ @HenningMakholm I'm not sure I follow. But, is your full proof more than six steps? $\endgroup$ – Doug Spoonwood Sep 15 '16 at 19:51
  • $\begingroup$ I think I now have it in 4 steps. $\endgroup$ – fleablood Sep 15 '16 at 20:39
  • 1
    $\begingroup$ I don't understand (3). How does it follow from Axiom 2? $\endgroup$ – 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.

  • 1
    $\begingroup$ What is Axiom 4? $\endgroup$ – user170039 Sep 15 '16 at 17:45
  • $\begingroup$ 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. $\endgroup$ – fleablood Sep 15 '16 at 18:08
  • $\begingroup$ @user170039 It was meant to be Axiom 3. $\endgroup$ – Luca Bressan Sep 15 '16 at 18:42
  • 2
    $\begingroup$ 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. $\endgroup$ – fleablood Sep 15 '16 at 21:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy