• View
• Edit
• History
• Print

ConstructiveMathematics

Constructive mathematics is dedicated to the principle that (in some sense) you have to be able to actually find the things you claim exist. This involves significant changes in the way one does mathematics, and the resulting theorems are subtly different from those of the more mainstream "classical" mathematics.

Classical mathematics uses proof methods that, almost unnoticeably, prove the existence of things that cannot be found. But so endemic are those methods of reasoning, that it is a major wrench for a classical mathematician to change his manner of thinking to be able to work constructively. Yet if he does so, he will find a mathematics of great elegance and clarity. I hope to present some of this beauty in these pages.

Constructivists have different terminology from the classical mathematicians. Sometime this manifest itself as new words for things that are of little importance classically; sometimes it involves subtly different meaning for shared words. Indeed, it is not possible to avoid meaning shifts entirely, because constructive logic is different from classical. When your methods of reasoning and understanding are changed, meaning is inevitably affected.

Constructivists have different methods of reasoning from classical mathematicians. The most noticeable difference is that most forms of proof by contradiction are outlawed. In a proof by contradiction, one assumes the negation of what one is trying to prove, and then derives a contradiction from that. Having shown that the negation cannot be true, one concludes that what one was trying to prove is true. If what one was trying to prove is that something exists, you have the illusion of its existence without the bother of actually having to find such a thing.

This does not mean that all contradiction is useless. In particular, contradiction is useful to prove a falsehood. It can be used as the definition of negation. Thus if you derive a contradiction from the assumption p, you can conclude \neg p; likewise, if you assume \neg p and derive a contradiction, you can conclude that \neg \neg p. But \neg \neg p is treated as distinct from p -- it is treated as a failure to disprove p rather than a success at proving p.