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

Question

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?

Answer 1

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

Answer 2

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

Answer 3

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?

Answer 4

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.