Im supposed to prove
$$\vdash(P\implies \neg P)\implies(\neg\neg P \implies \neg P)$$
from following axioms:
$P\implies ( Q \implies P )$
$P\implies ( Q \implies R ) \implies (P\implies Q)\implies(P\implies R)$
$(\neg Q \implies \neg P)\implies(P\implies Q)$
I have also proven/is also known that:
$P\implies \neg \neg P$
$\neg\neg P\implies P$
$(P\implies \neg P)\implies \neg P$
Every attempt i've had has led to nowhere.. Any tips? Thanks in advance
On
Here is a proof of : $(P \to \lnot P) \vdash (\lnot \lnot P \to \lnot P).$
You have proved: $\vdash \lnot \lnot P \to P$. Thus:
1) $(P \to \lnot P)\vdash (\lnot \lnot P \to P)$
2) $(P \to \lnot P)\vdash \lnot \lnot P \to (P \to \lnot P)$ --- from (Ax.1) by mp
3) $\vdash [\lnot \lnot P \to (P \to \lnot P)] \to [(\lnot \lnot P \to P) \to (\lnot \lnot P \to \lnot P)]$--- (Ax.2)
Thus, from 1), 2) and 3) by mp twice, we get:
4) $(P \to \lnot P) \vdash (\lnot \lnot P \to \lnot P).$
Now, we can use the Deduction Th to conclude with:
5) $\vdash (P \to \lnot P) \to (\lnot \lnot P \to \lnot P)$.
In a similar way, we can avoid the last application of DT through a longer derivation based on (Ax.1), (Ax.2) only:
1) $\vdash \lnot \lnot P \to P$
2) $\vdash (P \to \lnot P ) \to (\lnot \lnot P \to P)$ --- from Ax.1 and 1) by mp
3) $\vdash (P \to \lnot P)\to [(\lnot \lnot P \to P) \to (P \to \lnot P)] \text { (Ax.1)}$
4) $\vdash \{ (P \to \lnot P)\to [(\lnot \lnot P \to P) \to (P \to \lnot P)] \} \to \{ [(P \to \lnot P ) \to (\lnot \lnot P \to P)] \to [(P \to \lnot P) \to (\lnot \lnot P \to \lnot P)] \} \text { (Ax.2)}$
5) $\vdash [(P \to \lnot P ) \to (\lnot \lnot P \to P)] \to [(P \to \lnot P) \to (\lnot \lnot P \to \lnot P)]$--- from 3) and 4) by mp
6) $\vdash (P \to \lnot P) \to (\lnot \lnot P \to \lnot P)$--- from 2) and 5) by mp.
If you have the deduction theorem, this is equivalent to showing $(P\Rightarrow \neg P)\vdash(\neg\neg P \Rightarrow \neg P)$, which is equivalent to $\{P\Rightarrow \neg P, \neg \neg P\}\vdash \neg P$. But this is straight forward: