Prove that $\beta \rightarrow \neg \neg \beta$ is a theorem using standard axioms 1,2,3 and MP

Question

I've proven that $\neg \neg \beta \rightarrow \beta$ is a theorem, but I can't figure out a way to do the same for $\beta \rightarrow \neg \neg \beta$.

It seems the proof would use Axiom 2 and the deduction theorem (which allows $\beta$ to be an axiom)--but I've endlessy tried values to no avail.

Axiom 1: $A \rightarrow ( B \rightarrow A )$.

Axiom 2: $( A \rightarrow ( B \rightarrow C ) ) \rightarrow ( ( A \rightarrow B ) \rightarrow (A \rightarrow C) ) $.

Axiom 3: $( \neg B \rightarrow \neg A) \rightarrow ( ( \neg B \rightarrow A) \rightarrow B )$.

To clarify: A, B, C, $\alpha$, and $\beta$ are propositions (i.e. assigned True or False). $\rightarrow$ and $\neg$ have the standard logical meanings.

Note: $\TeX$ification does not work in the IE9 beta.

Answer 1

I'll use the deduction theorem, so I'll assume $\beta$ and need to prove $\neg\neg\beta$.

1. $\beta$ (assumption)

2. $\beta\to (\neg\neg\neg\beta\to\beta)$ (axiom 1)

3. $\neg\neg\neg\beta\to\beta$ (modus ponens using 1 and 2)

4. $\neg\neg\neg\beta\to\neg\beta$ (you have proved that $\neg\neg\beta\to\beta$ is a theorem)

5. $(\neg\neg\neg\beta\to\neg\beta)\to((\neg\neg\neg\beta\to\beta)\to\neg\neg\beta)$ (axiom 3)

6. $(\neg\neg\neg\beta\to\beta)\to\neg\neg\beta$ (modus ponens using 4 and 5)

7. $\neg\neg\beta$ (modus ponens using 3 and 6)

Answer 2

$A \rightarrow \lnot \lnot A$ is intuitionistically valid. Therefore you should be able to proof it already from MP plus Axiom 1 and Axiom 2 plus Ex Falso Quodlibet (An axiom that amounts to $\bot \rightarrow A$). No need to use Axiom 3.

But there is a twist, you need to represent $\lnot A$ as $A \rightarrow \bot$. Here you see a Hilbert style proof of $A \rightarrow ((A \rightarrow \bot) \rightarrow \bot)$:

We need first a little lemma, namely that $A \rightarrow A$ is derivable:

1: $(A \rightarrow ((B \rightarrow A) \rightarrow A)) \rightarrow ((A \rightarrow (B \rightarrow A)) \rightarrow (A \rightarrow A))$ (Axiom 2)
2: $A \rightarrow ((B \rightarrow A) \rightarrow A)$ (Axiom 1)
3: $(A \rightarrow (B \rightarrow A)) \rightarrow (A \rightarrow A)$ (MP 1, 2)
4: $A \rightarrow (B \rightarrow A)$ (Axiom 1)
5: $A \rightarrow A$ (MP 3, 4)

Now we can proof what we desire:

1: $(A \rightarrow (((A \rightarrow \bot) \rightarrow A) \rightarrow ((A \rightarrow \bot) \rightarrow \bot))) \rightarrow ((A \rightarrow ((A \rightarrow \bot) \rightarrow A)) \rightarrow (A \rightarrow ((A \rightarrow \bot) \rightarrow \bot)))$ (Axiom 2)
2: $(((A \rightarrow \bot) \rightarrow A) \rightarrow ((A \rightarrow \bot) \rightarrow \bot)) \rightarrow (A \rightarrow (((A \rightarrow \bot) \rightarrow A) \rightarrow ((A \rightarrow \bot) \rightarrow \bot)))$ (Axiom 1)
3: $((A \rightarrow \bot) \rightarrow (A \rightarrow \bot)) \rightarrow (((A \rightarrow \bot) \rightarrow A) \rightarrow ((A \rightarrow \bot) \rightarrow \bot))$ (Axiom 2)
4: $(A \rightarrow \bot) \rightarrow (A \rightarrow \bot)$ (Lemma)
5: $((A \rightarrow \bot) \rightarrow A) \rightarrow ((A \rightarrow \bot) \rightarrow \bot)$ (MP 3, 4)
6: $A \rightarrow (((A \rightarrow \bot) \rightarrow A) \rightarrow ((A \rightarrow \bot) \rightarrow \bot))$ (MP 2, 5)
7: $(A \rightarrow ((A \rightarrow \bot) \rightarrow A)) \rightarrow (A \rightarrow ((A \rightarrow \bot) \rightarrow \bot))$ (MP 1, 6)
8: $A \rightarrow ((A \rightarrow \bot) \rightarrow A)$ (Axiom 1)
9: $A \rightarrow ((A \rightarrow \bot) \rightarrow \bot)$ (MP 7, 8)

The given proof shows something even stronger, $A \rightarrow \lnot \lnot A$ is not only intuitionistically valid, it is already valid in minimal logic, since we did not make use of Ex Falso Quodlibet. We were able to derive it from MP plus Axiom 1 and Axiom 2.

Best Regards