Formalism (mathematics) - Hilbert's Formalism

Hilbert's Formalism

A major early proponent of formalism was David Hilbert, whose program was intended to be a complete and consistent axiomatization of all of mathematics. Hilbert aimed to show the consistency of mathematical systems from the assumption that the "finitary arithmetic" (a subsystem of the usual arithmetic of the positive integers, chosen to be philosophically uncontroversial) was consistent (i.e. no contradictions can be derived from the system).

The way that Hilbert tried to show that an axiomatic system was consistent was by formalizing it using a particular language (Snapper, 1979). In order to formalize an axiomatic system, you must first choose a language in which you can express and perform operations within that system. This language must include five components:

• It must include variables such as x, which can stand for some number.
• It must have quantifiers such as the symbol for the existence of an object.
• It must include equality.
• It must include connectives such as ↔ for "if and only if."
• It must include certain undefined terms called parameters. For geometry, these undefined terms might be something like a point or a line, which we still choose symbols for.

Once we choose this language, Hilbert thought that we could prove all theorems within any axiomatic system using nothing more than the axioms themselves and the chosen formal language.

Gödel's conclusion in his incompleteness theorems was that you cannot prove consistency within any axiomatic system rich enough to include classical arithmetic. On the one hand, you must use only the formal language chosen to formalize this axiomatic system; on the other hand, it is impossible to prove the consistency of this language in itself (Snapper, 1979). Hilbert was originally frustrated by Gödel's work because it shattered his life's goal to completely formalize everything in number theory (Reid and Weyl, 1970). However, Gödel did not feel that he contradicted everything about Hilbert's formalist point of view. After Gödel published his work, it became apparent that proof theory still had some use, the only difference is that it could not be used to prove the consistency of all of number theory as Hilbert had hoped (Reid and Weyl, 1970). Present-day formalists use proof theory to further our understanding in mathematics, but perhaps because of Gödel's work, they make no claims about semantic meaning in the work that they do with mathematics. Proofs are simply the manipulation of symbols in our formal language starting from certain rules that we call axioms.

It is important to note that Hilbert is not considered a strict formalist as formalism is defined today. He thought there was some meaning and truth in mathematics, which is precisely why he was trying to prove the consistency of number theory. If number theory turned out to be consistent, then there had to be some sort of truth in it (Goodman, 1979). Strict formalists consider mathematics apart from its semantic meaning. They view mathematics as pure syntax: the manipulation of symbols according to certain rules. They then attempt to show that this set of rules is consistent, much like Hilbert attempted to do (Goodman, 1979). Formalists currently believe that computerized algorithms will eventually take over the task of constructing proofs. Computers will replace humans in all mathematical activities, such as checking to see if a proof is correct or not (Goodman, 1979).

Hilbert was initially a deductivist, but, he considered certain metamathematical methods to yield intrinsically meaningful results and was a realist with respect to the finitary arithmetic. Later, he held the opinion that there was no other meaningful mathematics whatsoever, regardless of interpretation.