Axioms of propositional logic

Question

The book on which I'm studying logic (Mendelson) uses the following axioms:

$$\begin{array} {rl} \text{A1)} & P \to (Q \to P) \\ \text{A2)} & [P \to (Q \to R)] \to [(P \to Q) \to (P \to R)] \\ \text{A3)} & (\lnot P \to \lnot Q) \to [(\lnot P \to Q) \to P] \\ \end{array}$$

Other sources I’ve seen replace A3) with one of the axioms:

$$\begin{array} {rl} \text{A3’) }& (\lnot P \to \lnot Q) \to (Q \to P) \\ \text{A3’’)}& \lnot \lnot P \to P \end{array}$$

Can someone give a proof of $A3$ in the systems $\{A1,A2,A3’\}$ and $\{A1,A2,A3’’\}$?

Answer 1

$\{A1, A2, A3''\}$ cannot establish $A3$. Just consider when $\lnot$ is interpreted as the identity.

$\{A1, A2, A3'\}$ can establish $A3$ because it is classically complete. But the actual derivation can be long and tedious. For reference Bram's answer to this question: help with some Hilbert style proofs in a propositional logic axiom system.

Answer 2

$\lnot$$\lnot$P gets used only when $\lnot$P abbreviates (P$\rightarrow$$\bot$). Thus, when used, A3'': ($\lnot$$\lnot$P$\rightarrow$P) is not the axiom, but rather (((P$\rightarrow$$\bot$)$\rightarrow$$\bot$)$\rightarrow$P) is the axiom, which is a special case of the tautology (((P$\rightarrow$Q)$\rightarrow$$\bot$)$\rightarrow$P). That is a complete system, but you have to start with (((P$\rightarrow$$\bot$)$\rightarrow$$\bot$)$\rightarrow$P). It doesn't occur in the first system you mentioned, since $\lnot$ is a primitive connective, nor is $\bot$ well-formed for that system.

From the theorem prover Prover9 developed by William McCune at Argonne National Laboratory; if you interpret "P" as $\vdash$, the following corresponds to a condensed detachment proof of A3 (at least if correct, I haven't hand-checked it). Note that a correlate to $\lnot$$\lnot$P in formula 4594 gets proved here also.

% -------- Comments from original proof --------
% Proof 1 at 14.73 (+ 4.26) seconds.
% Length of proof is 46.
% Level of proof is 17.
% Maximum clause weight is 24.
% Given clauses 1864.

1 P((-x -> -y) -> ((-x -> y) -> x)) # label(non_clause) # label(goal).  [goal].
2 -P(x -> y) | -P(x) | P(y).  [assumption].
3 P(x -> (y -> x)).  [assumption].
4 P((x -> (y -> z)) -> ((x -> y) -> (x -> z))).  [assumption].
5 P((-x -> -y) -> (y -> x)).  [assumption].
6 -P((-c1 -> -c2) -> ((-c1 -> c2) -> c1)).  [deny(1)].
7 P(x -> (y -> (z -> y))).  [hyper(2,a,3,a,b,3,a)].
8 P(((x -> (y -> z)) -> (x -> y)) -> ((x -> (y -> z)) -> (x -> z))).  [hyper(2,a,4,a,b,4,a)].
9 P(x -> ((y -> (z -> u)) -> ((y -> z) -> (y -> u)))).  [hyper(2,a,3,a,b,4,a)].
10 P((x -> y) -> (x -> x)).  [hyper(2,a,4,a,b,3,a)].
11 P(((-x -> -y) -> y) -> ((-x -> -y) -> x)).  [hyper(2,a,4,a,b,5,a)].
12 P(x -> ((-y -> -z) -> (z -> y))).  [hyper(2,a,3,a,b,5,a)].
14 P(x -> (y -> (z -> (u -> z)))).  [hyper(2,a,3,a,b,7,a)].
17 P(x -> x).  [hyper(2,a,10,a,b,7,a)].
18 P(((x -> y) -> x) -> ((x -> y) -> y)).  [hyper(2,a,4,a,b,17,a)].
26 P((x -> ((y -> x) -> z)) -> (x -> z)).  [hyper(2,a,8,a,b,7,a)].
44 P((x -> ((y -> (z -> y)) -> u)) -> (x -> u)).  [hyper(2,a,8,a,b,14,a)].
48 P(((x -> (y -> z)) -> (((x -> y) -> (x -> z)) -> u)) -> ((x -> (y -> z)) -> u)).  [hyper(2,a,8,a,b,9,a)].
71 P((x -> (-y -> -z)) -> (x -> (z -> y))).  [hyper(2,a,4,a,b,12,a)].
159 P(-x -> (x -> y)).  [hyper(2,a,26,a,b,12,a)].
160 P((x -> y) -> ((z -> x) -> (z -> y))).  [hyper(2,a,26,a,b,9,a)].
166 P(x -> (-y -> (y -> z))).  [hyper(2,a,3,a,b,159,a)].
197 P(((-x -> (x -> y)) -> z) -> z).  [hyper(2,a,18,a,b,166,a)].
815 P(((x -> y) -> z) -> (y -> z)).  [hyper(2,a,44,a,b,160,a)].
835 P(x -> (((y -> z) -> u) -> (z -> u))).  [hyper(2,a,3,a,b,815,a)].
841 P(x -> ((x -> y) -> y)).  [hyper(2,a,815,a,b,18,a)].
842 P(x -> ((-y -> -x) -> y)).  [hyper(2,a,815,a,b,11,a)].
915 P(((x -> ((x -> y) -> y)) -> z) -> z).  [hyper(2,a,841,a,b,841,a)].
918 P((x -> y) -> (x -> ((y -> z) -> z))).  [hyper(2,a,160,a,b,841,a)].
1299 P((x -> (-y -> -x)) -> (x -> y)).  [hyper(2,a,4,a,b,842,a)].
3180 P((x -> (y -> z)) -> (y -> (x -> z))).  [hyper(2,a,48,a,b,835,a)].
3224 P(x -> ((((x -> y) -> y) -> z) -> z)).  [hyper(2,a,915,a,b,918,a)].
4594 P(--x -> x).  [hyper(2,a,197,a,b,1299,a)].
4644 P(--x -> ((x -> y) -> y)).  [hyper(2,a,918,a,b,4594,a)].
4672 P(x -> --x).  [hyper(2,a,5,a,b,4594,a)].
4728 P((x -> y) -> (x -> --y)).  [hyper(2,a,160,a,b,4672,a)].
19603 P(x -> ((x -> y) -> --y)).  [hyper(2,a,3180,a,b,4728,a)].
19609 P((x -> y) -> (--x -> y)).  [hyper(2,a,3180,a,b,4644,a)].
20528 P(--x -> ((x -> y) -> --y)).  [hyper(2,a,19609,a,b,19603,a)].
23007 P((((x -> y) -> y) -> z) -> (x -> z)).  [hyper(2,a,3180,a,b,3224,a)].
26321 P((x -> y) -> (--x -> --y)).  [hyper(2,a,3180,a,b,20528,a)].
27746 P((x -> y) -> (-y -> -x)).  [hyper(2,a,71,a,b,26321,a)].
27754 P(x -> (-y -> -(x -> y))).  [hyper(2,a,23007,a,b,27746,a)].
28044 P((x -> -y) -> (x -> -(x -> y))).  [hyper(2,a,4,a,b,27754,a)].
28694 P((-x -> -y) -> ((-x -> y) -> x)).  [hyper(2,a,71,a,b,28044,a)].
28695 $F.  [resolve(28694,a,6,a)].