4
$\begingroup$

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??

  • 0
    One cannot rely on uniformity of terminology. Among non-classical logics the author may have in mind are the various flavours of modal logic.2012-10-03

2 Answers 2

4

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.

  • 0
    @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.2012-10-03
4

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".)

  • 0
    @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*.2012-10-03