Brouwer published two papers in 1918 and 1919 in German on “intuitionistic set theory”. From 1907 Brouwer rejected the principle of the excluded middle (PEM). PEM is the logical principle that the statement p . v p must always be true. The intuitionist view is that one can only state p . q when one can give either a constructive proof of p or a constructive proof of q.

A constructivist has a different view of what truth is. To say that a proposition is true simply means we can prove it by in accordance with the stringent methods they utilize. In this sense mathematics is not timeless. What is not true today may be true tomorrow.

Brouwer utilized concepts he called species, spread and choice sequence. A species is a set that has been defined by a characteristic property. A choice sequence may change over time. A spread has choice sequences as its elements. It is like a law that regulates how choice sequences are constructed. Brouwer has a concept of the continuum that is like that of Aristotle.

Brouwer defined a function to be the assignment of values to the elements of a spread. For Brouwer the function f(x) = 0 for x < 0 and =1 otherwise is not a well defined function.

The rejection of PEM also has the effect that intuitionistic negation and differs from classical negation. And intuitionistic arithmetic is different from classical arithmetic.

Godel and Gentzen were able to establish a correspondence between classical arithmetic and intuitionistic arithmetic.

In the 1920’s it became more and more clear that intuitionistic analysis was extremely complicated and foreign. Weyl initially supported intuitionism but eventually abandoned it. The Hilbert program approach suggested another way of rehabilitating classical mathematics.

Hilbert’s program, 1928, was an attempt to “eliminate from the world once and for all the skeptical doubts” of the acceptability of the classical ideas of mathematics. “The main goal was to establish, by means of syntactic consistency proofs, the logical acceptability of the principles and modes of inference of modern mathematics. Axiomatics, logic and formalization made it possible to study mathematical theories from a purely mathematical standpoint (hence the name metamathematics), and Hilbert hoped to establish the consistency of the theories by employing very weak means.” Hilbert “hoped to answer all the criticism of Weyl and Brower, and thereby justify set theory, the classical theory of real numbers, classical analysis, and of course classical logic with its PEM (the basis for indirect proofs by reducto ad absurdum).”

Hilbert realized that when theories are formalized any proof becomes a finite combinatorial object.

The theroies were also hoped to be complete in the sense that they would allow the derivation of all the relevant results. However, Gödel showed this to be impossible.

Hilbert’s theory proceeded gradually from weak theories to stronger theories. The word formalism to describe this theory came from formalizing each mathematical theory and formally studying its proof structure. Hilbert himself understood and valued the informal mathematical statements as well as the formal ones.

Hilbert and Brouwer were at odds and Hilbert eventually had Brouwer removed from the editorial board of Mathematische Annalen. Albert Einstein was slightly involved in this scuffle. Brouwer stopped being involved and the crisis slowly abated.

In 1931 Gödel proved that systems like axiomatic set theory and Dedekind-Peano arithmetic are incomplete. That is there exist propositions in the system such that neither the proposition or the negative of the proposition is provable. This is published in Monatshefte Fr Mathematik and Physik.

Gödel’s second theorem showed that it is impossible to establish the consistency of the systems that the first theorem dealt with by any proof that can be codified within them. Mathematics has continued to develop in light of Gödel’s results.