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.
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)