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)


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

  • $\begingroup$ Thank you very much Zhen Lin. For " propositional logic" I was mean tha classical one (the Lindembaum algebra is the free boolean algebra on the primitive (atomic) proposition), and as the above $(1), (2), (3)$ as axioms . Now I realize that axiom $(3)$ isnt derivable from the Johnstone genaral categorical logic, because is about tha particular boolean context. Can you hint me some books about "general propositional logic"? $\endgroup$ Dec 26, 2011 at 15:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.