Constructive mathematics

Existence and Logic

The classic approach to math logic is the same as Aristotle's: a thing either is or is not. Classical logic is bivalent, admitting only two truth values, and, moreover, something is either true or false, not both nor neither, and it is so independently of any evidence either way. It admits the law of the excluded middle (LEM), A ∨ ¬A; a negation of truth immediately yields falsehood, ¬T = F and F = ¬T; this also implies the law of double negation (DN) that ¬¬T = T and that ¬¬F = F. Constructivist disagree, which is embedded in the intuitionistic logic, which doesn't admit LEM and DN.

What exactly constitutes a proof of existence of an object with certain properties is met with two views. A mathematician of the classic persuasion will state that to prove ∃x.P(x), it is sufficient to prove that ∀x.¬P(x) is contradictory. A constructivist would argue that all that proof establishes is the contradiction: the proof of existence must supply an x (the so-called witness) and prove that P(x) holds.

Classical proof relies on the LEM, ∃x.P(x) ∨ ¬∃x.P(x): if ∀x.¬P(x), which is equivalent to ¬∃x.P(x), is contradictory, then it must be ∃x.P(x).

An interesting effect of constructivising is that classically equivalent results often split into a number of constructively inequivalent results, one or more of which can be shown to be valid by constructive means.

The constructive view of logic concentrates on what it means to prove or to demonstrate convincingly the validity of a statement, rather than concentrating on the abstract truth conditions which constitute the semantic foundation of classical logic.