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

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.

-
This is stated and proved as C11 in Section I.3.2 of Bourbaki's "Theory of Sets". – Pierre-Yves Gaillard Sep 30 '10 at 17:25
You should state the axioms as well, not all books have the same set of axioms or in the same order. – Weltschmerz Sep 30 '10 at 17:30
Bourbaki derives it from the four axioms (A or A) implies A, A implies (A or B), (A or B) implies (B or A), (A implies B) implies ((C or A) implies (C or B)). – Pierre-Yves Gaillard Sep 30 '10 at 17:40
If you have $\neg\beta$ defined to be $\beta\rightarrow\bot$, then you just need the deduction theorem and modus ponens. – Charles Stewart Sep 30 '10 at 18:30
anyone know how to get tex to show up right? i'll edit my post to include the axioms – Mahir Oct 1 '10 at 0:16

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)

-
Thank you sir. Any tips on finding a proof sequence? Intuition and experience with this stuff? I've got an exam coming up next wednesday! – Mahir Oct 1 '10 at 15:40
I guess it requires a lot of practice and getting familiar with how the axioms work. For example in this one if you thought about using the 3rd axiom, its structure could hint you towards using 3 negations. Also, when I took a similar course and had to find these kind of proofs, I sometimes found useful to keep in mind how I would prove the sentence intuitively. – Apostolos Oct 1 '10 at 17:31

$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

-
Thanks Jan, I never learned about Ex Falso Quodlibet or using constants (or unary function symbols) like $\bot$ in deductions but nonetheless this is why I love math. Thanks again. – Mahir Feb 10 '11 at 4:50
BTW: On another occasion I did a proof of something else using also minimal logic and two axioms that make it clasical. One will also find hints on techniques that allow one to find proofs: stackoverflow.com/questions/1581256/… – j4n bur53 Feb 26 '11 at 21:49