|
A general answer to this question is that constructive mathematics is mathematics which, at least in principle, can be implemented on a computer.
There are at least two ways of developing mathematics constructively. In the first way one uses classical (that is, traditional) logic. Unfortunately, that logic allows us to prove theorems that no computer can implement, so in order to do things constructively, we have to work within a strict algorithmic framework such as recursive function theory [22] or Weihrauch�s Type Two Effectivity theory [35]. This can make the resulting mathematics appear rather hard to read and certainly different from normal analysis, algebra, or the like.
The second way of approaching constructivity is to replace classical logic by intuitionistic logic, which neatly captures the proof processes used when you work in a rigorously computational manner. This way has the advantage that, once you get used to a logic which does not allow, for example, the application of the law of excluded middle (LEM)
P∨�P,
you find yourself working in the style of a traditional algebraist, analyst, and so on, without referring continually to a special algorithmic language and symbolism.
In these comments I will use constructive mathematics (CM for short) to mean mathematics with intuitionistic logic. (Actually, we need a bit more than just a change of logic: namely, some kind of number�theoretic or set�theoretic foundation that does not conflict with that logic. One such foundation is constructive Zermelo�Fraenkel set theory [3].)
|
