## 1. Historical development of Hilbert's Program


### 1.1 Early work on foundations



Hilbert's work on the foundations of mathematics has its roots
in his work on geometry of the 1890s, culminating in his influential
textbook *Foundations of Geometry*
 (1899)
 (see
 19th Century Geometry). Hilbert
believed that the proper way to develop any scientific subject
rigorously required an axiomatic approach. In providing an axiomatic
treatment, the theory would be developed independently of any need for
intuition, and it would facilitate an analysis of the logical
relationships between the basic concepts and the axioms. For Hilbert,
the investigation of the independence and, above all, consistency of
the axioms is of basic importance for an axiomatic treatment. For the
axioms of geometry, consistency can be proved by providing an
interpretation of the system in the real plane, and thus, the
consistency of geometry is reduced to the consistency of analysis. The
foundation of analysis, of course, itself requires an axiomatization
and a consistency proof. Hilbert provided such an axiomatization in
(1900b), but it became clear very quickly
that the consistency of analysis faced significant difficulties, in
particular because the favored way of providing a foundation for
analysis in Dedekind's work relied on dubious assumptions akin
to to those that lead to the paradoxes of set theory and
 Russell's Paradox
 in Frege's foundation of arithmetic.



Hilbert thus realized that a *direct* consistency proof of
analysis, i.e., one not based on reduction to another theory, was
needed. He proposed the problem of finding such a proof as the second
of his 23 mathematical problems in his address to the International
Congress of Mathematicians in 1900
 (1900a)
 and presented a sketch of such a proof in his Heidelberg talk
 (1905).
 Several factors delayed the further development of Hilbert's
foundational program. One was perhaps the criticism of
 Poincare (1906)
 against what he saw as a viciously circular use of induction in
Hilbert's sketched consistency proof (see
 Steiner 1975,
 Appendix). Hilbert also realized that axiomatic investigations
