Questions tagged [constructive-mathematics]

The term "constructive mathematics" refers to the discipline in mathematics in which one proves the existence of mathematical objects only by presenting a construction that provides such an object. Indirect proofs involving proof by contradiction are considered nonconstructive. Construvtivism is the philosophical stance that the only "true" mathematics as constructive mathematics.

In constructivism, an existence proof is not accepted, unless the object in question is constructed. As an example of a nonconstructive proof, consider the following classical proof of the fact that there are irrational numbers $ a $ and $ b $ such that $ a ^ b $ is rational:

Either $ { \sqrt 2 } ^ { \sqrt 2 } $ is rational, in which case we take $ a = b = \sqrt 2 $; or else $ { \sqrt 2 } ^ { \sqrt 2 } $ is irrational, in which case we take $ a = { \sqrt 2 } ^ { \sqrt 2 } $ and $ b = \sqrt 2 $.

The above argument is nonconstructive, because as it stands, it does not enable us to pinpoint which of the two choices of the pair $ ( a , b ) $ has the required property. An alternative proof for the same theorem which is constructive, goes like:

Take $ a = \sqrt 2 $ and $ b = \log _ 2 9 $.

Also, the law of excluded middle is typically not accepted as an axiom. That's because it can result in nonconstructive reasoning, as the above example illustrates. Therefore classical logic is rejected by constructivists, and instead they use intuitionistic logic, which is essentially classical logic without the law of the excluded middle. There are also mathematical axioms like the axiom of choice rejected by constructivists, as they have nonconstructive consequences.

As some of classical methods are not constructively valid, there are classically valid sentences that don't have constructive proofs. As an example there is no constructive proof for the following sentence:

For every real number $ x $, either $ x < 0 $, $ x = 0 $ or $ x > 0 $.

There is a suitable replacement for this which is constrcutively valid. In many applications this alternative is sufficient, although it's slightly weaker than the classical sentence:

For every real number $ x $ and every positive real number $ \epsilon $, either $ x < 0 $, $ | x | < \epsilon $ or $ x > 0 $.

Constructivism has different varieties, among which the most famous are:

1. intuitionist-logic, a formal basis for the theory of intuitionism founded by L. E. J. Brouwer
2. Recursive constructive mathematics, a.k.a russian construve mathematics, founded by A. A. Markov
3. Bishop's constructive mathematics, founded by E. Bishop