Deriving A, ¬A ⊢ B in a weak Hilbert proof system

Question

I am asked to derive A, ¬A ⊢ B in the following supposedly weaker system:

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

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

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

Inference rule: Modus Ponens

Proved: Deduction theorem

Here is what I have tried:

1. $((¬B \to A) \to ((¬B \to ¬A) \to ¬¬B))$ [Ax 3]

2. $(A \to (¬B \to A))$ [Ax 1]

3. $A$ [Ass]

4. $(¬B \to A)$ [MP, 2, 3]

5. $((¬B \to ¬A) \to ¬¬B)$ [MP, 1, 4]

6. $(¬A \to (¬B \to ¬A))$ [Ax 1]

7. $¬A$ [Ass]

8. $(¬B \to ¬A)$ [MP, 6, 7]

9. $¬¬B$ [MP,5, 8]

Now I'm stuck because I can't see how to derive $⊢ ¬¬B \to B$ (I have been able to derive $B \to ¬¬B$). Maybe there's a completely different way to derive $A, ¬A ⊢ B$, possibly using the Deduction theorem, that I can't see.

Answer 1

Mayhap you missed an additional axiom, or whoever assigned this problem tried to pull a fast one on you? Either way, you cannot derive $A \rightarrow \neg A \rightarrow B$ in the Hilbert system given by the three axioms

1. $A \rightarrow B \rightarrow A$,
2. $(A \rightarrow B \rightarrow C) \rightarrow (A \rightarrow B) \rightarrow A \rightarrow C$, and
3. $(A \rightarrow B) \rightarrow (A \rightarrow \neg B) \rightarrow \neg A$.

First, let me note that your current strategy cannot go any further: you certainly can't derive $\neg\neg B \rightarrow B$ in this system. Why? Well, all three of the axioms above hold not just in the usual classical logic, but in intuitionistic logic as well. If you could prove double-negation elimination from the three axioms, then double-negation elimination would hold in intuitionistic logic too; but it famously does not.

Even though this particular strategy cannot work, one could still hope for a completely different way to derive $A, \neg A \vdash B$. To dash this hope once and for all, I'll give an algebraic semantics to the Hilbert system with the three axioms above, which demonstrates that this system cannot derive $A \rightarrow \neg A \rightarrow B$.

Our semantics will have two truth-values, $0$ and $1$. We define the implication operation $\rightarrow$ in the way familiar from classical logic, by the equations $0 \rightarrow x = 1$ and $1 \rightarrow x = x$. However, we define the negation operation $\neg$ in a very unusual way, by the equation $\neg x = 1$ for all $x$.

Now, notice that no matter how you assign values $0,1$ to the variables $x,y,z$, the algebraic expressions corresponding to the three axioms above always satisfy the equalities

1. $x \rightarrow y \rightarrow x = 1$,
2. $(x \rightarrow y \rightarrow z) \rightarrow (x \rightarrow y) \rightarrow (x \rightarrow z) = 1$, and
3. $(x \rightarrow y) \rightarrow (x \rightarrow \neg y) \rightarrow \neg x = 1$.

Moreover, if $x \rightarrow y = 1$ and $x = 1$ both hold, then $y = 1$ must hold as well. Thus, if one can derive some proposition $\varphi$ in the system above, then the algebraic expression corresponding to $\varphi$ evaluates to $1$ no matter which values one assign to the variables.

But if one sets $x = 1$ and $y = 0$, then the algebraic expression $x \rightarrow \neg x \rightarrow y$ corresponding to $A \rightarrow \neg A \rightarrow B$ evaluates to $1 \rightarrow (1 \rightarrow 0) = 1 \rightarrow 0 = 0$, instead of the value $1$. Thus, as claimed, one cannot derive $A \rightarrow \neg A \rightarrow B$ in the Hilbert system presented above (and therefore, by the deduction theorem, $A,\neg A \vdash B$ cannot be obtained either).

Note: one could arrive at the same conclusion by considering minimal logic instead of intuitionistic logic in the first argument above. Indeed that's how I knew that this particular two-valued semantics would do the job.