What does “classical logic” mean?

I'm a junior researcher in Computer Science field and I've had some difficulties with some scientific terms like the one on the title "classical logic" which is used to represent and identify some other things. Could any one "simplify" the meaning a bit??

• Have you looked at the Wikipedia article? – Qiaochu Yuan Oct 3 '12 at 21:32
• One cannot rely on uniformity of terminology. Among non-classical logics the author may have in mind are the various flavours of modal logic. – André Nicolas Oct 3 '12 at 23:06

Classical logic is the logic usually used for mathematical reasoning, where things such as $P\lor \neg P$ are always provable no matter what the formula $P$ is.

The most prominent alternative to classical logic is intuitionistic logic, which started out as an attempt to formalize the kind of reasoning that the "intuitionist" school of mathematicians about a century ago accepted as valid. In intuitionistic locic $P\lor \neg P$ is not always a theorem, nor does $\neg\neg P$ mean the same thing as $P$ itself, and De Morgan's laws are not exact equivalences. (On the other hand, every proof in intuitionistic logic is also valid in classical logic).

There are very few (if any) mathematicians today who think ordinary mathematical reasoning should be restricted to something like what intuitionistic logic allows. It is still interesting as a formal object of study in its own right.

Of particular interest for computer science is that "formulas" and "proofs" in propositional intuitionistic logic correspond exactly to "types" and "terms" in the simply typed lambda calculus extended with product and sum types, via the Curry-Howard isomorphism.

• It is perhaps worth adding, though, that an intuitionistically acceptable proof can give you more information -- e.g. by providing a recipe for a witness for an existential quantification. And such extra info can be worth having. – Peter Smith Oct 3 '12 at 22:53
• @PeterSmith: Yes, and this is very closely connected with the fact that terms in the lambda calculus (which encode intuitionistic proofs) can be executed as programs, giving a direct natural semantics for the "constructive" content of intuitionistic proofs. – Henning Makholm Oct 3 '12 at 22:55

What does it take to establish a proposition of the form $\exists x Fx$? Do you think you must be able to exhibit or at least give a recipe for constructing a particular object $a$ such that $Fa$? Or is it on occasion enough to proceed indirectly and show that the supposition that $\neg\exists xFx$ leads to absurdity?

If you take the first line, you are giving a constructivist or intuitionist reading of the quantifier. On the second line, you are giving a non-constructive or classical reading of the quantifier. The latter goes with a classical understanding of negation more generally, according to which showing that $\neg P$ leads to absurdity shows not just that $\neg\neg P$ (which is agreed on all sides) but also to plain $P$ (which is disputed by constructivists).

Depending how you read the quantifier and negation, your logic will vary. On the constructive readings you will probably end up with intuitionist logic, and you will not endorse double-negation elimination or some related principles like excluded middle. On the non-constructive readings you get the standard classical quantification logic of the founding fathers such as Frege, Russell and Whitehead, Hilbert and Ackermann, etc.

So, in headline terms, "classical" indicates the logic developed by the classic authors of the modern era, and contrasts principally with intuitionist logic.

(Some people, less helpfully I think, use "classical" to contrast the old core you find in e.g. Hilbert and Ackermann with later developements like modal logic. etc.: but I think the usually intended contrast is not "classical" vs. "new-fangled" but "classical" vs. "constructivist".)

• A quibble: '..."classical" indicates the logic developed by the classic authors of the modern era...' Isn't classical logic also referred to as Aristotelian logic, implying that it dates to long before the modern era? – Ben Crowell Oct 3 '12 at 22:39
• No. In standard modern usage, classical logic means Frege and after -- see e.g. plato.stanford.edu/entries/logic-classical In this sense, ancient Aristotelian logic is pre-classical. (Compare: classical dynamics does not mean ancient theories of motion!) – Peter Smith Oct 3 '12 at 22:44
• Note that the distinction between classical and intuitionistic logic is not limited to reasoning about quantifiers. It shows up already on the propositional level (at least formally; the philosophical considerations behind the distinction seem to become rather degenerate without quantifiers). – Henning Makholm Oct 3 '12 at 22:52
• @HenningMakholm "[T]he philosophical considerations behind the distinction seem to become rather degenerate without quantifiers". Absolutely. Which is why I started from there. The late Michael Dummett is very good on this sort of thing in his classic Elements of Intuitionism. – Peter Smith Oct 3 '12 at 22:56