Prove double negation introduction with this axiom system.

Question

I want to find a proof for ( $⊢A \rightarrow ¬¬A $ ) with these four axioms:

A1: $ A \rightarrow (B\rightarrow A) $

A2: $ (A \rightarrow (B\rightarrow C)) \rightarrow ((A\rightarrow B)\rightarrow(A\rightarrow C)) $

A3: $ \lnot\lnot A \rightarrow A $

A4: $ \lnot A \leftrightarrow (A\rightarrow \bot) $

These axioms are some Hilbert system so I tried to prove A3 which is:

Ax3 : $ (( \lnot B \rightarrow \lnot A)\rightarrow(( \lnot B \rightarrow A)\rightarrow B))) $

But i couldn't do that. so i thought maybe this system with these 4 Axioms cant do that, but i think with double-negation elimination rule and first two rules of Hilbert system it should be able to do such thing.

Thanks.

Answer 1

By modus ponens, we see

$$A, (A \to \bot) \vdash \bot$$

Then applying the deduction theorem twice, we find

$$ \vdash A \to (A \to \bot) \to \bot$$

Lastly, we apply axiom $4$ twice to see

$$ \vdash A \to \lnot \lnot A $$

---

I hope this helps ^_^