How to prove (P→¬P)→¬P when ¬ is primitive The logical connectives are → and ¬. Usable logical axioms, theorems and rules are 


*

*A→(B→A)

*(A→(B→C))→((A→B)→(A→C))

*(¬A→¬B)→(B→A)

*¬¬A→A

*A→¬¬A

*modus ponens. 


Deduction theorem is also available.
I know how to do this if there were a falsum constant ⊥ and ¬P were defined as P→⊥. Assuming P and P→¬P I get ¬P:=P→⊥, then ⊥ is deduced from P→⊥ and the added premise P and finally P→⊥ results from the deduction theorem, cancelling P.
Now with ¬ being primitive, all I can get now is P,P→¬P⊢¬P and P,¬P⊢anything. I can't find a way to cancel the additional premise P. (P→¬P)→¬P should be provable because this system is complete relative to the usual truth value semantics.
Thanks.
 A: The easiest way that i consider here is that $A \rightarrow B$ is true when A is false (or) B is true.
So, $p \rightarrow ¬p$ is equivalent to $¬p \lor ¬p \Leftrightarrow ¬p$ 
A: The proof is quite tedious...
We have to prove :

$\vdash (A \to B) \to ((\lnot A \to B) \to B)$ --- (*).

With it, and the additional result : $\vdash A \to A$ --- (§), we have :
1) $\vdash \lnot P \to \lnot P$ --- from (§)
2) $P \to \lnot P$ --- assumed [a]
3) $\vdash (P \to \lnot P) \to ((\lnot P \to \lnot P) \to \lnot P)$ --- from (*)
4) $\lnot P$ --- from 1), 2) and 3) by modus ponens twice

5) $(P \to \lnot P) \to \lnot P$ --- from 2) and 4) by Deduction Th, discharging [a].


Now for the proof of (*) above :
(A) 1) $A \to B$
2) $\lnot \lnot A$ --- assumed [a]
3) $\vdash \lnot \lnot A \to A$
4) $A$ --- by mp
5) $B$ --- by mp
6) $\vdash B \to \lnot \lnot B$
7) $\lnot \lnot B$ --- by mp

8) $A \to B \vdash \lnot \lnot A \to \lnot \lnot B$ --- by DT, discharging [a].


(B) 1) $A \to B$ --- premise
2) $\lnot \lnot A \to \lnot \lnot B$ --- from (A)

3) $A \to B \vdash \lnot B \to \lnot A$ --- from 2) and Ax.3 by mp.


(C) 1) $\vdash \lnot A \to (\lnot B \to \lnot A)$ --- Ax.1

2) $\vdash \lnot A \to (A \to B)$ --- from 1) and Ax.3 by mp and DT.


(D) 1) $\vdash \lnot A \to (A \to \lnot B)$ --- from (C)
2) $\vdash (\lnot A \to (A \to \lnot B)) \to ((\lnot A \to A) \to (\lnot A \to \lnot B))$ --- Ax.2
3) $\vdash (\lnot A \to A) \to (\lnot A \to \lnot B)$ --- from 1) and 2) by mp
4) $\vdash (\lnot A \to \lnot B) \to (B \to A)$ --- Ax.3

5) $\vdash (\lnot A \to A) \to (B \to A)$ --- from 3) and 4) by mp and DT.


(E) 1) $\vdash (\lnot A \to A) \to ((\lnot A \to A) \to A)$ --- from (D)
2) $\vdash (\lnot A \to A) \to (\lnot A \to A)$ --- from $\vdash P \to P$

3) $\vdash (\lnot A \to A) \to A$ --- from 1), 2) and Ax.2 by mp.


(F) 1) $A \to B$ --- premise
2) $\lnot A \to B$ --- premise
3) $\lnot B \to \lnot A$ --- from 1) and (B) by mp
4) $\lnot B \to B$ --- from 3) and 2) by mp and DT
5) $\vdash (\lnot B \to B) \to B$ --- from (E)

6) $A \to B, \lnot A \to B \vdash B$ --- from 4) and 5) by mp.

Now, (*) follows from (F) by DT.


Added
1) $A$ --- premise
2) $\lnot B$ --- premise
3) $A \to B$ --- assumed [a]
4) $B$ --- from 1) and 3) by mp
5) $(A \to B) \to B$ --- from 3) and 4) by DT, discharging [a]
6) $\lnot B \to \lnot (A \to B)$ --- from 5) by (B) above

$A , \lnot B \vdash \lnot (A \to B)$ --- from 1), 2) and 5) by mp.

