In the first, geometric stage of Hilbert’s formalism, his view was that a system of axioms does not express truths particular to a given subject matter but rather expresses a network of logical relations that can (and, ideally, will) be common to other subject matters.
The formalism of Hilbert’s arithmetical period extended this view by emptying even the logical terms of contentual meaning. They were treated purely as ideal elements whose purpose was to secure a simple and perspicuous logic for arithmetical reasoning – specifically, a logic preserving the classical patterns of logical inference. Hilbert believed, however, that the use of ideal elements should not lead to inconsistencies. He thus undertook to prove the consistency of ideal arithmetic with its contentual or finitary counterpart and to do so by purely finitary means.
In this, ‘Hilbert’s programme’, Hilbert and his followers were unsuccessful. Work published by Kurt Gödel in 1931 suggested that such failure was perhaps inevitable. In his second incompleteness theorem, Gödel showed that for any consistent formal axiomatic system T strong enough to formalize what was traditionally regarded as finitary reasoning, it is possible to define a sentence that expresses the consistency of T, and is not provable in T. From this it has generally been concluded that the consistency of even the ideal arithmetic of the natural numbers is not finitarily provable and that Hilbert’s programme must therefore fail.
Despite problematic elements in this reasoning, post-Gödelian work on Hilbert’s programme has generally accepted it and attempted to minimize its effects by proposing various modifications of Hilbert’s programme. These have generally taken one of three forms: attempts to extend Hilbert’s finitism to stronger constructivist bases capable of proving more than is provable by strictly finitary means; attempts to show that for a significant family of ideal systems there are ways of ‘reducing’ their consistency problems to those of theories possessing more elementary (if not altogether finitary) justifications; and attempts by the so-called ‘reverse mathematics’ school to show that the traditionally identified ideal theories do not need to be as strong as they are in order to serve their mathematical purposes. They can therefore be reduced to weaker theories whose consistency problems are more amenable to constructivist (indeed, finitist) treatment.
The monotone completeness theorem in constructive reverse mathematics
