Derive $P \to \neg \neg P$ in a structure with not and implies

We can define an abstract system with the following three axiom schemes that define $\to$ and $\lnot$ as follows:

ax1. $P\to(Q\to P)$

ax2. $(\lnot Q \to \lnot P)\to(P\to Q)$

ax3. $(P\to(Q\to R))\to((P\to Q)\to(P\to R))$

And any logical expressions may be substituted for $P, Q, R$. Now obviously, you can't assume anything else (not even any definition of $\lnot$, etc.) these two objects $\to$ and $\lnot$ need not have anything at all to do with the standard implication and negation we know of, they just happen to satisfy the above properties. But with the above, we can prove basic "logical laws" like:

$$P\to P$$

(which we can prove by applying ax3 on ax1, showing that $(P\to Q)\to(P\to P)$, so we just need to construct a $Q$ for any $P$ to imply, and such a $Q$ is provided by ax1, $Q:= (R\to P)$.)

Is it possible to prove this? :--

$$P\to \lnot\lnot P$$

The person who gave me this problem insists it is provable, although it seems to me that such a proof is impossible, as none of the axioms increase the depth of $\lnot$s across the $\to$ (i.e. none of them have a more knotty right-hand-side than left-hand-side).

Solution 1:

Yes, this is possible, but the proof is not short and simple. From a birds-eye view, the trick is to start by proving double-negation elimination: $$ \neg\neg Q \to Q $$ This requires two instances of axiom 2: $$ (\neg\neg\neg\neg Q \to \neg\neg Q) \to (\neg Q \to \neg\neg\neg Q) \\ (\neg Q \to \neg\neg\neg Q) \to (\neg\neg Q \to Q) $$ If we temporarily assume $\neg\neg Q$, then by axiom 1 we have $\neg\neg\neg\neg Q\to\neg\neg Q$, and by the two implications above get get $\neg\neg Q\to Q$. Since we're still assuming $\neg\neg Q$, we can get $Q$. Now the deduction theorem applied to this reasoning then gives a proof of $\neg\neg Q\to Q$ without any additional assumptions.

To arrive at double-negation introduction, set $Q := \neg P$. The elimination formula we have just proved is then $$ \neg\neg\neg P \to \neg P $$ and a final appeal to axiom 2 converts this into the desired $$ P \to \neg\neg P $$

Unfolding the deduction theorem (and optimising a bit by hand) gives us this somewhat formidable proof, where several internal application of modus ponens have been omitted:

$$ \begin{array}{rll} \\ 1. & \neg^3P \to (\neg^5 P \to \neg^3 P) & \mathrm{Ax.}1 \\ 2. & (\neg^5P \to \neg^3P) \to (\neg^2P\to\neg^4P) & \mathrm{Ax.}2 \\ 3. & \neg^3P \to (\neg^5P \to \neg^3P) \to (\neg^2P\to\neg^4P) & \mathrm{Ax.}1, (2) \\ 4. & \neg^3P \to (\neg^2P \to \neg^4P) & \mathrm{Ax.}3, (3), (1) \\ 5. & (\neg^2P \to \neg^4P) \to (\neg^3P\to\neg P) & \mathrm{Ax.}2 \\ 6. & \neg^3P \to (\neg^2P \to \neg^4P) \to (\neg^3 P\to\neg P) & \mathrm{Ax.}1, (5) \\ 7. & \neg^3P \to (\neg^3P \to \neg P) & \mathrm{Ax.}3, (6), (4) \\ 8. & \neg^3P \to \neg^3P & \mathrm{Ax.}1, \mathrm{Ax.}3 \\ 9. & \neg^3P \to \neg P & \mathrm{Ax.3}, (7), (8) \\ 10. & P\to \neg\neg P & \mathrm{Ax.2}, (9) \end{array} $$

Solution 2:

Is it possible to prove this? :--

$$P\to \lnot\lnot P$$

The person who gave me this problem insists it is provable, although it seems to me that such a proof is impossible, as none of the axioms increase the depth of $\lnot$s across the $\to$ (i.e. none of them have a more knotty right-hand-side than left-hand-side).

The mistake in your reasoning is that with the axioms, you can get more $\neg$'s ... for example, if you have $P$, then with axiom $1$, you can get $Q \rightarrow P$ for any $Q$ ... so this $Q$ could have many more $\neg$'s than the $P$, and using Axiom 2, you can get those to the other aside of the conditional.

Now, the actual proof of $P \rightarrow \neg \neg P$ is pretty nasty. In fact, below I'll assume that you can use the Deduction Theorem, which states that for any $\Gamma$, $\varphi$, and $\psi$:

If $\Gamma \cup \{ \varphi \} \vdash \psi$, then $\Gamma \vdash \varphi \rightarrow \psi$

Now for the proof. First, let's prove: $\phi \to \psi, \psi \to \chi, \phi \vdash \chi$:

1. $\phi \to \psi$ Premise

2. $\psi \to \chi$ Premise

3. $\phi$ Premise

4. $\psi$ MP 1,3

5. $\chi$ MP 2,4

By the Deduction Theorem, this gives us Hypothetical Syllogism (HS): $\phi \to \psi, \psi \to \chi \vdash \phi \to \chi$

Now let's prove the general principle that $\neg \phi \vdash (\phi \to \psi)$:

1. $\neg \phi$ Premise

2. $\neg \phi \to (\neg \psi \to \neg \phi)$ Axiom1

3. $\neg \psi \to \neg \phi$ MP 1,2

4. $(\neg \psi \to \neg \phi) \to (\phi \to \psi)$ Axiom2

5. $\phi \to \psi$ MP 3,4

With the Deduction Theorem, this means $\vdash \neg \phi \to (\phi \to \psi)$ (Duns Scotus Law)

Let's use Duns Scotus to show that $\neg \phi \to \phi \vdash \phi$

1. $\neg \phi \to \phi$ Premise

2. $\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))$ (Duns Scotus Law)

3. $(\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))) \to ((\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi)))$ Axiom3

4. $(\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi))$ MP 2,3

5. $\neg \phi \to \neg (\neg \phi \to \phi)$ MP 1,4

6. $(\neg \phi \to \neg (\neg \phi \to \phi)) \to ((\neg \phi \to \phi) \to \phi)$ Axiom2

7. $(\neg \phi \to \phi) \to \phi$ MP 5,6

8. $\phi$ MP 1,7

By the Deduction Theorem, this means $\vdash (\neg \phi \to \phi) \to \phi$ (Law of Clavius)

Using Duns Scotus and the Law of Clavius, we can now show that $ \neg \neg \phi \vdash \phi$:

1. $\neg \neg \phi$ Premise

2. $\neg \neg \phi \to (\neg \phi \to \phi)$ Duns Scotus

3. $\neg \phi \to \phi$ MP 1,2

4. $(\neg \phi \to \phi) \to \phi$ Law of Clavius

5. $\phi$ MP 3,4

By the Deduction Theorem, this also means that $\vdash \neg \neg \phi \to \phi$ (DN Elim)

Now we can prove $\vdash \phi \to \neg \neg \phi$ (DN Intro) as well:

1. $\neg \neg \neg \phi \to \neg \phi$ (DN Elim)

2. $(\neg \neg \neg \phi \to \neg \phi) \to (\phi \to \neg \neg \phi)$ Axiom 2

3. $\phi \to \neg \neg \phi$ MP 1,2