About logical axioms of propositional logic. I see in th P . Johnstone little (but dense) book "Notes on logic and Sety theory" that propositional logical calculus as the follow three axioms:
1) $(p\Rightarrow (q\Rightarrow p)$
2) $[p\Rightarrow (q\Rightarrow r)] \Rightarrow [(p\Rightarrow q)\Rightarrow (p\Rightarrow r)]$
3) $\neg\neg p \Rightarrow p$
where $\neg p$ is an abbreviation of $p\Rightarrow \bot$ 
Then is proved that any tautology follow from some dedution from these axioms.
In particular: 
3') $p\Rightarrow \neg\neg p $
Then reading the (still) Johnstone  "Sketches of an Elephant II" about categorical logic I see at. p.830 the structural rules $(a), (b), (c), (d), (e)$ for make a syntactic deduction (the other rules are about existential or universal quantifiers) then I ask (to myself):
" can we deduce from  from these any tautology?"
Then I working for deduce the axioms $(1), (2), (3)$ above, I get the firs two, and at soon I understand that cannot get the axiom $(3)$ just because in a Heyting algebra I only have $x\leq \neg\neg x$ (like in the $(3')$ above) and no the reverse (then the equality, that is true in Boolean contest). THen I see that the $(3')$ above is deducible from the 
structural ruels $(a), (b), (c), (d), (e)$. 
THen I ask: are $(1), (2), (3')$  admisible as axioms for the propositional logic?
(Good Christman time to all) 
 A: Which propositional logic are you asking about? Axioms K (your axiom 1) and S (your axiom 2) are admissible for the implicational fragment of intuitionistic propositional logic, but your axiom 3 is not. Your axiom 3' is redundant and follows from K and S. Short proof: $S(K(S(SKK)))K a b = b a$; apply the Curry–Howard isomorphism. Explicitly:


*

*(K) $p \to (\lnot p \to p)$

*(K) $\lnot p \to (\lnot p \to \lnot p)$

*(K) $\lnot p \to ((\lnot p \to \lnot p) \to \lnot p)$

*(S) $(\lnot p \to ((\lnot p \to \lnot p) \to \lnot p)) \to ((\lnot p \to (\lnot p \to \lnot p)) \to (\lnot p \to \lnot p))$

*(MP 3, 4) $(\lnot p \to (\lnot p \to \lnot p)) \to (\lnot p \to \lnot p)$

*(MP 2, 5) $\lnot p \to \lnot p$

*(S) $(\lnot p \to \lnot p) \to ((\lnot p \to p) \to \lnot \lnot p)$

*(MP 6, 7) $(\lnot p \to p) \to \lnot \lnot p$

*(K) $((\lnot p \to p) \to \lnot \lnot p) \to (p \to ((\lnot p \to p) \to \lnot \lnot p))$

*(MP 8, 9) $p \to ((\lnot p \to p) \to \lnot \lnot p)$

*(S) $(p \to ((\lnot p \to p) \to \lnot \lnot p)) \to ((p \to (\lnot p \to p)) \to (p \to \lnot \lnot p))$

*(MP 10, 11) $(p \to (\lnot p \to p)) \to (p \to \lnot \lnot p)$

*(MP 1, 12) $p \to \lnot \lnot p$


In fact, if we replace $\lnot A$ by $A \to q$, then the above derives $p \to ((p \to q) \to q)$ from axioms K and S. It's not surprising that this is derivable from K and S alone: it is easy to verify that $\lambda x . \lambda y . y x$ is a lambda term of the required type.
