# 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". Commented Sep 30, 2010 at 17:25
• You should state the axioms as well, not all books have the same set of axioms or in the same order. Commented Sep 30, 2010 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)). Commented Sep 30, 2010 at 17:40
• If you have $\neg\beta$ defined to be $\beta\rightarrow\bot$, then you just need the deduction theorem and modus ponens. Commented Sep 30, 2010 at 18:30
• anyone know how to get tex to show up right? i'll edit my post to include the axioms Commented Oct 1, 2010 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! Commented Oct 1, 2010 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. Commented Oct 1, 2010 at 17:31
• I think if you are using Axiom 3 then it is better simply to apply modus ponens on $\neg\neg\neg \beta\to \neg \beta$ (obtained by the theorem schema that $\vdash \neg\neg p\to p$, already proved) and $(\neg\neg\neg \beta\to \neg \beta)\to (\beta\to \neg\neg \beta)$.
– user170039
Commented Sep 22, 2016 at 13:22

$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. Commented Feb 10, 2011 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/…
– user4414
Commented Feb 26, 2011 at 21:49