Syntactically deduce $p\vdash \neg\neg p$

Question

Given the following axioms $$\begin{aligned}&1. p\Rightarrow (q\Rightarrow p)\\&2. [p\Rightarrow (q\Rightarrow r )] \Rightarrow [(p\Rightarrow q)\Rightarrow (p\Rightarrow r)]\\&3. \neg\neg p \Rightarrow p \end{aligned}$$ and the deduction rule of modus ponens, I want to prove that $$p\vdash \neg\neg p$$ and should therefore use the Deduction Theorem.

Has anyone a hint how to start?

Answer 1

I will outline the basic idea of the proof, but you can formalize it. We set, $q\equiv(\neg \neg p \to p)$ and, $r \equiv (\neg \neg p)$ and let $p \equiv p$. Then, by axiom 2, we have that

$$[p \to (q \to r)] \to [(p \to q)\to (p \to r)]$$

is equivalent to

$$[p \to ((\neg \neg p \to p) \to (\neg \neg p))] \to [(p \to (\neg \neg p \to p))\to (p \to (\neg \neg p))]$$

On the LHS, since we assumed $p$, we now have $(\neg \neg p \to p) \to (\neg \neg p)$. By axiom 1, this also holds. Therefore, the RHS of the sentence must also hold.

Now, we consider the RHS. The LHS of the RHS holds by axiom 1 as well. Hence, we then get the RHS of the RHS must hold, which is $(p \to \neg \neg p)$, i.e. the statement we are trying to prove.

Note: If this post is too confusing, I will be glad to rewrite it in the morning.

Answer 2

To solve questions like these in general, it may help to reverse engineer the proof. Suppose we had a proof of $\vdash p \Rightarrow \lnot \lnot p$. There must be a first such occurrence of $p \Rightarrow \lnot \lnot p$ within the proof.

Notice that this first such occurrence cannot be in the conclusion of a modus ponens application. This is because if modus ponens was applied on $\{A, A \Rightarrow B\}$ to infer the conclusion $B$ and if the $B$ contains an occurrence of $p \Rightarrow \lnot \lnot p$, then another occurrence must also occur in the RHS of the premise $A \Rightarrow B$.

Therefore, the first such occurrence of $p \Rightarrow \lnot \lnot p$ must be the rightmost subexpression from an axiom. Here are the forms of all viable candidates:

• From the first axiom schema $A \Rightarrow (B \Rightarrow A)$, they are:
  1. $\lnot \lnot p \Rightarrow (p \Rightarrow \lnot \lnot p)$
  2. $(p \Rightarrow \lnot \lnot ~p) \Rightarrow (B \Rightarrow (p \Rightarrow \lnot \lnot ~p))$
• From the second axiom schema $[A \Rightarrow (B \Rightarrow C)] \Rightarrow [(A \Rightarrow B) \Rightarrow (A \Rightarrow C)]$, they are:
  3. $[p \Rightarrow (B \Rightarrow \lnot \lnot p)] \Rightarrow [(p \Rightarrow B) \Rightarrow (p \Rightarrow \lnot \lnot p)]$
  4. $[A \Rightarrow (B \Rightarrow (p \Rightarrow \lnot \lnot p))] \Rightarrow [(A \Rightarrow B) \Rightarrow (A \Rightarrow (p \Rightarrow \lnot \lnot p))]$
• From the third axiom schema $\lnot \lnot A \Rightarrow A$, it is:
  5. $\lnot \lnot (p \Rightarrow \lnot \lnot ~p) \Rightarrow (p \Rightarrow \lnot \lnot ~p)$

(Note: For the sake of clarity, I used the letters $A$, $B$, and $C$ to denote arbitrary formulas.)

Now, which one of these are actually useful to include in the proof? Since the premise of (1) is logically invalid, it cannot be that. Since using modus ponens on (2) would require that $p \Rightarrow \lnot \lnot p$ was a premise, it cannot be that.

Since the premise of (4) and the premise of (5) both include $p \Rightarrow \lnot \lnot p$ as a subexpression, I would not recommend trying those candidates first.

Thus, as a hint, try to include candidate (3).

Answer 3

Here is the proof.

We can prove it also with a "Natural Deduction-like" proof, using the definition :

$\lnot p := p \rightarrow \bot$.

---

Axioms 1 and 2 are enough to prove : $\vdash \varphi \rightarrow \varphi$ as well as the Deduction Theorem.

---

With the above definition, the proof is quite simple :

i) $p$ --- assumed

ii) $\lnot p$ --- assumed

iii) $p \rightarrow \bot$ --- from ii) by definition of $\lnot$

iv) $\bot$ --- from i) and iii) by modus ponens

v) $\lnot \lnot p$ --- from ii) and iv) by DT and definition of $\lnot$, "discharging" assumption ii).

$\vdash p \rightarrow \lnot \lnot p$ --- from i) and v) by DT.

---

Note

This poof does not use Axiom 3, as expected, due to the fact that $p \rightarrow \lnot \lnot p$ is intuitionistically valid, while Axiom 3 : $\lnot \lnot p \rightarrow p$ is not.