I am currently going through Philip Wadler's "Proposition as Types" and a passage of the introduction has struck me:

Propositions as Types is a notion with breadth. It applies to a range of logics including propositional, predicate, second-order, intuitionistic, classical, modal, and linear.

I am familiar with intuitionistic and classical logic but I could not find any direct, informal explanations of the differences and nuances between each of those on the Internet.

  • 1
    $\begingroup$ For linear logic, Wadler's own "Linear types can change the world!" is not a bad introduction. $\endgroup$ May 31, 2015 at 23:36

2 Answers 2


Proof theoretically intuitionist logic is a sub-theory of classical logic. The Wikipedia article indicates this by indicating that if we have a certain set of axioms for intuitionist logic (those axioms can get found under the section entitled "Hilbert style calculus", then classical logic may get obtained by joining to the system the law of the excluded middle... in Polish notation ApNp, Peirce's law CCCpqpp, or the law of double negation elimination CNNpp, or with the definition Np := Cp0, we might write CCCp00p.

Thus, all formal proofs done in a an intuitionist logic framework work as proofs for any classical logic framework, but not all proofs done in a classical logic framework will work in any intuitionist logic framework.

For example, one might deduce Cpp from a classical logic framework as follows:

thesis 1 CCpqCCqrCpr
thesis 2 CpCNpq
thesis 3 CCNppp
DD123  4 Cpp

This is not a possible proof of Cpp in any intuitionist logic framework, since CCNppp is not a thesis in any intuitionist logic (the term "thesis" refers to a formula which is either an axiom or a theorem).

Semantically speaking intuitionist logic qualifies as much richer than classical logic in that the truth set for intuitionist logic is infinite-valued, while that of classical logic is two-valued. Semantically speaking, intuitionist logic behaves the same way as classical logic when truth-values get confined to "True" and "False". In such a case, each formula whether interpreted from the perspective of classical logic or intuitionist logic yields the same result. But, intuitionist logic can get said to reject the law of bivalence in that no two-valued models of intuitionist logic qualify as adequate for a semantics of it.

  • $\begingroup$ Could you please elaborate on the polish notation thing? How is that related to logic, to LEM or Pierce's Law? Thank you! $\endgroup$ Jun 5, 2015 at 0:00
  • $\begingroup$ There isn't much relation to LEM or Peirce's law (though identifying the principal connective of those formulas is easier in Polish notation than in infix notation). Polish notation involves putting functions before their arguments uniformly, with "C" standing for implication, and "N" for negation. "C" takes two arguments, and "N" takes one. You might see here plato.stanford.edu/entries/lukasiewicz/polish-notation.html or the wikipedia for more details online. It might interest you to know that some of the original papers written in Polish notation got burned. $\endgroup$ Jun 5, 2015 at 1:25

Intuitionistic logic could be succintly described as classical logic that violates the law of excluded middle (LEM), i.e. $A\lor \lnot A$ is not always true in intuitionistic logic. This is mainly due to the intuitionistic negation being an intensional operator.

This can be seen if we consider the canonical (Brower-Heyting-Kolmogorov) interpretation: a proof of $\lnot A$ means that there is a proof that there is no proof for $A$. Now take some as yet unproven conjecture---say the twin prime conjecture $TP$.

Now, since there's neither a proof of $TP$ nor is there a proof that there is no proof of $TP$, it follows from the definition of '$\lor$' that there's no proof of $TP \lor \lnot TP$.

  • 1
    $\begingroup$ LEM isn't valid in intuitionistic logic --- the statement you're taking issue with says no more than that. Do you then also take issue with the following relevant section of the SEP article? plato.stanford.edu/entries/logic-intuitionistic/#RejTerNonDat $\endgroup$ Jun 1, 2015 at 18:18
  • 3
    $\begingroup$ The general phenomenon that @DougSpoonwood gave several specific instances of is that, in the many different axiomatizations of classical logic, there are different parts that go beyond intuitionistic logic. In some systems, that part is $p\lor\neg p$; in some it is $(\neg\neg p)\to p$; in some it is not an axiom at all but a definition of $p\lor q$ as $(\neg p)\to q$; etc. Furthermore, it is not guaranteed that an arbitrary complete axiomatization of classical logic can be split into a complete axiomatization of intuitionistic logic plus intuitionistically invalid stuff. $\endgroup$ Jun 1, 2015 at 22:19
  • 1
    $\begingroup$ @ErwanAaron The difficulty is that "LEM is not an axiom or double negation" doesn't uniquely describe intuitionistic logic. One can axiomatize classical logic in such a way that neither LEM nor double negation is an axiom. Of course, such an axiomatization will contain some other non-intuitionistic principle, which then ought to be removed, but your definition doesn't cover that. Furthermore, I expect that one could axiomatize classical logic in such a way that none of the axioms are intuitionistically acceptable, so they'd all need to be removed. $\endgroup$ Jun 5, 2015 at 0:44
  • 2
    $\begingroup$ @ErwanAaron I hoped you don't mind me responding. Consider the axiom set that the Wikipedia gives for intuitionistic logic under the section for Hilbert-style calculus. Call that system IL. Define a thesis as a theorem or an axiom. An intutionistic logic is any formal system that has the same theses as IL. $\endgroup$ Jun 5, 2015 at 4:11
  • 2
    $\begingroup$ @ErwanAaron Doug Spoonwood has given a good answer to your first question. I'd add that there are other, equivalent axiomatizations in the literature, and they could be used in place of IL in Doug's answer. For your second question, about "subset of classical ...", your proposed description is true but also applies to some other, weaker systems than intuitionistic logic. Also, it presupposes that "constructive provability" has already been defined, whereas, in fact, defining it seems to be one of the main issues here. $\endgroup$ Jun 5, 2015 at 13:44

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .