About logical axioms of propositional logic.

Question

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)

Answer 1

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:

1. (K) $p \to (\lnot p \to p)$
2. (K) $\lnot p \to (\lnot p \to \lnot p)$
3. (K) $\lnot p \to ((\lnot p \to \lnot p) \to \lnot p)$
4. (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))$
5. (MP 3, 4) $(\lnot p \to (\lnot p \to \lnot p)) \to (\lnot p \to \lnot p)$
6. (MP 2, 5) $\lnot p \to \lnot p$
7. (S) $(\lnot p \to \lnot p) \to ((\lnot p \to p) \to \lnot \lnot p)$
8. (MP 6, 7) $(\lnot p \to p) \to \lnot \lnot p$
9. (K) $((\lnot p \to p) \to \lnot \lnot p) \to (p \to ((\lnot p \to p) \to \lnot \lnot p))$
10. (MP 8, 9) $p \to ((\lnot p \to p) \to \lnot \lnot p)$
11. (S) $(p \to ((\lnot p \to p) \to \lnot \lnot p)) \to ((p \to (\lnot p \to p)) \to (p \to \lnot \lnot p))$
12. (MP 10, 11) $(p \to (\lnot p \to p)) \to (p \to \lnot \lnot p)$
13. (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.