Constructivism (philosophy of mathematics)

The law of non-contradiction (which states that contradictory statements cannot both be true at the same time) is still valid.

In fact, L. E. J. Brouwer, founder of the intuitionist school, viewed the law of the excluded middle as abstracted from finite experience, and then applied to the infinite without justification.

And while the conjecture may one day be solved, the argument applies to similar unsolved problems.

To Brouwer, the law of the excluded middle is tantamount to assuming that every mathematical problem has a solution.

We can use ƒ and g together to compute as close a rational approximation as we like to the real number they represent.

In fact, the standard constructive interpretation of the mathematical statement is precisely the existence of the function computing the modulus of convergence.

Thus the difference between the two definitions of real numbers can be thought of as the difference in the interpretation of the statement "for all... there exists..." This then opens the question as to what sort of function from a countable set to a countable set, such as f and g above, can actually be constructed.

Constructions can be defined as broadly as free choice sequences, which is the intuitionistic view, or as narrowly as algorithms (or more technically, the computable functions), or even left unspecified.

If, for instance, the algorithmic view is taken, then the reals as constructed here are essentially what classically would be called the computable numbers.

To take the algorithmic interpretation above would seem at odds with classical notions of cardinality.

And yet Cantor's diagonal argument here shows that real numbers have uncountable cardinality.

One trivial meaning of "constructive", used informally by mathematicians, is "provable in ZF set theory without the axiom of choice."

The choice principles that intuitionists accept do not imply the law of the excluded middle.

Traditionally, some mathematicians have been suspicious, if not antagonistic, towards mathematical constructivism, largely because of limitations they believed it to pose for constructive analysis.

These views were forcefully expressed by David Hilbert in 1928, when he wrote in Grundlagen der Mathematik, "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists".

[citation needed] For example, constructive proofs in analysis may ensure witness extraction, in such a way that working within the constraints of the constructive methods may make finding witnesses to theories easier than using classical methods.

[citation needed] Applications for constructive mathematics have also been found in typed lambda calculi, topos theory and categorical logic, which are notable subjects in foundational mathematics and computer science.

[citation needed] Physicist Lee Smolin writes in Three Roads to Quantum Gravity that topos theory is "the right form of logic for cosmology" (page 30) and "In its first forms it was called 'intuitionistic logic'" (page 31).