What is the difference between intuitionistic, classical, modal and linear logic?

Question

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.

Answer 1

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

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