How to prove ~~P from P in the Hilbert Axiomatic System?

Question

Can someone provide me with hints for, or a rough sketch of, a proof of ~~P from P in the Hilbert system? I had very little trouble proving the reverse, that P is provable from ~~P, but seem to be totally stuck on this guy. My axioms are the following:

φ->(ψ->φ) (1)

[φ->(ψ->χ)]->[(φ->ψ)->(φ->χ)] (2)

(~ψ->~φ)->[(~ψ->φ)->ψ] (3)

and my one rule of inference is modus ponens.

I am also allowed to work with tools like ex falso quodlibet, transitivity, weakening the consequent, etc.

Any help would be greatly appreciated; thank you!

Answer 1

You say you can derive $P$ from $\neg \neg P$. Using the Deduction theorem, you can therefore prove $\neg \neg P \rightarrow P$. And that means that we can use $\neg \neg \varphi \rightarrow \varphi$ as a Lemma.

Now, let's show that $\neg \psi \rightarrow \neg \varphi, \varphi \vdash \psi$:

1. $\neg \psi \rightarrow \neg \varphi$ Premise
2. $\varphi$ Premise
3. $\varphi \rightarrow (\neg \psi \rightarrow \varphi)$ Axiom 1
4. $\neg \psi \rightarrow \varphi$ MP 2,3
5. $(\neg \psi \rightarrow \neg \varphi) \rightarrow ((\neg \psi \rightarrow \varphi) \rightarrow \psi$ Axiom 3
6. $(\neg \psi \rightarrow \varphi) \rightarrow \psi$ MP 1,5
7. $\psi$ MP 4,6

Using the Deduction Theorem, that means we can also prove $(\neg \psi \rightarrow \neg \phi) \rightarrow (\varphi \rightarrow \psi)$ (this statement is usually used as the third axiom in the Hilbert System ... so let's call it Axiom 3')

OK, so then:

1. $P$ Premise
2. $\neg \neg \neg P \rightarrow \neg P$ Lemma
3. $(\neg \neg \neg P \rightarrow \neg P) \rightarrow (P \rightarrow \neg \neg P)$ Axiom 3'
4. $P \rightarrow \neg \neg P$ MP 2,3
5. $\neg \neg P$ MP 1,4

Answer 2

Here's a computer generated rough sketch of a detachment based proof. I used the theorem prover, Prover9, which is freely available online courtesy of Argonne National Laboratory near Chicago. You'll need to find the substitution instances of axioms and theorems in order to fill in the details. I used '~' instead of $\lnot$ as a symbol. I didn't use any strategy whatsoever. I merely embedded the axioms into the first-order context appropriate for the theorem-prover and used "-P(x-> y) | -P(x) | P(y)." since under hyperressolution (the hyper referenced in the proof) it behaves like condensed detachment does in propositional calculus:

% -------- Comments from original proof -------- 
% Proof 1 at 0.03 (+0.00) seconds. 
% Length of proof is 17. 
% Level of proof is 7. 
% Maximum clause weight is 20. 
% Given clauses 48.

1 P(~(~(x)) -> 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)) -> ((~(x) -> y) -> x)). [assumption]. 
6 -P(~(~(c1)) -> 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)]. 
10 P((x -> y)-> (x -> x)).  [hyper(2,a,4,a,b,3,a)]. 
11 P(((~(x) -> ~(y)) -> (~(x) -> y)) -> ((~(x) -> ~(y)) -> x)).  [hyper(2,a,4,a,b,5,a)]. 
17 P(x -> x).  [hyper(2,a,10,a,b,7,a)]. 
20 P(x -> (y -> y)). [hyper(2,a,3,a,b,17,a)]. 
27 P((x -> ((y -> x) -> z)) -> (x -> z)). [hyper(2,a,8,a,b,7,a)]. 
71 P((~(x) -> ~(~(x))) -> x). [hyper(2,a,11,a,b,20,a)]. 
77 P(x -> ((~(y) -> ~(~(y))) -> y)). [hyper(2,a,3,a,b,71,a)]. 
255 P(~(~(x)) -> x). [hyper(2,a,27,a,b,77,a)]. 
256 $F.  [resolve(255,a,6,a)].

============================== end of proof ==========================