Differences between constructivism and formalism

Question

What are the main differences between the formalism and constructivism in mathematics? Is there some theorem or axiom valid in formalism which isn't valid in constructivism and vice versa? Is the constructivism still valid after the Godel theorems or these theorems affected only the formalistic way of thinking mathematics? Thanks.

Answer 1

Usually when one speaks of these schools one has in mind Hilbert for the Formalist school and Brouwer for the Intuitionist school. Two points should be kept in mind:

(1) Hilbert's Formalist school has little to do with a "formalistic way of thinking mathematics". On the contrary, Hilbert is on record as affirming the central importance of meaning in mathematics. What Hilbert tried to is find metamathematical "finitist" ways of justifying mathematical procedures that would provide a solid foundation for mathematics.

(2) Brouwer's Intuitionist school is mainly characterized by the rejection of a logical principle called the Law of Excluded Middle (LEM). This is the main ingredient in what is known as the proof by contradiction meaning that the correctness of a proposition P is deduced from showing that "not-P" leads to a contradiction, or in formulas $\neg\neg P\implies P$. Bishop's Constructivism has a somewhat different set of emphases as compared to Brouwer's school, but the main feature is also the rejection of LEM.

Brouwer famously announced that every function is continuous. What this means, roughly, is that no discontinuous function can be constructed to the degree of explicitness required by Constructive mathematics.

Classical theorems like the Extreme Value Theorem are not true if one works in intuitionistic logic.