required a well worked-out logical formalism. At the time he relied on
a conception of logic based on the algebraic tradition, in particular,
on Schroder's work, which was not particularly suited as a
formalism for the axiomatization of mathematics. (See
 Peckhaus 1990
 on the early development of Hilbert's Program.)


### 1.2 The influence of *Principia Mathematica*



The publication of Russell and Whitehead's
 *Principia Mathematica*
 provided the required logical basis for a renewed attack on
foundational issues. Beginning in 1914, Hilbert's student
Heinrich Behmann and others studied the system of *Principia*
(see
 Mancosu 1999
 on Behmann's role in Hilbert's school). Hilbert himself
returned to work on foundational issues in 1917. In September 1917, he
delivered an address to the Swiss Mathematical Society entitled
"Axiomatic Thought"
 (1918a).
 It is his first published contribution to mathematical foundations
since 1905. In it, he again emphasizes the requirement of consistency
proofs for axiomatic systems: "The chief requirement of the
theory of axioms must go farther [than merely avoiding known
paradoxes], namely, to show that within every field of knowledge
contradictions based on the underlying axiom-system are *absolutely
impossible*." He poses the proof of the consistency of
arithmetic (and of set theory) again as the main open problems. In
both these cases, there seems to be nothing more fundamental available
to which the consistency could be reduced other than logic itself. And
Hilbert then thought that the problem had essentially been solved by
Russell's work in *Principia*. Nevertheless, other
fundamental problems of axiomatics remained unsolved, including the
problem of the "decidability of every mathematical
question," which also traces back to Hilbert's 1900
address.



These unresolved problems of axiomatics led Hilbert to devote
significant effort to work on logic in the following years. In 1917,
Paul Bernays joined him as his assistant in Gottingen. In a
series of courses from 1917-1921, Hilbert, with the assistance
of Bernays and Behmann, made significant new contributions to formal
logic. The course from 1917
 (Hilbert, 1918b),
 in particular, contains a sophisticated development of first-order
logic, and forms the basis of Hilbert and Ackermann's textbook
*Principles of Theoretical Logic*
 (1928)
 (see
 Ewald and Sieg 2013,
 Sieg 1999, and Zach
 1999,
 2003).


### 1.3 Finitism and the quest for consistency proofs



Within the next few years, however, Hilbert came to reject
Russell's logicist solution to the consistency problem for
arithmetic. At the same time,
 Brouwer's
 intuitionistic mathematics gained currency. In particular,
Hilbert's former student Hermann Weyl converted to intuitionism.
Weyl's paper "The new foundational crisis in
mathematics"
 (1921)
 was answered by Hilbert in three talks in Hamburg in the Summer of
1921
 (1922b).
 Here, Hilbert presented his own proposal for a solution to the
problem of the foundation of mathematics. This proposal incorporated
Hilbert's ideas from 1904 regarding direct consistency proofs,
his conception of axiomatic systems, and also the technical
developments in the axiomatization of mathematics in the work of
Russell as well as the further developments carried out by him and his
collaborators. What was new was the way in which Hilbert wanted to
imbue his consistency project with the philosophical significance
necessary to answer Brouwer and Weyl's criticisms: the finitary
point of view.



According to Hilbert, there is a privileged part of mathematics,
contentual elementary number theory, which relies only on a
"purely intuitive basis of concrete signs." Whereas the
operating with abstract concepts was considered "inadequate and
uncertain," there is a realm of



> 
> extra-logical discrete objects, which exist intuitively as immediate
> experience before all thought. If logical inference is to be certain,
> then these objects must be capable of being completely surveyed in all
> their parts, and their presentation, their difference, their
> succession (like the objects themselves) must exist for us
> immediately, intuitively, as something which cannot be reduced to
> something else.
>  (Hilbert 1922b,
>  202; the passage is repeated almost verbatim in
>  Hilbert 1926,
>  376,
>  Hilbert 1928,
>  464, and
>  Hilbert 1931b,
>  267)
> 



These objects were, for Hilbert, *signs*. The domain of
contentual number theory consists in the finitary numerals, i.e.,
sequences of strokes. These have no meaning, i.e., they do not stand
for abstract objects, but they can be operated on (e.g., concatenated)
and compared. Knowledge of their properties and relations is intuitive
and unmediated by logical inference. Contentual number theory
developed this way is secure, according to Hilbert: no contradictions
can arise simply because there is no logical structure in the
propositions of contentual number theory.



The intuitive-contentual operations with signs forms the basis of
Hilbert's metamathematics. Just as contentual number theory
operates with sequences of strokes, so metamathematics operates with
sequences of symbols (formulas, proofs). Formulas and proofs can be
syntactically manipulated, and the properties and relationships of
formulas and proofs are similarly based in a logic-free intuitive
capacity which guarantees certainty of knowledge about formulas and
proofs arrived at by such syntactic operations. Mathematics itself,
however, operates with abstract concepts, e.g., quantifiers, sets,
functions, and uses logical inference based on principles such as
mathematical induction or the principle of the excluded middle. These
"concept-formations" and modes of reasoning had been
criticized by Brouwer and others on grounds that they presuppose
infinite totalities as given, or that they involve impredicative
definitions (which were considered by the critics as viciously
circular). Hilbert's aim was to justify their use. To this end,
he pointed out that they can be formalized in axiomatic systems (such
as that of *Principia* or those developed by Hilbert himself),
and mathematical propositions and proofs thus turn into formulas and
derivations from axioms according to strictly circumscribed rules of
derivation. Mathematics, so Hilbert, "becomes an inventory of
provable formulas." In this way the proofs of mathematics are
subject to metamathematical, contentual investigation. The goal of
Hilbert's program is then to give a contentual, metamathematical
proof that there can be no derivation of a contradiction, i.e., no
formal derivations of a formula \(A\) and of its negation \(\neg
A\).



This sketch of the aims of the program was fleshed out by Hilbert and
his collaborators in the following 10 years. On the conceptual side,
the finite standpoint and the strategy for a consistency proof were
elaborated by
 Hilbert (1928);
 Hilbert (1923);
 Hilbert (1926)
 and
 Bernays (1928b);
 Bernays (1922);
 Bernays (1930),
 of which Hilbert's article "On the infinite"
 (1926)
 provides the most detailed elaboration of the finitary standpoint. In
addition to Hilbert and Bernays, a number of other people were
involved in technical work on the program. In lectures given in
Gottingen
 (Hilbert and Bernays, 1923;
 Hilbert, 1922a), Hilbert and Bernays developed the
 \(\varepsilon\)-calculus
 as their definitive formalism for axiom systems for arithmetic and
analysis. Hilbert there also presented his approach to giving
consistency proofs using his so-called \(\varepsilon\)-substitution
method.
 Ackermann (1924)
 attempted to extend Hilbert's idea to a system of analysis. The
proof was, however, erroneous (see
 Zach 2003).
 John von Neumann, then visiting Gottingen, gave a corrected
consistency proof for a system of the \(\varepsilon\)-formalism
(which, however, did not include the induction axiom) in 1925
(published in
 1927).
 Building on von Neumann's work, Ackermann devised a new
\(\varepsilon\)-substitution procedure which he communicated to
Bernays (see
 Bernays 1928b).
 In his address "Problems of the grounding of mathematics"
to the International Congress of Mathematicians in Bologna in 1928
 (1929),
 Hilbert optimistically claimed that the work of Ackermann and von
Neumann had established the consistency of number theory and that the
proof for analysis had already been carried out by Ackermann "to
the extent that the only remaining task consists in the proof of an
elementary finiteness theorem that is purely arithmetical."


### 1.4 The impact of Godel's Incompleteness Theorems



Godel's incompleteness theorems
 showed that Hilbert's optimism was undue. In September 1930,
Kurt Godel announced his first incompleteness theorem at a
conference in Konigsberg. Von Neumann, who was in the audience,
immediately recognized the significance of Godel's result
for Hilbert's program. Shortly after the conference he wrote to
Godel, telling him that he had found a corollary to
Godel's result. Godel had found the same result
already independently: the second incompleteness theorem, asserting
that the system of *Principia* does not prove the formalization
of the claim that the system of *Principia* is consistent
(provided it is). All the methods of finitary reasoning used in the
consistency proofs up till then were believed to be formalizable in
*Principia*, however. Hence, if the consistency of
*Principia* were provable by the methods used in
Ackermann's proofs, it should be possible to formalize this
proof in *Principia*; but this is what the second
incompleteness theorem states is impossible. Bernays also realized the
importance of Godel's results immediately after he studied
Godel's paper in January 1931, writing to Godel that
(under the assumption that finitary reasoning can be formalized in
*Principia*) the incompleteness theorem shows that a finitary
consistency proof of *Principia* is impossible. Shortly
thereafter, von Neumann showed that Ackermann's consistency
proof is flawed and provided a counterexample to the proposed
\(\varepsilon\)-substitution procedure (see
 Zach 2003).



In
 (1936),
 Gentzen published a consistency proof of first-order Peano Arithmetic
(\(\PA\)). As Godel had shown was necessary, Gentzen's
proof used methods that could not be formalized in \(\PA\) itself,
namely, transfinite induction along the ordinal \(\varepsilon\_0\).
Gentzen's work marks the beginning of post-Godelian proof
theory and work on Relativized Hilbert Programs. Proof theory in the
tradition of Gentzen has analyzed axiomatic systems according to what
extensions of the finitary standpoint are necessary to prove their
consistency. Usually, the consistency strength of systems has been
measured by the system's *proof-theoretic ordinal*, i.e.,
the ordinal transfinite induction along which suffices to prove
consistency. In the case of \(\PA\), that ordinal is
\(\varepsilon\_0\). (For further discussion, see the entries on
 proof theory
 and
 the development of proof theory.)


## 2. The Finitary Point of View



The cornerstone of Hilbert's philosophy of mathematics, and the
substantially new aspect of his foundational thought from
 1922b
 onward, consisted in what he called the finitary standpoint. This
methodological standpoint consists in a restriction of mathematical
thought to those objects which are "intuitively present as
immediate experience prior to all thought," and to those
operations on and methods of reasoning about such objects which do not
require the introduction of abstract concepts, in particular, without
appeal to completed infinite totalities.



There are several basic and interrelated issues in understanding
Hilbert's finitary standpoint:


1. What are the objects of finitary reasoning?
2. What are the finitarily meaningful propositions?
3. What are the finitarily acceptable methods of construction and
reasoning?


### 2.1 Finitary objects and finitist epistemology



Hilbert characterized the domain of finitary reasoning in a well-known
paragraph which appears in roughly the same formulation in all of
Hilbert's more philosophical papers from the 1920s
 (1931b;
 1922b;
 1928;
 1926):



> 
> [A]s a condition for the use of logical inferences and the performance
> of logical operations, something must already be given to our faculty
> of representation, certain extralogical concrete objects that are
> intuitively present as immediate experience prior to all thought. If
> logical inference is to be reliable, it must be possible to survey
> these objects completely in all their parts, and the fact that they
> occur, that they differ from one another, and that they follow each
> other, or are concatenated, is immediately given intuitively, together
> with the objects, as something that can neither be reduced to anything
> else nor requires reduction. This is the basic philosophical position
> that I consider requisite for mathematics and, in general, for all
> scientific thinking, understanding, and communication.
>  (Hilbert, 1926,
>  376)
> 



These objects are, for Hilbert, the *signs*. For the domain of
contentual number theory, the signs in question are numerals such
as



> 
> 1, 11, 111, 11111
> 



The question of how exactly Hilbert understood the numerals is
difficult to answer. They are not physical objects (actual strokes on
paper, for instance), since it must always be possible to extend a
numeral by adding another stroke (and, as Hilbert also argues in
"On the infinite"
 (1926),
 it is doubtful that the physical universe is infinite). According to
 Hilbert (1922b, 202),
 their "shape can be generally and certainly recognized by
us--independently of space and time, of the special conditions of
the production of the sign, and of the insignificant differences in
the finished product." They are not mental constructions, since
their properties are objective, yet their existence is dependent on
their intuitive construction (see
 Bernays 1923,
 226). What is clear in any case is that they are logically primitive,
i.e., they are neither concepts (as Frege's numbers are) nor
sets. What is important here is not primarily their metaphysical
status (abstract versus concrete in the current sense of these terms),
but that they do not enter into logical relations, e.g., they cannot
be predicated of anything. In Bernays's most mature
presentations of finitism
 (Hilbert and Bernays, 1939;
 Bernays, 1930), 
the objects of finitism are characterized as *formal
objects* which are recursively generated by a process of
repetition; the stroke symbols are then concrete representations of
these formal objects.



The question of what Hilbert thought the epistemological status of the
objects of finitism was is equally difficult. In order to carry out
the task of providing a secure foundation for infinitistic
mathematics, access to finitary objects must be immediate and certain.
Hilbert's philosophical background was broadly Kantian, as was
Bernays's, who was closely affiliated with the neo-Kantian
school of philosophy around Leonard Nelson in Gottingen.
Hilbert's characterization of finitism often refers to Kantian
intuition, and the objects of finitism as objects given intuitively.
Indeed, in Kant's epistemology, immediacy is a defining
characteristic of intuitive knowledge. The question is, what kind of
intuition is at play?
 Mancosu (1998b)
 identifies a shift in this regard. He argues that whereas the
intuition involved in Hilbert's early papers was a kind of
perceptual intuition, in later writings (e.g.,
 Bernays 1928a)
 it is identified as a form of pure intuition in the Kantian sense.
However, at roughly the same time
 Hilbert (1928, 469)
 still identifies the kind of intuition at play as perceptual. In
 (1931b,
 266-267), Hilbert sees the finite mode of thought as a separate
source of *a priori* knowledge in addition to pure intuition
(e.g., of space) and reason, claiming that he has "recognized
and characterized the third source of knowledge that accompanies
experience and logic." Both Bernays and Hilbert justify finitary
knowledge in broadly Kantian terms (without however going so far as to
provide a transcendental deduction), characterizing finitary reasoning
as the kind of reasoning that underlies all mathematical, and indeed,
scientific, thinking, and without which such thought would be
impossible. (See
 Kitcher 1976
 and
 Parsons 1998
 on the epistemology of finitism,
 Patton 2014
 for historical and philosophical context of Hilbert's theory of
signs, and
 Eder (forthcoming)
 specifically on the ensuing debate with the German philosopher Aloys
Muller.)


### 2.2 Finitarily meaningful propositions and finitary reasoning



The most basic judgments about finitary numerals are those about
equality and inequality. In addition, the finite standpoint allows
operations on finitary objects. Here the most basic is that of
concatenation. The concatenation of the numerals 11 and 111 is
communicated as "\(2 + 3\)," and the statement that 11
concatenated with 111 results in the same numeral as 111 concatenated
with 11 by "\(2 + 3 = 3 + 2\)." In actual proof-theoretic
practice, as well as explicitly in
 (Hilbert and Bernays, 1934;
 Bernays, 1930), these basic operations 
are generalized to operations
defined by recursion, paradigmatically, primitive recursion, e.g.,
multiplication and exponentiation (see
 Parsons 1998
 for philosophical difficulties in relation to exponentiation and
 2007
 for an extended discussion of intuitive mathematics and finitism).
Similarly, finitary judgments may involve not just equality or
inequality but also basic decidable properties, such as "is a
prime." This is finitarily acceptable as long as the
characteristic function of such a property is itself finitary: For
instance, the operation which transforms a numeral to 1 if it is prime
and 11 otherwise can be defined by primitive recursion and is hence
finitary. Such finitary propositions may be combined by the usual
logical operations of conjunction, disjunction, negation, but also
bounded quantification.
 (Hilbert, 1926)
 gives the example of the proposition that "there is a prime
number between \(p + 1\) and \(p! + 1\)" where \(p\) is a
certain large prime. This statement is finitarily acceptable since it
"serves merely to abbreviate the proposition" that either
\(p + 1\) or \(p + 2\) or \(p + 3\) or ... or \(p! + 1\) is a
prime.



The problematic finitary propositions are those that express general
facts about numerals such as that, for any given numeral \(n, 1+n =
n+1\). It is problematic because, as Hilbert puts it, it "is
from the finitist point of view *incapable of being
negated*"
 (1926,
 378). By this he means that the contradictory proposition that there
is a numeral \(n\) for which \(1+n \ne n+1\) is not finitarily
meaningful. "One cannot, after all, try out all numbers"
 (1928,
 470). For the same reason, a finitary general proposition is not to
be understood as an infinite conjunction but "only as a
hypothetical judgment that comes to assert something when a numeral is
given" (ibid.). Even though they are problematic in this sense,
general finitary statements are of particular importance to
Hilbert's proof theory, since the statement of consistency of a
formal system \(S\) is of such a general form: for any given sequence
of formulas \(P, P\) is not a derivation of a contradiction in
\(S\).


### 2.3 Finitary operations and finitary proof



Of crucial importance to both an understanding of finitism and of
Hilbert's proof theory is the question of what operations and
what principles of proof should be allowed from the finitist
standpoint. That a general answer is necessary is clear from the
demands of Hilbert's proof theory, i.e., it is not to be
expected that given a formal system of mathematics (or even a single
sequence of formulas) one can "see" that it is consistent
(or that it cannot be a genuine derivation of an inconsistency) the
way we can see, e.g., that \(11 + 111 = 111 + 11\). What is required
for a consistency proof is an operation which, given a formal
derivation, transforms such a derivation into one of a special form,
plus proofs that the operation in fact does this and that proofs of
the special kind cannot be proofs of an inconsistency. To count as a
finitary consistency proof, the operation itself must be acceptable
from the finitist standpoint, and the proofs required must use only
finitarily acceptable principles.



Hilbert never gave a general account of which operations and methods
of proof are acceptable from the finitist standpoint, but only
examples of operations and methods of inference in contentual finitary
number theory which he accepted as finitary. Contentual induction was
accepted in its application to finitary statements of the
hypothetical, general kind explicitly in
 Hilbert (1922b).
 He
 (1923,
 1139) said that intuitive thought "includes recursion and
intuitive induction for finite existing totalities," and used
exponentiation in an example in
 1928.
 Bernays (1930) explained 
how exponentiation may be understood as a
finitary operation on numerals.
 Hilbert and Bernays (1934)
 give the only general account of finitary contentual number theory;
according to it, operations defined by primitive recursion and proofs
using induction are finitarily acceptable. All of these methods can be
formalized in a system known as primitive recursive arithmetic
(\(\PRA\)), which allows definitions of functions by primitive
recursion and induction on quantifier-free formulas (ibid.). However,
neither Hilbert nor Bernays ever claimed that *only* primitive
recursive operations count as finitary, and they in fact did use some
non-primitive recursive methods in ostensibly finitary consistency
proofs already in 1923 (see
 Tait 2002
 and
 Zach 2003).



The more interesting conceptual issue is which operations
*should* be considered as finitary. Since Hilbert was less than
completely clear on what the finitary standpoint consists in, there is
some leeway in setting up the constraints, epistemological and
otherwise, an analysis of finitist operation and proof must fulfill.
Hilbert characterized (see above) the objects of finitary number
theory as "intuitively given," as "surveyable in all
their parts," and said that their having basic properties must
"exist intuitively" for us.
 Bernays (1922, 216)
 suggests that in finitary mathematics, only "primitive
intuitive cognitions come into play," and uses the term
"point of view of intuitive evidence" in connection with
finitism
 1930,
 250. This characterization of finitism as primarily to do with
*intuition* and intuitive knowledge has been emphasized in
particular by
 (Parsons, 1998)
 who argues that what can count as finitary on this understanding is
not more than those arithmetical operations that can be defined from
addition and multiplication using bounded recursion. In particular,
according to him, exponentiation and general primitive recursion are
not finitarily acceptable.



The thesis that finitism coincides with primitive recursive reasoning
has received a forceful defense by
 (Tait 1981;
 see also
 2002,
 2005b,
 2019).
 Tait, in contrast to Parsons, rejects the aspect of representability
in intuition as the hallmark of the finitary; instead he takes
finitary reasoning to be "a minimal kind of reasoning
presupposed by all non-trivial mathematical reasoning about
numbers." and analyzes finitary operations and methods of proof
as those that are implicit in the very notion of number as the form of
a finite sequence. This analysis of finitism is supported by
Hilbert's contention that finitary reasoning is a precondition
for logical and mathematical, indeed any scientific thinking
 Hilbert (1931b, 267).
 Since finitary reasoning is that part of mathematics which is
presupposed by all non-trivial reasoning about numbers, it is, so
Tait, "indubitable" in a Cartesian sense, and this
indubitability as all that would be required of finitary reasoning to
provide the epistemological grounding of mathematics Hilbert intended
it for.



Another interesting analysis of finitary proof, which, however, does
not provide as detailed a philosophical justification, was proposed by
 Kreisel (1960).
 It yields the result that exactly those functions are finitary which
can be proved to be total in first-order arithmetic \(\PA\). It is
based on the proof-theoretic concept of a reflection principle; see
 Zach (2006)
 for more detail and
 Dean (2015)
 for an analysis.
 Kreisel (1970, Section 3.5)
 provides another analysis by focusing on what is
"visualizable." The result is the same: finitary
provability turns out to be coextensive with provability in
\(\PA\).



Tait's technical analysis yields that the finitistic functions
are exactly the primitive recursive ones, and the finitistic
number-theoretic truths are exactly those provable in the theory of
primitive recursive arithmetic \(\PRA.\) It is important to stress
that this analysis is not carried out from within the finitist
viewpoint itself. Since the general notions of "function"
and "proof" are not themselves finitary, the finitist is
unable to make sense of Tait's thesis that everything provable
in \(\PRA\) is finitistically true. According to Tait, a proper
analysis of finitistic provability must not assume that finitism
itself has access to such non-finitistic notions. Kreisel's
approach and some criticisms of Tait that rely on reflection
principles or \(\omega\)-rules run afoul of this requirement (see Tait
 2002,
 2005b). On the other hand, one could argue that \(\PRA\) is too
strong a theory to count as a formalization of what is
"presupposed by all non-trivial mathematical reasoning about
numbers": there are weaker but non-trivial theories which are
related to smaller classes of functions than the primitive recursive
ones, such as \(\PV\) and \(\EA\), related to the polynomial-time and
Kalmar-elementary functions respectively (see
 Avigad 2003
 on how much mathematics can be carried out in \(\EA)\). Using an
analysis along the same lines as Tait's,
 Ganea (2010)
 has arrived at the corresponding class of Kalmar-elementary functions
as those that are finitistic. See also
 Incurvati (2019)
 for further analysis of different notions of finitism.


## 3. Formalism, reductionism and instrumentalism



Weyl (1925)
 was a conciliatory reaction to Hilbert's proposal in
 1922b
 and
 1923,
 which nevertheless contained some important criticisms. Weyl
described Hilbert's project as replacing contentual mathematics
by a meaningless game of formulas. He noted that Hilbert wanted to
"secure not *truth*, but the *consistency* of
analysis" and suggested a criticism that echoes an earlier one
by Frege: Why should we take consistency of a formal system of
mathematics as a reason to believe in the truth of the pre-formal
mathematics it codifies? Is Hilbert's meaningless inventory of
formulas not just "the bloodless ghost of analysis"? Weyl
suggested a solution:



> 
> [I]f mathematics is to remain a serious cultural concern, then some
> *sense* must be attached to Hilbert's game of formulae,
> and I see only one possibility of attributing it (including its
> transfinite components) an independent intellectual meaning. In
> theoretical physics we have before us the great example of a [kind of]
> knowledge of completely different character than the common or
> phenomenal knowledge that expresses purely what is given in intuition.
> While in this case every judgment has its own sense that is completely
> realizable within intuition, this is by no means the case for the
> statements of theoretical physics. In that case it is rather *the
> system as a whole* that is in question if confronted with
> experience.
>  (Weyl, 1925,
>  140)
> 



The analogy with physics is striking, and one can find similar ideas
in Hilbert's own writing--perhaps Hilbert was influenced in
this by Weyl. Although Hilbert's first proposals focused
exclusively on consistency, there is a noticeable development in
Hilbert's thinking in the direction of a general reductivist
project of a sort quite common in the philosophy of science at the
time (as was pointed out by
 Giaquinto 1983).
 In the second half of the 1920s, Hilbert replaced the consistency
program with a conservativity program: Formalized mathematics was to
be considered by analogy with theoretical physics. The ultimate
justification for the theoretical part lies in its conservativity over
"real" mathematics: whenever theoretical,
"ideal" mathematics proves a "real"
proposition, that proposition is also intuitively true. This justifies
the use of transfinite mathematics: it is not only internally
consistent, but it proves only true intuitive propositions (and indeed
all, since a formalization of intuitive mathematics is part of the
formalization of all mathematics).



In
 1926,
 Hilbert introduced a distinction between real and ideal formulas.
This distinction was not present in
 1922b
 and only hinted at in
 1923.
 In the latter, Hilbert presents first a formal system of
quantifier-free number theory about which he says that "The
provable formulae we acquire in this way all have the character of the
finite" (1139). Then the transfinite axioms (i.e., quantifiers)
are added to simplify and complete the theory (1144). Here he draws
the analogy with the method of ideal elements for the first time:
"In my proof theory, the transfinite axioms and formulae are
adjoined to the finite axioms, just as in the theory of complex
variables the imaginary elements are adjoined to the real, and just as
in geometry the ideal constructions are adjoined to the actual"
(ibid). When Hilbert, in
 1926
 explicitly introduces the notion of an ideal proposition, and in
 1928,
 when he first speaks of *real propositions* in addition to the
ideal, he is quite clear that the real part of the theory consists
only of decidable, variable-free formulas. They are supposed to be
"directly capable of verification"--akin to
propositions derived from laws of nature which can be checked by
experiment
 (1928,
 475). The new picture of the program was this: Classical mathematics
is to be formalized in a system which includes formalizations of all
the directly verifiable (by calculation) propositions of contentual
finite number theory. The consistency proof should show that all real
propositions which can be proved by ideal methods are true, i.e., can
be directly verified by finite calculation. (Actual proofs such as the
\(\varepsilon\)-substitution had always been of such a kind: provide
finitary procedures which eliminate transfinite elements from proofs
of real statements, in particular, of \(0 = 1\).) Indeed, Hilbert saw
that something stronger is true: not only does a consistency proof
establish truth of real formulas provable by ideal methods, but it
yields finitary proofs of finitary general propositions if the
corresponding free-variable formula is derivable by ideal methods
 (1928,
 474).



Hilbert suggested further restrictions on the theory in addition to
conservativity: simplicity, brevity of proofs, "economy of
thought" and mathematical productivity. The formal system of
transfinite logic is not arbitrary: "This formula game is
carried out according to certain definite rules, in which the
*technique of our thinking* is expressed. [...] The
fundamental idea of my proof theory is none other than to describe the
activity of our understanding, to make a protocol of the rules
according to which our thinking actually proceeds"
 (Hilbert 1928,
 475). When
 Weyl (1928)
 eventually turned away from intuitionism, he emphasized this
motivation of Hilbert's proof theory: not to turn mathematics
into a meaningless game of symbols, but to turn it into a theoretical
science which codifies scientific (mathematical) practice (see
 Mancosu and Ryckman 2002
 and
 Kish Bar-On 2021
 on Weyl's relationship to intuitionism and Hilbert's
formalism).



Hilbert's formalism was thus quite sophisticated: It avoided two
crucial objections: (1) If the formulas of the system are meaningless,
how can derivability in the system generate any kind of belief? (2)
Why accept the system of \(\PA\) and not any other consistent system?
Both objections are familiar from Frege; both questions are (in part)
answered by a conservativity proof for real statements. For (2),
furthermore, Hilbert has a naturalistic criterion of acceptance: we
are constrained in the choice of systems by considerations of
simplicity, fecundity, uniformity, and by what mathematicians actually
do; Weyl would add that the ultimate test of a theory would be its
usefulness in physics.



Most philosophers of mathematics writing on Hilbert have read him as
an instrumentalist (including
 Kitcher 1976,
 Resnik 1980,
 Giaquinto 1983,
 Sieg 1990, and in particular
 Detlefsen 1986)
 in that they read Hilbert's explanation that the ideal
propositions "have no meaning in themselves"
 (Hilbert, 1926,
 381) as claiming that classical mathematics is a *mere*
instrument, and that statements of transfinite mathematics have no
truth value. To the extent that this is accurate, it must be
understood as a methodological instrumentalism: A successful execution
of the proof-theoretic program would show that one could pretend
*as if* mathematics was meaningless. The analogy with physics
is therefore not: transfinite propositions have no meaning just as
propositions involving theoretical terms have no meaning, but:
transfinite propositions require no direct intuitive meaning just as
one does not have to directly see electrons in order to theorize about
them.
 Hallett (1990),
 taking into account the 19th century mathematical background from
which Hilbert came as well as published and unpublished sources from
Hilbert's entire career (in particular
 Hilbert 1992,
 the most extensive discussion of the method of ideal elements) comes
to the following conclusion:



> 
> [Hilbert's treatment of philosophical questions] is *not*
> meant as a kind of instrumentalist agnosticism about existence and
> truth and so forth. On the contrary, it is meant to provide a
> non-skeptical and positive solution to such problems, a solution
> couched in cognitively accessible terms. And, it appears, the same
> solution holds for both mathematical and physical theories. Once new
> concepts or "ideal elements" or new theoretical terms have
> been accepted, then they exist in the sense in which *any*
> theoretical entities exist.
>  (Hallett, 1990,
>  239)
> 


## 4. Hilbert's Program and Godel's incompleteness theorems



There has been some debate over the impact of
 Godel's incompleteness theorems
 on Hilbert's Program, and whether it was the first or the
second incompleteness theorem that delivered the *coup de
grace*. Undoubtedly the opinion of those most directly
involved in the developments were convinced that the theorems did have
a decisive impact. Godel announced the second incompleteness
theorem in an abstract published in October 1930: no consistency proof
of systems such as
 *Principia*,
 Zermelo-Fraenkel set theory, or the 
systems investigated by Ackermann and von
Neumann is possible by methods which can be formulated in these
systems. In the full version of his paper,
 Godel (1931)
 left open the possibility that there could be finitary methods which
are not formalizable in these systems and which would yield the
required consistency proofs. Bernays's first reaction in a
letter to Godel in January 1931 was likewise that "if, as
von Neumann does, one takes it as certain that any and every finitary
consideration may be formalized within the system \(P\)--like
you, I regard that in no way as settled--one comes to the
conclusion that a finitary demonstration of the consistency of \(P\)
is impossible"
 (Godel, 2003a,
 87).



How do Godel's theorems impact Hilbert's program?
Through a careful ("Godel"-) coding of sequences of
symbols (formulas, proofs), Godel showed that in theories \(T\)
which contain a sufficient amount of arithmetic, it is possible to
produce a formula \(Pr(x, y)\) which "says" that \(x\) is
(the code of) a proof of (the formula with code) \(y\). Specifically,
if \(\ulcorner 0 = 1\urcorner\) is the code of the formula \(0 = 1\),
then \(Con\_T = \forall x \neg Pr(x,\ulcorner 0 = 1\urcorner)\) may be
taken to "say" that \(T\) is consistent (no number is the
code of a derivation in \(T\) of \(0 = 1)\). The second incompleteness
theorem (G2) says that under certain assumptions about \(T\) and the
coding apparatus, \(T\) does not prove \(Con\_T\). Now suppose there
were a finitary consistency proof of \(T\). The methods used in such a
proof would presumably be formalizable in \(T\).
("Formalizable" means that, roughly, if the proof uses a
finitary operation \(f\) on derivations which transforms any
derivation \(D\) into a derivation \(f (D)\) of a simple form; then
there is a formula \(F(x, y)\) so that, for all derivations \(D,T
\vdash F(\ulcorner D\urcorner ,\ulcorner f (D)\urcorner)\).) The
consistency of \(T\) would be finitarily expressed as the general
hypothetical that, if \(D\) is any given sequence of symbols, \(D\) is
not a derivation in \(T\) of the formula \(0 = 1\). The formalization
of this proposition is the formula \(\neg Pr(x,\ulcorner 0 =
1\urcorner)\) in which the variable \(x\) occurs free. If there were a
finitary proof of the consistency of \(T\), its formalization would
yield a derivation in \(T\) of \(\neg Pr\_T (x,\ulcorner 0 =
1\urcorner),\) from which \(Con\_T\) can be derived in \(T\) by simple
universal generalization on \(x\). Yet, a derivation of \(Con\_T\) in
\(T\) is ruled out by G2.



As mentioned above, initially Godel and Bernays thought that the
difficulty for the consistency proof of \(\PA\) could be overcome by
employing methods which, although not formalizable in \(\PA\), are
nonetheless finitary. Whether such methods would be considered
finitary according to the original conception of finitism or
constitute an extension of the original finitist viewpoint is a matter
of debate. The new methods considered included a finitary version of
the \(\omega\)-rule proposed by Hilbert
 (1931b;
 1931a). It is fair to say, however, 
that after about 1934 it
has been almost universally accepted that the methods of proof
accepted as finitary prior to Godel's results are all
formalizable in \(\PA\). Extensions of the original finitist
standpoint have been proposed and defended on broadly finitary
grounds, e.g.,
 Gentzen (1936)
 defended the use of transfinite induction up to \(\varepsilon\_0\) in
his consistency proof for \(\PA\) as "indisputable,"
 Takeuti (1987)
 gave another defense.
 Godel (1958)
 presented another extension of the finitist standpoint; the work of
Kreisel mentioned above may be seen as another attempt to extend
finitism while retaining the spirit of Hilbert's original
conception.



A different attempt at providing a way around Godel's
second theorem for Hilbert's Program was proposed by Detlefsen
 (1986;
 2001;
 1979).
 Detlefsen presents several lines of defense, one of which is similar
to the one just described: arguing that a version of the
\(\omega\)-rule is finitarily acceptable, although not capable of
formalization (however, see
 Ignjatovic 1994).
 Detlefsen's other argument against the common interpretation of
Godel's second theorem focuses on the notion of
formalization: That the particular formalization of "\(T\) is
consistent" by Godel's formula \(Con\_T\) is not
provable does not imply that there couldn't be other formulas,
which *are* provable in \(T\), and which have as much right to
be called "formalizations of the consistency of \(T\)."
These rely on different formalizations of the provability predicate
\(Pr\_T\) than the standard ones. It is known that formalized
consistency statements are unprovable whenever the provability
predicate obeys certain general derivability conditions. Detlefsen
argues that these conditions are not necessary for a predicate to
count as a genuine provability predicate, and indeed there are
provability predicates which violate the provability conditions and
which give rise to consistency formulas which *are* provable in
their corresponding theories. These, however, depend on non-standard
conceptions of provability which would likely not have been accepted
by Hilbert (see also
 Resnik 1974,
 Auerbach 1992 and
 Steiner 1991).



Smorynski (1977)
 has argued that already the first incompleteness theorem defeats
Hilbert's Program. Hilbert's aim was not merely to show
that formalized mathematics is consistent, but to do so in a specific
way by showing that ideal mathematics can never lead to conclusions
not in accord with real mathematics. Thus, to succeed, ideal
mathematics must be *conservative* over the real part: whenever
formalized ideal mathematics proves a real formula \(P, P\) itself (or
the finitary proposition it expresses) must be finitarily provable.
For Smorynski the real formulas include not just numerical equalities
and combinations thereof, but also general formulas with free
variables but without unbounded quantifiers.



Now Godel's first incompleteness theorem (G1) states that
for any sufficiently strong, consistent formal theory \(S\) there is a
sentence \(G\_S\) which is true but not derivable in \(S\). \(G\_S\) is
a real sentence according to Smorynski's definition. Now
consider a theory \(T\) which formalizes ideal mathematics and its
subtheory \(S\) which formalizes real mathematics. \(S\) satisfies the
conditions of G1 and hence \(S\) does not derive \(G\_S\). Yet, \(T\),
being a formalization of all of mathematics (including what is
required to see that \(G\_S\) is true), does derive \(G\_S\). Hence, we
have a real statement which is provable in ideal mathematics and not
in real mathematics.



Detlefsen
 (1986,
 Appendix; see also
 1990)
 has defended Hilbert's Program against this argument as well.
Detlefsen argues that "Hilbertian" instrumentalism escapes
the argument from G1 by denying that ideal mathematics must be
conservative over the real part; all that is required is
real-soundness. Hilbertian instrumentalism requires only that the
ideal theory not prove anything which is in conflict with the real
theory; it is not required that it prove *only* real statements
which the real theory also proves.



Franks (2009)
 has provided a related defense and re-evaluation of Hilbert's
project, and
 McCarthy (2016)
 an alternative approach to the provability of consistency and G2 due
to Godel himself.
 Kripke (forthcoming)
 shows how Hilbert's own approach to consistency proofs
naturally lead to Godelian incompleteness.
 Santos et al. (forthcoming),
 expanding on work by
 Artemov (2020),
 argue that a "partial finitism" allows for consistency
proofs compatible with G2, and is in line with Hilbert's own
post-Godelian views. See also
 Schirn and Niebergall (2001)
 and
 Schirn (2019) for
 related proposals.
 Zach (2004)
 provides historical detail on the issue of conservativity and
consistency in Hilbert's program. See the entries on
 Godel
 and
 Godel's incompleteness theorem,
 as well as
 Cheng (2021),
 for further discussion on Godel's theorems and consistency
proofs.


## 5. Revised Hilbert Programs



Even if no finitary consistency proof of arithmetic can be given, the
question of finding consistency proofs is nevertheless of value: the
methods used in such proofs, although they must go beyond
Hilbert's original sense of finitism, might provide genuine
insight into the constructive content of arithmetic and stronger
theories. What Godel's result showed was that there can be
no absolute consistency proof of all of mathematics; hence work in
proof theory after Godel concentrated on relative results, both:
relative to the system for which a consistency proof was given, and
relative to the proof methods used.



Reductive proof theory in this sense has followed two traditions: the
first, mainly carried out by proof theorists following Gentzen and
Schutte, has pursued a program of what is called *ordinal
analysis*, and is exemplified by Gentzen's first consistency
proof of \(\PA\) by induction up to \(\varepsilon\_0 . \varepsilon\_0\)
is a certain transfinite (though countable) ordinal, however,
"induction up
to \(\varepsilon\_0\)" in the sense used
here is not a genuinely transfinite procedure. Ordinal analysis does
not operate with infinite ordinal numbers, but rather with *ordinal
notation systems* which themselves can be formalized in very weak
(essentially, finitary) systems. An ordinal analysis of a system \(T\)
is given if: (a) one can produce an ordinal notation system which
mimics the ordinals less than some ordinal \(\alpha\_T\) so that (b) it
can be proved finitarily that the formalization \(TI(\alpha\_T)\) of
the principle of induction up to \(\alpha\_T\) implies the consistency
of \(T\) (i.e., \(S \vdash TI(\alpha\_T)\rightarrow Con\_T)\) and (c)
\(T\) proves \(TI(\beta)\) for all \(\beta \lt \alpha\_T\) (\(S\) is a
theory formalizing finitary metamathematics and is generally a weak
sub-theory of \(T)\). To have any foundational significance it is also
required that one can give a constructive argument for transfinite
induction up to \(\alpha\_T\). As mentioned above, this was done for by
Gentzen and Takeuti for \(\varepsilon\_0\), the proof theoretic ordinal
of \(\PA\), but becomes more difficult and of progressively
questionable philosophical significance for stronger theories. See the
entry on
 proof theory
 for a survey of Gentzen's consistency proof,
 Mancosu et al. 2021
 for an accessible textbook presentation, and
 Thomas-Bolduc and Darnell 2022
 on Takeuti's well-ordering proof.



A philosophically more satisfactory continuation of Hilbert's
Program in proof theoretic terms has been suggested by Kreisel
 (1983;
 1968) and Feferman
 (Feferman, 1988;
 Feferman, 1993a). This work proceeds from 
a wider conception of
Hilbert's Program as an attempt to justify ideal mathematics by
restricted means. In this conception, the aim of Hilbert's proof
theory was to show that, at least as far as a certain class of real
propositions is concerned, ideal mathematics does not go beyond real
mathematics. A finitary consistency proof of the kind envisaged by
Hilbert would have accomplished this: if ideal mathematics proves a
real proposition, then this proposition is already provable by real
(i.e., finitary) methods. In a sense this *reduces* ideal
mathematics to real mathematics. A *proof-theoretic reduction*
of a theory \(T\) to a theory \(S\) shows that, as far as a certain
class of propositions is concerned, if \(T\) proves a proposition,
then \(S\) proves it too, and the proof of this fact is itself
finitary. Hilbert's proof theoretic program can then be seen to
be a search for a proof theoretic reduction of all of mathematics to
finitary mathematics; in a relativized program one looks for
reductions of theories weaker than all of classical mathematics to
theories often stronger than finitary mathematics. Proof theorists
have obtained a number of such results, including reductions of
theories which on their face require a significant amount of ideal
mathematics for their justification (e.g., subsystems of analysis) to
finitary systems.
 (Feferman, 1993b)
 has used such results in combination with other results that show
that most, if not all, of scientifically applicable mathematics can be
carried out in systems for which such reductions are available to
argue against the
 indispensability argument
 in the philosophy of mathematics. The philosophical significance of
such proof theoretic reductions is currently the subject of debate
 (Hofweber, 2000;
 Feferman, 2000).



The program of so-called reverse mathematics developed by, in
particular, Friedman and Simpson, is another continuation of
Hilbert's program. In the face of Godel's results
showing that not all of classical mathematics can be reduced to the
finitary, they seek to answer the question: how much of classical
mathematics can be so reduced? Reverse mathematics seeks to give a
precise answer to this question by investigating which theorems of
classical mathematics are provable in weak subsystems of analysis
which are reducible to finitary mathematics (in the sense discussed in
the preceding paragraph). A typical result is that the Hahn-Banach
theorem of functional analysis is provable in a theory known as
\(WKL\_0\) (for "weak Konig lemma"); \(WKL\_0\) is
conservative over \(\PRA\) for \(\Pi^{0}\_2\) sentences (i.e.,
sentences of the form \(\forall x\exists yA(x, y)\). (See
 Simpson 1988
 for an overview and
 Simpson 1999
 for a technical treatment.)