MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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)

share|cite|improve this question

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.

share|cite|improve this answer
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"? – Buschi Sergio Dec 26 '11 at 15:32

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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