1: % Hilbert's Program Then and Now
2: % Richard Zach
3: % submitted version July 1, 2005
4:
5: % Note to typesetter: line breaks inside \index{} entries in source
6: % file generate multiple index entries. These have to be fixed
7:
8: \documentclass{article}
9: \usepackage{amssymb,named}
10:
11: \newcommand{\Bcite}[2]{\cite[#1]{#2}}
12: \newcommand{\pp}[1]{#1}
13:
14: \let\epsilon\varepsilon
15:
16: % Sam Buss's \Godelnum macro
17:
18: \newbox\gnBoxA
19: \newdimen\gnCornerHgt
20: \setbox\gnBoxA=\hbox{$\ulcorner$}
21: \global\gnCornerHgt=\ht\gnBoxA
22: \newdimen\gnArgHgt
23:
24:
25: \def\Godelnum #1{%
26: \setbox\gnBoxA=\hbox{$#1$}%
27: \gnArgHgt=\ht\gnBoxA%
28: \ifnum \gnArgHgt<\gnCornerHgt
29: \gnArgHgt=0pt%
30: \else
31: \advance \gnArgHgt by -\gnCornerHgt%
32: \fi
33: \raise\gnArgHgt\hbox{$\ulcorner$} \box\gnBoxA %
34: \raise\gnArgHgt\hbox{$\urcorner$}}
35:
36: \title{Hilbert's Program Then and Now}
37:
38: \author{Richard Zach}
39: \date{}
40: \begin{document}\bibliographystyle{named}
41:
42: \maketitle
43:
44: \begin{abstract}
45: Hilbert's program was an ambitious and wide-ranging project in the philosophy
46: and foundations of mathematics. In order to ``dispose of the foundational
47: questions in mathematics once and for all,'' Hilbert proposed a two-pronged
48: approach in 1921: first, classical mathematics should be formalized in
49: axiomatic systems; second, using only restricted, ``finitary'' means, one
50: should give proofs of the consistency of these axiomatic systems. Although
51: G\"odel's incompleteness theorems show that the program as originally
52: conceived cannot be carried out, it had many partial successes, and generated
53: important advances in logical theory and meta-theory, both at the time and
54: since. The article discusses the historical background and development of
55: Hilbert's program, its philosophical underpinnings and consequences, and its
56: subsequent development and influences since the 1930s.
57:
58:
59: \textbf{Keywords:} Hilbert's program, philosophy of mathematics, formalism,
60: finitism, proof theory, meta-mathematics, foundations of mathematics,
61: consistency proofs, axiomatic method, instrumentalism.
62: \end{abstract}
63:
64: \section{Introduction}
65:
66: Hilbert's program\index{Hilbert's program|(} is, in the first instance, a
67: proposal and a research program in the philosophy and foundations of
68: mathematics. It was formulated in the early 1920s by German mathematician
69: David Hilbert\index{Hilbert, D.|(} (1862--1943), and was pursued by him and his
70: collaborators at the University of G\"ottingen and elsewhere in the 1920s and
71: 1930s. Briefly, Hilbert's proposal called for a new foundation of mathematics
72: based on two pillars: the axiomatic method\index{axiomatic method}, and
73: finitary proof theory. Hilbert thought that by formalizing mathematics in
74: axiomatic systems, and subsequently proving by finitary methods that these
75: systems are consistent (i.e., do not prove contradictions), he could provide a
76: philosophically satisfactory grounding of classical, infinitary mathematics
77: (analysis and set theory). Had it been successful, Hilbert's program would
78: perhaps not only have eclipsed in subsequent influence other foundational
79: projects of the time, such as the logicist projects pursued by Frege and
80: Russell (see Vol.~9, Ch.~5) and Brouwer's\index{Brouwer, L. E. J.}
81: intuitionism\index{intuitionism} (see \textbf{Handbook reference?}), but it
82: would also have achieved Hilbert's stated goal, viz., to ``dispose of the
83: foundational questions in mathematics as such once and for all''
84: \cite[228]{Hilbert:29}. Unfortunately, G\"odel's theorems (see Ch.~11) show
85: that the program as originally envisaged by Hilbert cannot be carried out.
86:
87: Although Hilbert's own project for the foundation of mathematics was
88: ultimately unsuccessful, the project itself and technical advances made in its
89: pursuit have had an enormous impact on logic and the foundations of
90: mathematics more generally. In order to carry out the first part of the
91: program, the axiomatization of mathematics in a formal system, Hilbert and his
92: collaborators had pushed forward the development of logical formalisms in
93: which such an axiomatization could be carried out. This led, in particular,
94: to the first axiomatizations of propositional and first-order logic as
95: independent systems (i.e., other than as fragments of more comprehensive
96: higher-order systems, such as Frege's\index{Frege, G.} \emph{Begriffsschrift}
97: and the Whitehead-Russell\index{Russell, B.}\index{Whitehead, A. N.} system of
98: \emph{Principia mathematica})\index{Principia Mathematica} and their
99: meta-logical investigation, such as the proof (by Paul Bernays\index{Bernays,
100: P.} in 1918) of the completeness of the propositional calculus and the work
101: in Hilbert's school from 1921 onward on the decision problem. The
102: investigation of the meta-logical properties of logical systems led directly
103: to some of the most important meta-logical results in logic, viz., G\"odel's
104: completeness theorem\index{completeness theorem} and the negative solution by
105: Church\index{Church, A.} and Turing\index{Turing, A. M.} of the decision
106: problem\index{decision problem}. The development of proof theory itself is an
107: outgrowth of Hilbert's program. Gentzen's\index{Gentzen, G.} development of
108: natural deduction and the sequent calculus was carried out in the tradition of
109: Hilbert's program and with the aim of constructing a logical system which
110: facilitates consistency proofs\index{consistency proof}.
111: G\"odel\index{G\"odel, K.} obtained his incompleteness
112: theorems\index{incompleteness theorems} while trying to prove the consistency
113: of analysis. And the tradition of reductive proof theory of the
114: Gentzen-Sch\"utte school and others is itself a direct continuation of
115: Hilbert's program.
116:
117: The present chapter is divided into three parts: The first part provides a
118: sketch of the historical development of logic, proof theory, and philosophy of
119: mathematics in the work of Hilbert and his followers through the 1930s. The
120: second part deals with the philosophical interpretation and assessment of
121: Hilbert's program. The third part presents recent work in proof theory which
122: bears on the aims of Hilbert's program.
123:
124: \section{Hilbert's program then}
125:
126: \subsection{Hilbert's early work on foundations}
127:
128: Hilbert's\index{Hilbert's program!history of|(} work on the foundations of
129: mathematics can be traced to his work on geometry of the 1890s which resulted
130: in his influential textbook \emph{Foundations of Geometry}
131: \shortcite{Hilbert:99}. One philosophical advance of this work was the
132: development of Hilbert's conception of the axiomatic method\index{axiomatic
133: method}. Hilbert believed that the proper way to develop any scientific
134: subject rigorously required an axiomatic approach. In providing an axiomatic
135: treatment, the theory would be developed independently of any need for
136: intuition, and it would facilitate an analysis of the logical relationships
137: between the basic concepts and the axioms. Of basic importance for an
138: axiomatic treatment are, so Hilbert, investigation of the independence and,
139: above all, of the consistency of the axioms. In his 1902 lectures on the
140: foundations of geometry, he puts it thus:
141: \begin{quotation}
142: Every science takes its starting point from a sufficiently coherent body of
143: facts is given. It takes form, however, only by \emph{organizing} this body
144: of facts. This organization takes place through the \emph{axiomatic
145: method}\index{axiomatic method}, i.e., one constructs a \emph{logical
146: structure of concepts} so that the relationships between the concepts
147: correspond to relationships between the facts to be organized.
148:
149: There is arbitrariness in the construction of such a structure of concepts;
150: we, however, \emph{demand} of it:
151:
152: 1) completeness, 2) independence, 3) consistency. \cite[540]{Hilbert:04}
153: \end{quotation}
154: From the time of his work on geometry forward, the last consideration,
155: consistency, was of special importance in Hilbert's conception of the
156: axiomatic method\index{axiomatic method} in general and the foundations of
157: mathematics in particular. Hilbert was heavily influenced by the foundational
158: views of late-19th century mathematicians, in particular, Cantor\index{Cantor,
159: G.}, Dedekind,\index{Dedekind, R.} and Kronecker\index{Kronecker, L.|(}. He
160: shared with Dedekind and Cantor the view that mathematical activity should be
161: free of constraints, which led to his view, highlighted in his correspondence
162: with Frege\index{Frege, G.}, that consistency of an axiomatic theory
163: guarantees the existence of the structure described, and is in this sense
164: sufficient to justify the use of the theory. And he shared with Kronecker a
165: recognition that elementary arithmetic has a privileged role in mathematics,
166: although he was of course opposed to the converse espoused by Kronecker, viz.,
167: that the natural numbers, and constructions based on elementary arithmetic,
168: exhaust legitimate mathematics. These two influences in Hilbert's thought are
169: at the root of his investigations of consistency.
170:
171: Proofs of consistency\index{consistency proof} for the axioms of geometry can
172: be given by providing an interpretation of the system in the real plane, and
173: thus the consistency of geometry is reduced to the consistency of analysis.
174: Analysis, of course, itself requires justification. In
175: \shortcite{Hilbert:00}, Hilbert approached the problem from the axiomatic
176: standpoint by proposing an axiomatization of the real numbers. In order to
177: show the consistency of this system, Hilbert expressly rejected the
178: construction of a model, e.g., a construction based on Dedekind
179: cuts\index{Dedekind cut} of rationals, as an option. He considered the
180: construction of the reals from the rationals and ultimately the natural
181: numbers using the ``genetic method'' as insufficient: ``Despite the high
182: pedagogical and heuristic value of the genetic method, for the final
183: presentation and the complete logical grounding of our knowledge the axiomatic
184: method deserves the first rank'' \cite[1093]{Hilbert:00}. Hilbert thus was
185: after a \emph{direct} consistency proof\index{consistency proof} of analysis,
186: i.e., one not based on reduction to another theory. He proposed the problem
187: of finding such a proof as the second of his 23 mathematical problems in his
188: address to the International Congress of Mathematicians in 1900
189: \shortcite{Hilbert:00a}.
190:
191: The discovery of Russell's paradox\index{Russell's paradox} in 1902 made it
192: clear that an axiomatic foundation of arithmetic and set theory requires a
193: more precise development of the underlying logical systems. Hilbert knew of
194: the paradoxes of set theory\index{set theory!paradoxes of} from
195: Cantor\index{Cantor, G.} and Zermelo\index{Zermelo, E.|(}, but it was
196: apparently not until Russell\index{Russell, B.}'s \shortcite{Russell:02a}
197: publication of the contradiction in Frege\index{Frege, G.}'s system that
198: Hilbert and Zermelo realized their importance. Hilbert's exchange with
199: Frege\index{Frege, G.} on the axiomatic approach to geometry led him to
200: realize that his conceptions of ``axiom,'' ``definition,'' ``proof'' were in
201: need of clarification. In response, Hilbert formulated an early version of
202: his proof-theoretical program in his 1904 Heidelberg talk
203: \shortcite{Hilbert:05}. After criticizing the foundational views of
204: Kronecker\index{Kronecker, L.|)} as dogmatic, and those of Frege\index{Frege,
205: G.} and Dedekind\index{Dedekind, R.} as suffering from ``unavoidable
206: contradictions,'' he writes:
207: \begin{quotation}
208: Arithmetic is often considered to be a part of logic, and the traditional
209: fundamental logical notions are usually presupposed when it is a question of
210: establishing a foundation for arithmetic. If we observe attentively,
211: however, we realize that in the traditional exposition of the laws of logic
212: certain fundamental arithmetic notions are already used, for example, the
213: notion of set and, to some extent, also that of number. Thus we find
214: ourselves turning in a circle, and that is why a partly simultaneous
215: development of the laws of logic and of arithmetic is required if paradoxes
216: are to be avoided. \cite[131]{Hilbert:05}
217: \end{quotation}
218: Hilbert's sketch of this ``simultaneous development'' of logic and arithmetic
219: in the case of a very basic axiom system for the natural numbers is very close
220: to the the approach Hilbert's proof theoretic program would take 20 years
221: later: Hilbert gives a direct argument that no contradiction can arise from
222: the five axioms of his system.
223:
224: This was a promising start, but several factors delayed the further
225: development of Hilbert's proof theoretic program. One was Poincar\'e's
226: \shortcite{Poincare:06a}\index{Poincar\'e, H.} criticism of what he saw as a
227: viciously circular use of induction\index{induction!Poincar\'e on} in
228: Hilbert's sketched consistency proof\index{consistency proof} (see
229: \cite{Steiner:75}\index{Steiner, M.}, Appendix). Moreover, Hilbert realized
230: that axiomatic investigations required a well worked-out logical formalism in
231: which axiomatic systems could be developed. At the time he used a logical
232: formalism based on Schr\"oder's\index{Schr\"oder, E.} algebraic
233: logic\index{logic!algebraic}, which was not particularly suited as a formalism
234: for the axiomatization of mathematics. Following the 1905 lectures on
235: foundations, Hilbert turned his immediate attention to work in other areas of
236: mathematics and theoretical physics. He did, however, actively support others
237: who worked on foundational questions in G\"ottingen, in particular Ernst
238: Zermelo\index{Zermelo, E.|)} and Leonard Nelson\index{Nelson,
239: L.}.\footnote{See \cite{Sieg:99,Sieg:02}\index{Sieg, W.},
240: \cite{Stein:88}\index{Stein, H.},
241: \cite{Hallett:90,Hallett:94}\index{Hallett, M.},
242: \cite{Mancosu:98c}\index{Mancosu, P.}, and \cite{Avigad:01}\index{Avigad,
243: J.}\index{Reck, E.} for further discussion of the conceptual framework and
244: historical background of Hilbert's thought, and
245: \cite{Resnik:74}\index{Resnik, M.} on the Frege\index{Frege, G.}-Hilbert
246: correspondence. On Hilbert's foundational interests before 1917, and his
247: engagement for Husserl\index{Husserl, E.}, Zermelo, and Nelson\index{Nelson,
248: L.} in G\"ottingen, see \cite{Peckhaus:90}\index{Peckhaus, V.}. On
249: general discussions of formalism and the place of Hilbert's thought in the
250: mathematical context of the late 19th century, see
251: \cite{Webb:97}\index{Webb, J.} and \cite{Detlefsen:05}\index{Detlefsen,
252: M.}.}
253:
254: The publication of Whitehead\index{Whitehead, A. N.} and Russell\index{Russell, B.}'s
255: \emph{Principia Mathematica}\index{Principia Mathematica}
256: \shortcite{Russell:10,Russell:12,Russell:13} provided the required logical
257: basis for a renewed attack on foundational issues. Beginning in 1914,
258: Hilbert's student Heinrich Behmann\index{Behmann, H.} and others studied the
259: system of \emph{Principia}.\footnote{See \cite{Mancosu:99} and
260: \shortcite{Mancosu:03}\index{Mancosu, P.} on Behmann\index{Behmann, H.}'s
261: role in Hilbert's school and the influence of Russell\index{Russell, B.}.} Hilbert
262: himself returned to work on the foundations of mathematics in 1917. In
263: September 1917, he delivered an address to the Swiss Mathematical Society
264: entitled ``Axiomatic Thought'' \shortcite{Hilbert:18}. It is his first
265: published contribution to mathematical foundations since 1905. In it, he
266: again emphasized the requirement of consistency proofs\index{consistency
267: proof} for axiomatic systems: ``The chief requirement of the theory of
268: axioms must go farther [than merely avoiding known paradoxes], namely, to show
269: that within every field of knowledge contradictions based on the underlying
270: axiom-system are \emph{absolutely impossible}.'' He posed the proof of the
271: consistency of the integers (and of set theory) again as the main problems.
272: In both these cases, there seems to be nothing more fundamental available to
273: which the consistency could be reduced other than logic itself. Hilbert at
274: the time considered the problem as essentially solved by
275: Whitehead\index{Whitehead, A. N.} and Russell\index{Russell, B.}'s work in
276: \emph{Principia}\index{Principia Mathematica}. Nevertheless, other
277: fundamental problems of axiomatics remained unsolved, including the problem of
278: the ``decidability of every mathematical question,'' which also traces back to
279: Hilbert's 1900 address.
280:
281: These unresolved problems of axiomatics led Hilbert to devote significant
282: effort to work on logic in the following years. In 1917, Paul
283: Bernays\index{Bernays, P.} joined him as his assistant in G\"ottingen. In a
284: series of courses from 1917--1921, Hilbert, with the assistance of
285: Bernays\index{Bernays, P.} and Behmann\index{Behmann, H.}, made significant
286: new contributions to formal logic. The course from 1917 \cite{Hilbert:17}, in
287: particular, contains a sophisticated development of first-order
288: logic\index{logic!first order}, and forms the basis of Hilbert and
289: Ackermann\index{Ackermann, W.}'s textbook \emph{Principles of Theoretical
290: Logic} \shortcite{Hilbert:28b}. In 1918, Bernays\index{Bernays, P.}
291: submitted a treatise on the propositional calculus of \emph{Principia
292: mathematica} as a \emph{Habilitationsschrift}; it contains the first
293: completeness proof\index{completeness!of propositional logic} of the
294: propositional calculus for truth-functional semantics.\footnote{See
295: \cite{Moore:97}\index{Moore, G.}, \cite{Sieg:99}\index{Sieg, W.} and
296: \cite{Zach:99}\index{Zach, R.} for more detail on the
297: development of logic in Hilbert's school around 1918.}
298:
299: The 1917--18 lectures were only the beginning of a strand of work on logic and
300: meta-logic in Hilbert's school, including work on the decision problem. The
301: decision problem for first-order logic was tightly bound up with the aim of
302: finding a completeness proof for the first-order predicate
303: calculus\index{logic!first order} (the ``restricted calculus of functions'' in
304: Hilbert's terminology). This aim was stated in the 1917--18 lectures, but
305: since completeness does not hold for first-order logic in any purely syntactic
306: sense (an early result due to Ackermann\index{Ackermann, W.}), a development
307: of the semantics of first-order logic was needed first. The decision
308: problem\index{decision problem}, one of Hilbert's main aims for
309: metamathematics in the 1920s, was already an issue in the lectures from 1905,
310: and has its roots in Hilbert's belief, first explicitly stated in the Paris
311: address, that ``in mathematics, there is no ignorabimus,'' i.e., that every
312: mathematical question can be solved either affirmatively or negatively. The
313: questions of completeness\index{completeness} and decidability thus became
314: closely linked in the 1920s, with Behmann\index{Behmann, H.},
315: Bernays\index{Bernays, P.}, Sch\"onfinkel, and later
316: Ackermann\index{Ackermann, W.} working on special cases of the decision
317: problem\index{decision problem} for first-order logic throughout the 1920s.
318:
319: \subsection{The consistency program, finitism, and proof theory}
320:
321: In about 1920, Hilbert came to reject Russell\index{Russell, B.}'s
322: logicist\index{logicism} solution to the consistency problem for arithmetic,
323: mainly for the reason that the axiom of reducibility cannot be accepted as a
324: purely logical axiom. In lectures from the Summer term 1920, he concluded
325: that ``the aim of reducing set theory, and with it the usual methods of
326: analysis, to logic, has not been achieved today and maybe cannot be achieved
327: at all'' \cite{Hilbert:20b}. At the same time, Brouwer's\index{Brouwer, L. E.
328: J.} intuitionist\index{intuitionism} mathematics gained currency. In
329: particular, Hilbert's former student Hermann Weyl\index{Weyl, H.} converted
330: to intuitionism. Weyl's 1920 address to the Hamburg Mathematical Seminar,
331: ``The new foundational crisis in mathematics'' \shortcite{Weyl:21} was
332: answered by Hilbert in three talks in Hamburg in the Summer of 1921
333: \shortcite{Hilbert:22a}. Here, Hilbert presented his own mature proposal for
334: a solution to the problem of the foundation of mathematics. This proposal
335: incorporated Hilbert's ideas from 1904 regarding direct consistency
336: proofs\index{consistency proof}, his conception of axiomatic systems, and also
337: the technical developments in the axiomatization of mathematics in the work of
338: Russell\index{Russell, B.} as well as the further developments carried out by him and
339: his collaborators. What was new was the way in which Hilbert wanted to imbue
340: his consistency project with the philosophical significance necessary to
341: answer Brouwer\index{Brouwer, L. E. J.} and Weyl\index{Weyl, H.}'s criticisms:
342: the finitary point of view.
343:
344: According to Hilbert, there is a privileged part of
345: mathematics,\index{finitism|(} contentual elementary number theory, which
346: relies only on a ``purely intuitive basis of concrete signs.'' Whereas the
347: operating with abstract concepts was considered ``inadequate and uncertain,''
348: there is a realm of
349: \begin{quote}
350: extra-logical discrete objects, which exist intuitively as immediate
351: experience before all thought. If logical inference is to be certain, then
352: these objects must be capable of being completely surveyed in all their
353: parts, and their presentation, their difference, their succession (like the
354: objects themselves) must exist for us immediately, intuitively, as something
355: which cannot be reduced to something else.\footnote{\cite[202]{Hilbert:22a}.
356: The passage is repeated almost verbatim in \cite[376]{Hilbert:26},
357: \cite[464]{Hilbert:28}, and \cite[267]{Hilbert:31a}}
358: \end{quote}
359: The objects in questions are \emph{signs}, both numerals and the signs
360: that make up formulas a formal proofs. The domain of contentual number theory
361: consists in the finitary numerals, i.e., sequences of strokes. These have no
362: meaning, i.e., they do not stand for abstract objects, but they can be
363: operated on (e.g., concatenated) and compared. Knowledge of their properties
364: and relations is intuitive and unmediated by logical inference. Contentual
365: number theory developed this way is secure, according to Hilbert: no
366: contradictions can arise simply because there is no logical structure in the
367: propositions of contentual number theory.\index{finitism|)}
368:
369: The intuitive-contentual operations with signs form the basis of Hilbert's
370: meta-mathematics\index{meta-mathematics}. Just as contentual number theory
371: operates with sequences of strokes, so meta-mathematics operates with
372: sequences of symbols (formulas, proofs). Formulas and proofs can be
373: syntactically manipulated, and the properties and relationships of formulas
374: and proofs are similarly based in a logic-free intuitive capacity which
375: guarantees certainty of knowledge about formulas and proofs arrived at by such
376: syntactic operations. Mathematics itself, however, operates with abstract
377: concepts, e.g., quantifiers, sets, functions, and uses logical inference based
378: on principles such as mathematical induction or the principle of the excluded
379: middle. These ``concept-formations'' and modes of reasoning had been
380: criticized by Brouwer and others on grounds that they presuppose infinite
381: totalities as given, or that they involve impredicative\index{impredicative}
382: definitions (which were considered by the critics as viciously circular).
383: Hilbert's aim was to justify their use. To this end, he pointed out that they
384: can be formalized in axiomatic systems (such as that of
385: \emph{Principia}\index{Principia Mathematica} or those developed by Hilbert
386: himself), and mathematical propositions and proofs thus turn into formulas and
387: derivations from axioms according to strictly circumscribed rules of
388: derivation. Mathematics, so Hilbert, ``becomes an inventory of provable
389: formulas.'' In this way the proofs of mathematics are subject to
390: metamathematical, contentual investigation. The goal of Hilbert's program is
391: then to give a contentual, meta-mathematical proof that there can be no
392: derivation of a contradiction\index{contradiction}, i.e., no formal derivation
393: of a formula $A$ and of its negation $\neg A$.
394:
395: This sketch of the aims of the program was fleshed out by Hilbert and his
396: collaborators in the following 10 years. On the conceptual side, the finite
397: standpoint and the strategy for a consistency proof\index{consistency proof}
398: were elaborated by Hilbert \shortcite{Hilbert:23,Hilbert:26,Hilbert:28} and
399: Bernays\index{Bernays, P.} \shortcite{Bernays:22,Bernays:28a,Bernays:30}, of
400: which Hilbert's article ``On the infinite'' \shortcite{Hilbert:26} provides
401: the most detailed discussion of the finitary standpoint. In addition to
402: Hilbert and Bernays\index{Bernays, P.}, a number of other people were involved
403: in technical work on the program. The $\epsilon$-operator\index{epsilon
404: calculus@$\epsilon$-calculus|(} was first introduced in the Hamburg lecture
405: of 1921 \cite{Hilbert:22a}, and developed in a number of lectures given in
406: G\"ottingen \cite{Hilbert:21,Hilbert:22b}, as well as in \cite{Hilbert:23}.
407: Hilbert and Bernays\index{Bernays, P.} developed the $\epsilon$-calculus as
408: their definitive formalism for axiom systems for arithmetic and analysis, and
409: the so-called $\epsilon$-substitution method as the preferred approach to
410: giving consistency proofs.
411:
412: Briefly, the $\epsilon$-calculus is a formalism that includes $\epsilon$ as a
413: term-forming operator. If $A(x)$ is a formula, then $\epsilon_x A(x)$ is a
414: term, which intuitively stands for a witness for~$A(x)$. In a logical
415: formalism containing the $\epsilon$-operator, the quantifiers can be defined
416: by: $\exists x\, A(x) \equiv A(\epsilon_x A(x))$ and $\forall x\, A(x) \equiv
417: A(\epsilon_x \lnot A(x))$. The only additional axiom necessary is the
418: so-called ``transfinite axiom,'' $A(t) \to A(\epsilon_x A(x))$. Based on this
419: idea, Hilbert and his collaborators developed axiomatizations of number theory
420: and analysis. Consistency proofs\index{consistency proof} for these systems
421: were then given using the $\epsilon$-substitution method\index{epsilon
422: substitution@$\epsilon$-substitution method}. The idea of this method is,
423: roughly, that the $\epsilon$-terms $\epsilon_x A(x)$ occurring in a formal
424: proof are replaced by actual numerals, resulting in a quantifier-free proof.
425: The simplest case, outlined in Hilbert's papers, is as follows. Suppose we
426: had a (suitably normalized) derivation of $0 = 1$ that contains only one
427: $\epsilon$-term $\epsilon_x A(x)$. Replace all occurrences of $\epsilon_x
428: A(x)$ by $0$. The instances of the transfinite axiom then are all of the form
429: $A(t) \to A(0)$. Since no other $\epsilon$-terms occur in the proof, $A(t)$
430: and $A(0)$ are basic numerical formulas without quantifiers and, we may
431: assume, also without free variables. So they can be evaluated by finitary
432: calculation. If all such instances turn out to be true numerical formulas, we
433: are done. If not, this must be because $A(t)$ is true for some~$t$, and
434: $A(0)$ is false. Then replace $\epsilon_x A(x)$ instead by $n$, where $n$ is
435: the numerical value of the term~$t$. The resulting proof is then seen to be a
436: derivation of $0=1$ from true, purely numerical formulas using only modus
437: ponens, and this is impossible. Indeed, the procedure works with only slight
438: modifications even in the presence of the induction axiom, which in the
439: $\epsilon$-calculus takes the form of a least number principle: $A(t) \to
440: \epsilon_x A(x) \le t$, which intuitively requires $\epsilon_x A(x)$ to be the
441: \emph{least} witness for $A(x)$.
442:
443: The $\epsilon$-substitution method is simple enough for the basic cases
444: considered by Hilbert, but becomes extremely complex when $\epsilon$-operators
445: are nested. In his 1924 dissertation, \cite{Ackermann:24}\index{Ackermann,
446: W.} presented an (erroneous) consistency proof\index{consistency proof}
447: based on the $\epsilon$-substitution method for a version of analysis. John
448: von Neumann\index{von Neumann, J.}, then visiting G\"ottingen, gave a
449: corrected consistency proof\index{consistency proof} for a system of the
450: $\epsilon$-formalism (which, however, did not include the induction axiom) in
451: 1925 \shortcite{Neumann:27}\index{von Neumann, J.}. Building on von Neumann's
452: work, Ackermann\index{Ackermann, W.} devised a new $\epsilon$-substitution
453: procedure which he communicated to Bernays\index{Bernays, P.} (see
454: \cite{Bernays:28a}). Ackermann and Bernays considered the proof to be correct
455: for the entire first-order fragment of arithmetic and were confident that it
456: could be extended to a consistency proof\index{consistency proof} of analysis.
457: In his address ``Problems of the grounding of mathematics'' to the
458: International Congress of Mathematicians in Bologna in 1928
459: \shortcite{Hilbert:29}, Hilbert optimistically claimed that the work of
460: Ackermann\index{Ackermann, W.} and von Neumann\index{von Neumann, J.} had
461: established the consistency of number theory and that the proof for analysis
462: had already been carried out by Ackermann\index{Ackermann, W.} ``to the extent
463: that the only remaining task consists in the proof of an elementary finiteness
464: theorem that is purely arithmetical.''\footnote{See
465: \cite{Avigad:02}\index{Avigad, J.} for a general introduction to the
466: $\epsilon$-calculus and \cite{Zach:03}\index{Zach, R} and
467: \shortcite{Zach:02} on the history of the $\epsilon$-calculus and the
468: substitution method. \cite{Sieg:99}\index{Sieg, W.} presents a detailed and
469: perceptive analysis of the development of the program and its influence as a
470: whole.}\index{epsilon calculus@$\epsilon$-calculus|)}
471:
472: \subsection{The impact of G\"odel's incompleteness
473: theorems}\label{impact-godel}
474:
475: G\"odel\index{G\"odel, K.}'s incompleteness theorems\index{incompleteness
476: theorems|(} \cite{Godel:31} showed that Hilbert's optimism was unfounded. In
477: September 1930, Kurt G\"odel\index{G\"odel, K.} announced his first
478: incompleteness theorem\index{incompleteness theorems!first incompleteness
479: theorem} at a conference in K\"onigsberg. Von Neumann\index{von Neumann,
480: J.}, who was in the audience, immediately recognized the significance of
481: G\"odel\index{G\"odel, K.}'s result for Hilbert's program. Shortly after the
482: conference he wrote to G\"odel\index{G\"odel, K.}, telling him that he had
483: found a corollary to G\"odel's result. G\"odel\index{G\"odel, K.} had found
484: the same result already independently: the second incompleteness
485: theorem\index{incompleteness theorems!second incompleteness theorem},
486: asserting that the system of \emph{Principia}\index{Principia Mathematica}
487: does not prove the formalization of the claim that the system of
488: \emph{Principia} is consistent (provided it is). All the methods of finitary
489: reasoning used in the consistency proofs\index{consistency proof} up till then
490: were believed to be formalizable in \emph{Principia}, however. Hence, if the
491: consistency of \emph{Principia} were provable by the methods used in
492: Ackermann\index{Ackermann, W.}'s proofs, it should be possible to formalize
493: this proof in \emph{Principia}; but this is what the second incompleteness
494: theorem\index{incompleteness theorems!second incompleteness theorem} states is
495: impossible. Bernays\index{Bernays, P.} also immediately realized the
496: importance of G\"odel\index{G\"odel, K.}'s results after he studied G\"odel's
497: paper in January 1931. He wrote to G\"odel\index{G\"odel, K.} that (under the
498: assumption that finitary reasoning can be formalized in \emph{Principia}) the
499: incompleteness theorems seem to show that a finitary consistency
500: proof\index{consistency proof} of \emph{Principia} is impossible. Shortly
501: thereafter, von Neumann\index{von Neumann, J.} showed that
502: Ackermann\index{Ackermann, W.}'s consistency proof\index{consistency proof} is
503: flawed and provided a counterexample to the proposed $\epsilon$-substitution
504: procedure.\footnote{The correspondence between G\"odel\index{G\"odel, K.} and
505: Bernays\index{Bernays, P.} is published in \cite[41--313]{Godel:03} and that
506: with von Neumann\index{von Neumann, J.} in \cite[327--377]{Godel:03a}. See
507: also the informative introductions by Feferman and Sieg, respectively, to
508: these sections of the correspondence, as well as
509: \cite{Mancosu:04a}\index{Mancosu, P.} and the last section of
510: \cite{Zach:03}\index{Zach, R.}.}
511:
512: Although the impact of G\"odel\index{G\"odel, K.}'s incompleteness theorems
513: for Hilbert's program was recognized soon after their publication, Hilbert's
514: program was by no means abandoned. Hilbert himself was no longer actively
515: involved in foundational research, but Bernays\index{Bernays, P.} continued to
516: work on the foundations of mathematics. The two-volume \emph{Grundlagen der
517: Mathematik} \cite{HilbertBernays:34,HilbertBernays:39} was prepared by
518: Bernays\index{Bernays, P.} alone, and included new results by
519: Ackermann\index{Ackermann, W.} and Bernays\index{Bernays, P.} on the
520: $\epsilon$-calculus. It also included Herbrand's\index{Herbrand, J.}
521: \shortcite{Herbrand:30} work on proof theory, and a sketch of
522: Gentzen\index{Gentzen, G.}'s \shortcite{Gentzen:36} consistency
523: proof\index{consistency proof} of first-order arithmetic\index{Peano
524: arithmetic}. Bernays\index{Bernays, P.}'s and Gentzen\index{Gentzen, G.}'s
525: work, in particular, focused on possible extensions of the finitary standpoint
526: which could yield consistency proofs for substantial parts of mathematics in
527: spite of G\"odel\index{G\"odel, K.}'s theorems.\index{incompleteness
528: theorems|)}
529:
530: Gentzen\index{Gentzen, G.}'s first consistency proof\index{consistency proof}
531: for number theory, the so-called galley proof \shortcite{Gentzen:35}, was the
532: result of a combination of Gentzen's \shortcite{Gentzen:34} earlier work on
533: the logical formalism of the sequent calculus, which provided a
534: proof-theoretically more convenient axiomatization of arithmetic, and a new
535: strategy of proving consistency. This strategy involved defining certain
536: ``reduction steps'' on proofs: local transformations of parts of a derivation
537: in the new formalism. The consistency proof\index{consistency proof} then
538: proceeds by showing that by iterating these reductions on a proof one
539: eventually arrives at a proof of a special form (a proof free of the cut rule
540: and the induction rule), and no proof of such a form can be the proof of a
541: contradiction. The first version of the proof relied on the notion of a
542: reduction rule, which itself cannot be formalized in arithmetic.\footnote{On
543: the galley proof, see \cite{Bernays:70}\index{Bernays, P.}, \cite[Appendix
544: II]{Kreisel:71}, and \cite{Negri:80}.} This notion met with some
545: objections, and in the revised, published version \shortcite{Gentzen:36},
546: Gentzen\index{Gentzen, G.} replaced the appeal to reduction rules by a proof
547: that the iteration of reduction steps itself terminates. He did this by
548: assigning a measure for the complexity of a given derivation, and showed that
549: the result of the application of a reduction step to a proof reduces the
550: complexity measure of that proof. The complexity measure
551: Gentzen\index{Gentzen, G.} used was certain finite strings of numbers which
552: may be interpreted as naming countable ordinals less
553: than~$\epsilon_0$\index{epsilon zero@$\epsilon_0$}.\footnote{If $\omega_0 =
554: \omega$, and $\omega_{n+1} = \omega^{\omega_n}$, then the ordinal
555: $\epsilon_0$ is the limit of $\omega_n$ for $n = 1, 2, \ldots$. In other
556: words, $\epsilon_0$ is the least fixed point of $\alpha = \omega^\alpha$.}
557: The consistency result\index{consistency proof} then follows if one accepts
558: that there are no infinite descending sequences of such ordinal notations, or,
559: more precisely, by using transfinite induction up to~$\epsilon_0$. This
560: principle, by G\"odel\index{G\"odel, K.}'s incompleteness
561: theorem\index{incompleteness theorems}, cannot itself be formalized in
562: first-order arithmetic \cite{Gentzen:43}. Gentzen\index{Gentzen, G.}'s proof
563: allowed \cite{Ackermann:40}\index{Ackermann, W.} to give a correct consistency
564: proof\index{consistency proof} based on the $\epsilon$-substitution method for
565: first-order arithmetic, also based on transfinite induction up
566: to~$\epsilon_0$.
567:
568: Gentzen\index{Gentzen, G.}'s work marks the beginning of post-G\"odelian proof
569: theory. In the proof-theoretic tradition of Gentzen\index{Gentzen, G.},
570: axiomatic theories are analyzed according to which transfinite induction
571: principles are required to prove the consistency\index{consistency proof} of
572: the theory. However, Gentzen\index{Gentzen, G.}'s contribution and influence
573: goes beyond this: He emphasized that proof-theoretic methods do not just allow
574: us to prove the consistency of a theory, but that they also enable us to
575: extract information from proofs beyond the fact that the formula proved
576: follows from the axioms.\index{Hilbert's program!history of|)}
577:
578: \section{Philosophical interpretation of Hilbert's program}
579:
580: The philosophical importance and influence of Hilbert's work on foundations is
581: twofold. First, the epistemological standpoint of Hilbert's finitism is of
582: interest in the philosophy of mathematics quite independently of the success
583: of the proof-theoretic program which it underlies. Like other important
584: proposals in the philosophy of mathematics such as
585: intuitionism\index{intuitionism}, predicativism, and logicism\index{logicism},
586: Hilbert's finitism is, \emph{inter alia}, a philosophical view about the
587: nature of mathematical knowledge and delineates a particular set of
588: (finitarily) meaningful propositions, as well as finitarily admissible
589: constructions and methods of proof. Debate about the status of finitary
590: evidence and proof are still very much alive today. Second, Hilbert's program
591: can and has been seen as a version of reductive instrumentalism in
592: mathematics. That is to say, one can read Hilbert as proposing that only a
593: certain part of mathematics (propositions, proofs) is meaningful, viz., the
594: finitary part. The rest, which includes classical infinitary mathematics (full
595: first-order arithmetic\index{Peano arithmetic}, analysis, and set theory, in
596: particular) are mere instruments. Hilbert's program has thus been an
597: important inspiration for related instrumentalist proposals in the philosophy
598: of mathematics (e.g., \cite{Field:80,Detlefsen:86}\index{Field,
599: H.}\index{Detlefsen, M.}).
600:
601: This section will expand on these two themes. In the case of both the debate
602: on the philosophy of finitism, and on the view of Hilbert's program as an
603: instrumentalist philosophy of mathematics, questions of historical
604: interpretation interact with conceptual analysis. The distinction between
605: these aspects should be kept in mind.
606:
607: \subsection{The finitary point of view}
608:
609: The cornerstone of Hilbert's philosophy of mathematics, and the substantially
610: new aspect of his foundational thought from \shortcite{Hilbert:22a} onward,
611: was the so-called finitary standpoint\index{finitism|(}. This methodological
612: standpoint consists in a restriction of mathematical thought to objects which
613: are ``intuitively present as immediate experience prior to all thought,'' and
614: to those operations on and methods of reasoning about such objects which do
615: not require the introduction of abstract concepts, in particular, require no
616: appeal to completed infinite totalities.
617:
618: Hilbert characterized the domain of finitary reasoning in a well-known
619: paragraph which appears in roughly the same formulation in all of
620: Hilbert's more philosophical papers from the 1920s
621: \shortcite{Hilbert:22a,Hilbert:26,Hilbert:28,Hilbert:31a}:
622: \begin{quote}
623: [A]s a condition for the use of logical inferences and the performance
624: of logical operations, something must already be given to our faculty
625: of representation, certain extra-logical concrete objects that are
626: intuitively present as immediate experience prior to all thought. If
627: logical inference is to be reliable, it must be possible to survey
628: these objects completely in all their parts, and the fact that they
629: occur, that they differ from one another, and that they follow each
630: other, or are concatenated, is immediately given intuitively, together
631: with the objects, as something that can neither be reduced to anything
632: else nor requires reduction. This is the basic philosophical position
633: that I consider requisite for mathematics and, in general, for all
634: scientific thinking, understanding, and
635: communication. \cite[376]{Hilbert:26}
636: \end{quote}
637: These objects are, for Hilbert, the \emph{signs}. For the domain of contentual
638: number theory, the signs in question are sequences of strokes (``numerals'')
639: such as
640: \[
641: \mid, \mid\mid, \mid\mid\mid, \mid\mid\mid\mid\mid.
642: \]
643: The question of how exactly Hilbert understood the numerals is difficult to
644: answer. What is clear in any case is that they are logically primitive, i.e.,
645: they are neither concepts (as Frege\index{Frege, G.}'s numbers are) nor sets.
646: For Hilbert, the important issue is not primarily their metaphysical status
647: (abstract versus concrete in the current sense of these terms), but that they
648: do not enter into logical relations, e.g., they cannot be predicated of
649: anything. In Bernays\index{Bernays, P.}'s most mature presentations of
650: finitism \cite{Bernays:30,HilbertBernays:39}, the objects of finitism are
651: characterized as \emph{formal objects} which are recursively generated by a
652: process of repetition; the stroke symbols are then concrete representations of
653: these formal objects (see \cite{Sieg:02}\index{Sieg, W.}).
654:
655: Sometimes Hilbert's view is presented as if Hilbert claimed that the numbers
656: are signs on paper. It is important to stress that this is a
657: misrepresentation, that the numerals are not physical objects in the sense
658: that truths of elementary number theory are dependent only on external
659: physical facts or even physical possibilities (e.g., on what sorts of stroke
660: symbols it is possible to write down). \cite{Hilbert:26} made too much of
661: the fact that for all we know, neither the infinitely small nor the infinitely
662: large are actualized in physical space and time, yet he certainly held that
663: the number of strokes in a numeral is at least potentially infinite. It is
664: also essential to the conception that the numerals are sequences of one kind
665: of sign, and that they are somehow dependent on being grasped as such a
666: sequence, that they do not exist independently of our intuition of them. Only
667: our seeing or using ``$\mid\mid\mid\mid$'' as a sequence of 4 strokes as
668: opposed to a sequence of 2 symbols of the form ``$\mid\mid$'' makes
669: ``$\mid\mid\mid\mid$'' into the numeral that it is. This raises the question
670: of individuation of stroke symbols. An alternative account would have
671: numerals be mental constructions. However, Bernays\index{Bernays, P.} denied
672: also this, writing that ``the objects of intuitive number theory, the number
673: signs, are, according to Hilbert, also not `created by thought'. But this
674: does not mean that they exist independently of their {\em intuitive
675: construction}, to use the Kantian term that is quite appropriate here''
676: \cite[226]{Bernays:23b}. \cite{Kitcher:76}\index{Kitcher, P.} proposes the
677: view that, whatever the numerals are, the strokes on paper or the stroke
678: sequences contemplated by the mind merely \emph{represent} the numerals.
679: According to Hilbert and Bernays\index{Bernays, P.}, the numerals are given in
680: our representation, but they are not merely subjective ``mental cartoons''
681: (Kitcher's term).
682: \begin{quote}
683: If we want [\dots] the ordinal numbers as definite objects free of all
684: inessential elements, then in each case we have to take the mere schema of
685: the relevant figure of repetition [{\em Wiederholungsfigur}] as an object;
686: this requires a very high abstraction. We are free, however, to represent
687: these purely formal objects by concrete objects (``number signs''); these
688: contain then inessential, arbitrarily added properties, which, however, are
689: also easily grasped as such. \cite[244]{Bernays:30}\index{Bernays, P.}
690: \end{quote}
691: One version of this view would be to hold that the numerals are {\em
692: types} of stroke-symbols as represented in intuition. This is
693: the interpretation that \cite{Tait:81}\index{Tait, W. W.} gives. At first
694: glance, this seems to be a viable reading of Hilbert. It takes care of the
695: difficulties that the reading of numerals-as-tokens (both physical and mental)
696: faces, and it gives an account of how numerals can be dependent on their
697: intuitive construction while at the same time not being created by thought.
698: The reasoning that leads Tait to put forward his reading lies in several
699: constraints that Hilbert and Bernays\index{Bernays, P.} put on the numerals.
700: For instance, \cite[159]{Bernays:23b} writes that ``figures [i.e., numerals]
701: {\em are} not shapes, they {\em have} a shape.'' Thus it is the shape of the
702: numerals, and not the numerals themselves, which is supposed to be independent
703: of place and time, independent of the circumstances of production, independent
704: of inessential differences in execution, and capable of secure recognition in
705: all circumstances \cite[163]{Hilbert:22a}. Tait\index{Tait, W. W.} infers from
706: this that identity between numerals is type identity, and hence, that numerals
707: should be construed as types of stroke symbols.
708:
709: Types are ordinarily considered to be abstract objects and not located in
710: space or time. Taking the numerals as intuitive representations of sign types
711: might commit us to taking these abstract objects as existing independently of
712: their intuitive representation. That numerals are ``space- and timeless'' is
713: a consequence that already \cite[158]{Muller:23}\index{M\"uller, A.} thought
714: could be drawn from Hilbert's statements, and that was in turn denied by
715: Bernays\index{Bernays, P.}. The reason is that a view on which numerals are
716: space- and timeless objects existing independently of us would be committed to
717: them existing simultaneously as a completed totality, and this is exactly what
718: Hilbert is objecting to.
719: \begin{quote}
720: It is by no means compatible, however, with Hilbert's basic thoughts to
721: introduce the numbers as ideal objects ``with quite different determinations
722: from those of sensible objects,'' ``which exist entirely independent of
723: us.'' By this we would go beyond the domain of the immediately certain. In
724: particular, this would be evident in the fact that we would consequently
725: have to assume the numbers {\em as all existing simultaneously.} But this
726: would mean to assume at the outset that which Hilbert considers to be
727: problematic. \cite[225--26]{Bernays:23b}\index{Bernays, P.}
728: \end{quote}
729: This is not to say that it is {\em incoherent} to consider the numbers
730: as being abstract objects, only that the finitary viewpoint prohibits
731: such a view. Bernays\index{Bernays, P.} goes on to say:
732: \begin{quote}
733: Hilbert's theory does not exclude the possibility of a philosophical
734: attitude which conceives of the numbers [but not the finitist's numerals] as
735: existing, non-sensible objects (and thus the same kind of ideal existence
736: would then have to be attributed to transfinite numbers as well, and in
737: particular to the numbers of the so-called second number class).
738: Nevertheless the aim of Hilbert's theory is to make such an attitude
739: dispensable for the foundation of the exact sciences.
740: \cite[226]{Bernays:23b}
741: \end{quote}
742: Another open question in this regard is exactly what Hilbert meant by
743: ``concrete.'' He very likely did not use it in the same sense as it is used
744: today, i.e., as characteristic of spatio-temporal physical objects in contrast
745: to ``abstract''\index{abstract objects} objects. However, sign types certainly
746: are different from full-fledged abstracta like pure sets in that all their
747: tokens are concrete. Parsons takes account of this difference by using the
748: term ``quasi-concrete''\index{quasi-concrete} for such abstracta. Tait, on the
749: other hand, thinks that even the tokens are not concrete physical objects, but
750: abstract themselves.
751:
752: Now what is the epistemological status of the finitary objects? In order to
753: carry out the task of providing a secure foundation for infinitary
754: mathematics, access to finitary objects must be immediate and certain.
755: Hilbert's philosophical background was broadly Kantian, as was
756: Bernays\index{Bernays, P.}'s, who was closely affiliated with the neo-Kantian
757: school of philosophy around Leonard Nelson\index{Nelson, L.} in G\"ottingen.
758: Hilbert's characterization of finitism often refers to Kantian
759: intuition\index{intuition!Kantian}, and the objects of finitism as objects
760: given intuitively. Indeed, in Kant's epistemology, immediacy is a defining
761: characteristic of intuitive knowledge. The question is, what kind of
762: intuition is at play? \cite{Mancosu:98c}\index{Mancosu, P.} identifies a
763: shift in this regard. He argues that whereas the intuition involved in
764: Hilbert's early papers was a kind of perceptual intuition, in later writings
765: (e.g., \cite{Bernays:28b}\index{Bernays, P.}) it is identified as a form of
766: pure intuition\index{intuition!Kantian} in the Kantian sense. \cite[266--267]{Hilbert:31a} later sees
767: the finite mode of thought as a separate source of \emph{a priori} knowledge
768: in addition to pure intuition (e.g., of space) and reason, claiming that he
769: has ``recognized and characterized the third source of knowledge that
770: accompanies experience and logic.'' Both Bernays\index{Bernays, P.} and
771: Hilbert justify finitary knowledge in broadly Kantian terms (without however
772: going so far as to provide a transcendental deduction), characterizing
773: finitary reasoning as the kind of reasoning that underlies all mathematical,
774: and indeed, scientific, thinking, and without which such thought would be
775: impossible.\footnote{See \cite{Kitcher:76}\index{Kitcher, P.} and
776: \cite{Parsons:98}\index{Parsons, C.} for more discussion on the metaphysics
777: and epistemology of finitism, and \cite{Sieg:99}\index{Sieg, W.} for
778: historical remarks on the development of finitism.}
779:
780: The simplest finitary propositions are those about equality and inequality of
781: numerals. The finite standpoint moreover allows operations on finitary
782: objects. Here the most basic is that of concatenation. The concatenation of
783: the numerals $\mid\mid$ and $\mid\mid\mid$ is communicated as ``$2 + 3$,'' and
784: the statement that $\mid\mid$ concatenated with $\mid\mid\mid$ results in the
785: same numeral as $\mid\mid\mid$ concatenated with $\mid\mid$ by ``$2 + 3 = 3 +
786: 2$.'' In actual proof-theoretic practice, as well as explicitly in
787: \cite{Bernays:30,HilbertBernays:34}\index{Bernays, P.}, these basic operations
788: are generalized to operations defined by recursion, paradigmatically,
789: primitive recursion\index{primitive recursion}, e.g., multiplication and
790: exponentiation. Roughly, a primitive recursive definition of a numerical
791: operation is one in which the function to be defined, $f$, is given by two
792: equations
793: \begin{eqnarray*}
794: f(0, \mathfrak{m}) & = & g(\mathfrak{m}) \\
795: f(\mathfrak{n}', \mathfrak{m}) & = & h(\mathfrak{n}, \mathfrak{m},
796: f(\mathfrak{n}, \mathfrak{m})),
797: \end{eqnarray*}
798: where $g$ and $h$ are functions already defined, and $\mathfrak{n}'$ is the
799: successor numeral to $\mathfrak{n}$. Fraktur letters are used here, as in
800: Hilbert's writings, as meta-variables for numerals. For instance, if we accept
801: the function $g(\mathfrak{m}) = \mathfrak{m}$ (the constant function) and
802: $h(\mathfrak{n}, \mathfrak{m}, \mathfrak{k}) = \mathfrak{m} + \mathfrak{k}$ as
803: finitary, then the equations above define a finitary function, in this case,
804: multiplication $f(\mathfrak{n}, \mathfrak{m}) = \mathfrak{n} \times
805: \mathfrak{m}$.
806:
807: Similarly, finitary judgments may involve not just equality or inequality but
808: also basic decidable properties, such as ``is a prime.'' This is finitarily
809: acceptable as long as the characteristic function of such a property is itself
810: finitary: For instance, the operation which transforms a numeral to $\mid$ if
811: it is prime and to $\mid\mid$ otherwise can be defined by primitive recursion
812: and is hence finitary. Such finitary propositions may be combined by the
813: usual logical operations of conjunction, disjunction, negation, but also
814: bounded quantification. \cite{Hilbert:26} gives the example of the
815: proposition that ``there is a prime number between $\mathfrak{p} + 1$ and
816: $\mathfrak{p}! + 1$'' where $\mathfrak{p}$ is a certain large prime. This
817: statement is finitarily acceptable since it ``serves merely to abbreviate the
818: proposition'' that either $\mathfrak{p} + 1$ or $\mathfrak{p} + 2 $ or
819: $\mathfrak{p} + 3$ or \dots or $\mathfrak{p}! + 1$ is a prime.
820:
821: The problematic finitary propositions are those that express general facts
822: about numerals such as that $1 + \mathfrak{n} = \mathfrak{n} + 1$ for any
823: given numeral $\mathfrak{n}$. It is problematic because, as Hilbert puts it,
824: it ``is from the finitist point of view \emph{incapable of being negated}''
825: \cite[378]{Hilbert:26}. By this he means that the contradictory proposition
826: that there is a numeral $\mathfrak{n}$ for which $1 + \mathfrak{n} \neq
827: \mathfrak{n} + 1$ is not finitarily meaningful. ``One cannot, after all, try
828: out all numbers'' \cite[470]{Hilbert:28}. For the same reason, a finitary
829: general proposition is not to be understood as an infinite conjunction but
830: ``only as a hypothetical judgment that comes to assert something when a
831: numeral is given'' \cite[378]{Hilbert:26}. Even though they are problematic in
832: this sense, general finitary statements are of particular importance to
833: Hilbert's proof theory, since the statement of consistency of a formal system
834: $T$ is of such a general form: for any given sequence~$p$ of formulas, $p$ is
835: not a derivation of a contradiction in~$T$.
836:
837: Even though in general existential statements are not finitarily meaningful,
838: they may be \emph{given} finitary meaning if the witness is given by a
839: finitary function. For instance, the finitary content of Euclid's theorem
840: that for every prime $\mathfrak{p}$ there is a prime $> \mathfrak{p}$, is
841: that given a specific prime $\mathfrak{p}$ one can produce, by a finitary
842: operation, another prime $> \mathfrak{p}$ (viz., by testing all numbers
843: between $\mathfrak{p}$ and $\mathfrak{p}! + 1$. This view is discussed by
844: \cite{Bernays:30}\index{Bernays, P.} and plays an important role in the uses
845: \cite{Gentzen:36} and others make of proof theory.
846:
847: \subsection{Analyses of finitism}
848:
849: Hilbert's substantial philosophical claims about the finitary standpoint are
850: difficult to flesh out. For instance, Hilbert and Bernays\index{Bernays, P.}
851: both appeal to the role of Kantian intuition for our apprehension of finitary
852: objects (they are given in the faculty of representation). Supposing one
853: accepts this line of epistemic justification in principle, it is plausible
854: that the simplest examples of finitary objects and propositions, and perhaps
855: even simple cases of finitary operations such as concatenations of numerals
856: can be given a satisfactory account. However, it is unclear exactly which
857: more complex objects, propositions, and operations should be admitted as
858: finitary, and how the account can be extended to cover them. This has led to
859: substantial debate since the 1920s about the nature of finitary reasoning and
860: its justification.
861:
862: Of crucial importance to both an understanding of finitism and of Hilbert's
863: proof theory is the question of what operations and what principles of proof
864: should be allowed from the finitist standpoint. That a general answer is
865: necessary is clear from the demands of Hilbert's proof theory, i.e., it is not
866: to be expected that given a formal system of mathematics (or even a single
867: sequence of formulas) one can ``see'' that it is consistent (or that it cannot
868: be a genuine derivation of an inconsistency) the way we can see, e.g., that
869: ${\mid\mid} + {\mid\mid\mid} = {\mid\mid\mid} + {\mid\mid}$. What is required
870: for a consistency proof\index{consistency proof} is an operation which, given
871: a formal derivation, transforms such a derivation into one of a special form,
872: plus proofs that the operation in fact succeeds in every case and that proofs
873: of the special kind cannot be proofs of an inconsistency. To count as a
874: finitary consistency proof, the operation itself must be acceptable from the
875: finitist standpoint, and the proofs required must use only finitarily
876: acceptable principles.
877:
878: Hilbert never gave a general account of which operations and methods of proof
879: are acceptable from the finitist standpoint, but only examples of operations
880: and methods of inference in contentual finitary number theory which he
881: accepted as finitary. Contentual induction\index{induction!contentual} was
882: accepted in its application to finitary statements of the hypothetical,
883: general kind explicitly in \shortcite{Hilbert:22a}. \cite[1139]{Hilbert:23}
884: said that intuitive thought ``includes recursion and intuitive induction for
885: finite existing totalities,'' and used exponentiation in an example in
886: \citeyear{Hilbert:28}. \cite{Bernays:30}\index{Bernays, P.} explained how
887: exponentiation may be understood as a finitary operation on numerals.
888: \cite{HilbertBernays:34}\index{Bernays, P.} give the only general account of
889: finitary contentual number theory; according to it, operations defined by
890: primitive recursion and proofs using induction are finitarily acceptable. All
891: of these methods, in their application in the domain of numbers, can be
892: formalized in a system known as primitive recursive arithmetic\index{primitive
893: recursive arithmetic} (\emph{PRA}), which allows definitions of functions by
894: primitive recursion and induction on quantifier-free formulas. However,
895: neither Hilbert nor Bernays\index{Bernays, P.} ever claimed that \emph{only}
896: primitive recursive\index{primitive recursion!and finitism|(} operations count
897: as finitary, and non-primitive recursive methods were used in ostensibly
898: finitary consistency proofs already in 1923 (see \cite{Tait:02}\index{Tait, W.
899: W.} and \cite{Zach:03}\index{Zach, R.}). These include, in particular, the
900: consistency proof\index{consistency proof} of a formal system of number theory
901: corresponding to primitive recursive arithmetic in \cite{Hilbert:22b}, and a
902: stronger system in Ackermann\index{Ackermann, W.}'s dissertation
903: \cite{Ackermann:24}.\footnote{Ackermann in fact used transfinite
904: induction\index{induction!transfinite} up to $\omega^{\omega^\omega}$ to
905: justify a non-primitive recursive reduction procedure.}
906:
907: Although Hilbert and his collaborators used methods which go beyond the
908: primitive recursive and accepted them as finitary, it is still unclear whether
909: they (a) realized that these methods were not primitive recursive and (b)
910: whether they would still have accepted them as finitary if they
911: had.\footnote{See Tait's discussion in the Appendix to Chapters~1 and 2 in
912: \cite{Tait:05}.} The conceptual issue is which operations \emph{should} be
913: considered as finitary. Since Hilbert was less than completely clear on what
914: the finitary standpoint consists in, there is some leeway in setting up the
915: constraints, epistemological and otherwise, an analysis of finitist operation
916: and proof must fulfill. Hilbert characterized the objects of finitary number
917: theory as ``intuitively given,'' as ``surveyable in all their parts,'' and
918: said that their having basic properties must ``exist intuitively'' for us.
919: \cite[216]{Bernays:22}\index{Bernays, P.} suggests that in finitary
920: mathematics, only ``primitive intuitive cognitions come into play,'' and uses
921: the term ``point of view of intuitive evidence'' in connection with finitism
922: \cite[250]{Bernays:30}\index{Bernays, P.}. This characterization of finitism
923: as primarily to do with \emph{intuition}\index{intuition!and finitism} and
924: intuitive knowledge has been emphasized in particular by
925: \cite{Parsons:98}\index{Parsons, C.} who argues that what can count as
926: finitary on this understanding is not more than those arithmetical operations
927: that can be defined from addition and multiplication using bounded recursion.
928: In particular, according to Parsons, exponentiation and general primitive
929: recursion are not finitarily acceptable.
930:
931: The thesis that finitism coincides with primitive recursive
932: reasoning\index{primitive recursion} has
933: received a forceful and widely accepted defense by \cite{Tait:81}.
934: Tait\index{Tait, W. W.|(}, in contrast to Parsons\index{Parsons, C.}, rejects
935: the aspect of representability in intuition as the hallmark of the finitary;
936: instead he takes finitary reasoning to be ``a minimal kind of reasoning
937: supposed by all non-trivial mathematical reasoning about numbers'' and
938: analyzes finitary operations and methods of proof as those that are implicit
939: in the very notion of number as the form of a finite sequence. This analysis
940: of finitism is supported by Hilbert's contention that finitary reasoning is a
941: precondition for logical and mathematical, indeed, any scientific thinking
942: \cite[267]{Hilbert:31a}.\index{primitive recursion!and finitism|)} The crucial
943: difference between Tait's conception of finitism and Parsons (as well as
944: Hilbert's own) is that according to Tait there is no ultimate epistemological
945: foundation for finitism which yields the security of finitary reasoning for
946: which Hilbert appealed to intuition. Tait argues that
947: \begin{quote}
948: [\dots] no absolute conception of security is realized by finitism
949: or any other kind of mathematical reasoning. Rather, the special role
950: of finitism consists in the circumstance that it is a minimal kind of
951: reasoning presupposed by all nontrivial mathematical reasoning about
952: numbers. And for this reason it is \emph{indubitable} in a Cartesian
953: sense that there is no preferred or even equally preferable ground on
954: which to stand and criticize it. Thus finitism is fundamental to
955: number-theoretical mathematics even if it is not a foundation in the
956: sense Hilbert wished. \cite[525]{Tait:81}
957: \end{quote}
958:
959: Another interesting analysis of finitary proof, which, however, does not
960: provide as detailed a philosophical justification, was proposed by
961: \cite{Kreisel:58}\index{Kreisel, G.|(}. It yields the result that exactly
962: those functions are finitary which can be proved to be well-defined in
963: first-order arithmetic \emph{PA}.\footnote{\cite[Section
964: 3.5]{Kreisel:70}\index{Kreisel, G.} provides another analysis by focusing on
965: what is ``visualizable.'' The result is the same: finitary functions turn
966: out to be just those provably total in~\emph{PA}.} Kreisel's proposal makes
967: use of the notions of formalizations of provability predicates and ordinal
968: progressions of theories. Kreisel argues that if $\mathit{Pr}(\Godelnum{A})$
969: has been recognized to be a provability predicate for a partial formalization
970: $\Sigma_\mu$ of finitary reasoning, and
971: $\mathit{Pr}(\Godelnum{A(0^{(x)})})$\footnote{Here, $x$ is a free variable,
972: and $\Godelnum{A(0^{(x)})}$ is the function of $x$ which computes
973: $\Godelnum{A(0^{\prime\cdots\prime})}$ with $x$ occurrences of~$'$.} is
974: provable in $\Sigma_\mu$ (and hence established by finitary means), then the
975: finitist is entitled to also accept $A(x)$ as finitarily established. If that
976: is the case, we may add $A(x)$ as an axiom to $\Sigma_\mu$ to obtain a new
977: theory $\Sigma_\nu$ which is also finitarily justified. On Kreisel's account,
978: finitary provability coincides with the provability in some $\Sigma_\nu$ so
979: obtained, starting from $\Sigma_0 = \mathit{PRA}$\index{primitive recursive
980: arithmetic}. If some $\Sigma_\nu$ proves $\exists y\, A(x, y)$, for $A(x,
981: y)$ a primitive recursive equation, then $f(x) =$ the least $y$ such that
982: $A(x, y)$ is finitarily justified. Kreisel sketches a proof of the theorem
983: that the functions so justified are exactly those which are provably total in
984: $\mathit{PA}$, and hence there are finitary functions which are not primitive
985: recursive.
986:
987: \cite[\S13]{Tait:81} also contains a discussion of Kreisel's analysis. In
988: order to obtain a non-primitive recursive function on Kreisel's account, we
989: must properly extend~$\Sigma_0$ since the provably total functions of
990: $\Sigma_0 = \mathit{PRA}$\index{primitive recursive arithmetic} are just the
991: primitive recursive functions. So suppose we have that
992: $\mathit{PRA}$\index{primitive recursive arithmetic} proves the
993: arithmetization of the claim that $\exists y\, A(0^{(x)}, y)$ is
994: provable.\footnote{In other words, there are primitive recursive functions
995: $h(x)$ and $g(x)$ so that $\mathit{PRA}$ proves that $g(x)$ codes a
996: derivation in $\mathit{PRA}$ of the formula $\Godelnum{A(0^{(x)}, t)}$,
997: where $t$ is the primitive recursive term (containing only the free variable
998: $x$) which is coded by $h(x)$.} This, according to Kreisel, justifies the
999: acceptance of $f(x)$ as defined above as finitary, because a finitary proof of
1000: the general fact that it is provable in $\mathit{PRA}$ that $f(x)$ is defined,
1001: together with the acceptance of $\mathit{PRA}$\index{primitive recursive
1002: arithmetic} as finitarily acceptable, amounts to a finitary proof that
1003: $f(x)$ is defined for all~$x$. The weak point in this justification,
1004: according to Tait, is this:
1005: \begin{quote}
1006: For the finitist to recognize the validity of primitive recursive
1007: arithmetic, he must recognize the \emph{general} validity of definition of
1008: functions by primitive recursion. But he cannot even formulate this since
1009: it involves the notion of function.
1010: \end{quote}
1011: Tait's point here is that there is a significant difference between accepting
1012: each primitive recursive definition individually as finitary, and accepting
1013: primitive recursion in general as a finitarily valid principle. The finitist
1014: is able to do the former, but not the latter. For to accept primitive
1015: recursion in general as a finitarily valid principle of definition, one would
1016: either, as Tait puts it, need to invoke the notion of a function (which is not
1017: a finitary object), or one needs a justification for why, say, all primitive
1018: recursive \emph{terms} are calculable for every argument---and for this a
1019: finitary evaluation procedure for primitive recursive terms is necessary.
1020: Such an evaluation procedure, however, cannot be primitive recursive. And
1021: prior to the extension of $\mathit{PRA}$\index{primitive recursive arithmetic}
1022: to include the new non-primitive recursive function $f(x)$ there is no reason
1023: to suppose that such an evaluation procedure exists. Although Tait's
1024: objection is directed at Kreisel's analysis of finitary function, it of course
1025: also raises doubts about Kreisel's account of finitary proof.\index{Kreisel,
1026: G.|)}\index{finitism|)}\index{Tait, W. W.|)}
1027:
1028: \subsection{Hilbert's program and instrumentalism}
1029:
1030: Hilbert's program has often been interpreted as an
1031: instrumentalist\index{instrumentalism!and Hilbert's program|(}\index{Hilbert's
1032: program!and instrumentalism|(} account of mathematics. This reading relies
1033: on the distinction Hilbert makes between the finitary part of mathematics and
1034: the non-finitary rest which is in need of grounding (via finitary
1035: meta-mathematics). The finitary part Hilbert calls ``contentual,'' i.e., its
1036: propositions and proofs have content. The infinitary part, on the other hand,
1037: is ``not meaningful from a finitary point of view.'' This distinction
1038: corresponds to a distinction between formulas of the the axiomatic systems of
1039: mathematics for which consistency proofs\index{consistency proof} are being
1040: sought. Some of the formulas correspond to contentual, finitary propositions:
1041: they are the ``real'' formulas. The rest are called ``ideal.'' They are
1042: added to the real part of our mathematical theories in order to preserve
1043: classical inferences such as the principle of the excluded middle for infinite
1044: totalities, i.e., the principle that either all numbers have a given property
1045: or there is a number which does not have it. This disjunction is not
1046: finitarily valid, as we saw above. Hilbert first mentioned ``ideal''
1047: propositions in \shortcite{Hilbert:26}, although the distinction was hinted at
1048: in~\shortcite{Hilbert:23}. In the latter paper, Hilbert presented a formal
1049: system of quantifier-free number theory about which he says that ``the
1050: provable formulae we acquire in this way all have the character of the
1051: finite'' (1139). Then the transfinite axioms (i.e., quantifiers) are added to
1052: simplify and complete the theory (1144). Here he draws the analogy with the
1053: method of ideal elements: ``In my proof theory, the transfinite axioms and
1054: formulae are adjoined to the finite axioms, just as in the theory of complex
1055: variables the imaginary elements are adjoined to the real, and just as in
1056: geometry the ideal constructions are adjoined to the actual'' (ibid). When
1057: Hilbert, in \shortcite{Hilbert:26}, explicitly introduces the notion of an
1058: ideal proposition, and in \shortcite{Hilbert:28}, when he first speaks of
1059: \emph{real propositions} in addition to the ideal, he is quite clear that the
1060: real part of the theory consists only of decidable, variable-free formulas.
1061: They are supposed to be ``directly capable of verification''---akin to
1062: propositions derived from laws of nature which can be checked by experiment
1063: \cite[475]{Hilbert:28}.\footnote{This reading is not universally accepted.
1064: \cite{Detlefsen:90}, for instance, considers the real formulas to also
1065: include the general formulas, i.e., formulas with free variables. See
1066: \cite{Zach:02}\index{Zach, R.} for a defense of the reading given here.} It
1067: is this extension of the real part of the theory by the ideal, infinitary part
1068: that is in need of justification by a consistency proof\index{consistency
1069: proof}:
1070: \begin{quote}
1071: For there is a condition, a single but absolutely necessary one, to which
1072: the use of the method of ideal elements is subject, and that is the
1073: \emph{proof of consistency}; for, extension by the addition of ideals is
1074: legitimate only if no contradiction is thereby brought about in the old,
1075: narrower domain, that is, if the relations that result for the old objects
1076: whenever the ideal objects are eliminated are valid in the old domain.
1077: \cite[383]{Hilbert:26}
1078: \end{quote}
1079: \cite{Weyl:25}\index{Weyl, H.} described Hilbert's project as replacing
1080: meaningful mathematics by a meaningless game of formulas. He noted that
1081: Hilbert wanted to ``secure not \emph{truth}, but the \emph{consistency} of
1082: analysis'' and suggested a criticism that echoes an earlier one by
1083: Frege\index{Frege, G.}: Why should we take consistency of a formal system of
1084: mathematics as a reason to believe in the truth of the pre-formal mathematics
1085: it codifies? Is Hilbert's meaningless inventory of formulas not just ``the
1086: bloodless ghost of analysis''? Weyl\index{Weyl, H.} suggested a solution:
1087: \begin{quote}
1088: [I]f mathematics is to remain a serious cultural concern, then some
1089: \emph{sense} must be attached to Hilbert's game of formulae, and I see only
1090: one possibility of attributing to it (including its transfinite components)
1091: an independent intellectual meaning. In theoretical physics we have before
1092: us the great example of a [kind of] knowledge of completely different
1093: character than the common or phenomenal knowledge that expresses purely what
1094: is given in intuition. While in this case every judgment has its own sense
1095: that is completely realizable within intuition, this is by no means the case
1096: for the statements of theoretical physics. In that case it is rather
1097: \emph{the system as a whole} that is in question if confronted with
1098: experience. \cite[140]{Weyl:25}\index{Weyl, H.}
1099: \end{quote}
1100: The analogy with physics is striking. Hilbert himself used a similar analogy
1101: in \shortcite{Hilbert:28}. He there suggested that consistency is not the
1102: only virtue ideal mathematics has: transfinite inference simplifies and
1103: abbreviates proofs, ``brevity and economy of thought are the \emph{raison
1104: d'\^etre} of existence proofs'' (476). The formal system of transfinite
1105: logic is not arbitrary: ``This formula game is carried out according to
1106: certain definite rules, in which the \emph{technique of our thinking} is
1107: expressed. [...] The fundamental idea of my proof theory is none other than to
1108: describe the activity of our understanding, to make a protocol of the rules
1109: according to which our thinking actually proceeds'' (ibid).
1110:
1111: Although these remarks are suggestive, they do not force an interpretation of
1112: Hilbert as an instrumentalist. Most commentators have taken this reading
1113: (including \cite{Kitcher:76}\index{Kitcher, P.},
1114: \cite{Resnik:80}\index{Resnik, M.}, \cite{Giaquinto:83}\index{Giaquinto, M.},
1115: \cite{Sieg:90}\index{Sieg, W.}, and in particular \cite{Detlefsen:86}) in that
1116: they interpret Hilbert's explanation that the ideal propositions ``have no
1117: meaning in themselves'' \cite[381]{Hilbert:26} as claiming that classical
1118: mathematics is a \emph{mere} instrument, and that statements of transfinite
1119: mathematics have no truth value. To the extent that this is accurate,
1120: however, it must be understood as a methodological instrumentalism: A
1121: successful execution of the proof-theoretic program would show that one could
1122: pretend \emph{as if} mathematics was meaningless.\footnote{On this point see
1123: also \cite{Sieg:99}\index{Sieg, W.}, esp.~B3 and the conclusion, and
1124: \cite{Sieg:02}.} The analogy with physics is therefore not: transfinite
1125: propositions have no meaning just as propositions involving theoretical terms
1126: have no meaning, but: transfinite propositions require no direct intuitive
1127: meaning just as one does not have to directly see electrons in order to
1128: theorize about them. \cite{Hallett:90}\index{Hallett, M.}, taking into
1129: account the 19th century mathematical background from which Hilbert came as
1130: well as published and unpublished sources from Hilbert's entire career (in
1131: particular \cite{Hilbert:92}, the most extensive discussion of the method of
1132: ideal elements) comes to the following conclusion:
1133: \begin{quote}
1134: [Hilbert's treatment of philosophical questions] is \emph{not} meant as a
1135: kind of instrumentalist agnosticism about existence and truth and so forth.
1136: On the contrary, it is meant to provide a non-skeptical and positive
1137: solution to such problems, a solution couched in cognitively accessible
1138: terms. And, it appears, the same solution holds for both mathematical and
1139: physical theories. Once new concepts or ``ideal elements'' or new
1140: theoretical terms have been accepted, then they exist in the sense in which
1141: \emph{any} theoretical entities exist. \cite[239]{Hallett:90}\index{Hallett,
1142: M.}
1143: \end{quote}
1144: This conclusion is in line with Weyl\index{Weyl, H.}'s assessment in
1145: \shortcite{Weyl:28}. When Weyl eventually turned away from
1146: intuitionism\index{intuitionism},\footnote{For the reasons for Weyl's
1147: rejection of intuitionism, see \cite{Mancosu:02b}\index{Mancosu,
1148: P.}\index{Ryckman, T.}.} he
1149: emphasized the purpose of Hilbert's proof theory, not to turn mathematics into
1150: a meaningless game of symbols, but to turn it into a theoretical science which
1151: codifies scientific (mathematical) practice.
1152:
1153: The reading of Hilbert as an instrumentalist goes hand in hand with a reading
1154: of the proof-theoretic program as a reductionist project. The instrumentalist
1155: reading interprets ideal mathematics as a meaningless formalism, which
1156: simplifies and ``rounds out'' mathematical reasoning. But a consistency
1157: proof\index{consistency proof} of ideal mathematics by itself does not explain
1158: what ideal mathematics is an instrument \emph{for}. Thus, commentators have
1159: sought to elaborate on Hilbert's discussion of consistency by pointing out
1160: that consistency proofs\index{consistency proof} do not just establish that
1161: ideal theories are free from formal contradictions, but that they establish
1162: more than mere consistency. They establish
1163: \emph{conservativity}\index{conservativity|(} of the ideal over the real part
1164: of the theory, in the following sense: If the ideal theory proves a real
1165: statement, then the real statement is also provable by real, finitary means.
1166: Such reductivist projects were common in the philosophy of science at the
1167: time, as was pointed out by \cite{Giaquinto:83}\index{Giaquinto, M.}. A
1168: conservativity proof justifies the use of transfinite mathematics: it is not
1169: only internally consistent, but it proves only true intuitive propositions.
1170:
1171: On this picture, classical mathematics is to be formalized in a system which
1172: includes formalizations of all the directly verifiable (by calculation)
1173: propositions of contentual finite number theory. The consistency
1174: proof\index{consistency proof} should show that all real propositions which
1175: can be proved by ideal methods are true, i.e., can be directly verified by
1176: finite calculation. Actual proofs such as the
1177: $\epsilon$-substitution\index{epsilon substitution@$\epsilon$-substitution
1178: method} procedure are of such a kind: they provide finitary procedures which
1179: eliminate transfinite elements from proofs of real statements. In particular,
1180: they turn putative ideal derivations of $0 = 1$ into derivations in the real
1181: part of the theory; the impossibility of such a derivation establishes
1182: consistency of the theory. Indeed, Hilbert saw that something stronger is
1183: true: not only does a consistency proof\index{consistency proof} establish
1184: truth of real formulas provable by ideal methods, but it yields finitary
1185: proofs of finitary \emph{general} propositions if the corresponding
1186: free-variable formula is derivable by ideal methods \cite[474]{Hilbert:28}.
1187:
1188: It bears pointing out that Hilbert never clearly articulated conservativity of
1189: the ideal over the real for finitary general statements as an aim of his
1190: foundational project. There are contemporary commentators, e.g.,
1191: \cite{Neumann:31}\index{von Neumann, J.} who attribute to Hilbert an interest
1192: in conservativity proofs, but it was only Bernays\index{Bernays, P.} in the
1193: \emph{Grundlagen der Mathematik} who pointed out that consistency
1194: proofs\index{consistency proof} themselves established not only the truth of
1195: variable-free formulas provable by ideal methods, but also of free-variable
1196: theorems. In this context, Bernays\index{Bernays, P.} used the term
1197: `verifiable' (\emph{verifizierbar}): a free-variable formula $A(x)$ is
1198: verifiable if each numerical instance $A(\mathfrak{z})$ is (finitarily) true.
1199: The proof transformation methods used in consistency proofs\index{consistency
1200: proof} for systems of arithmetic in \cite[248,
1201: 298]{HilbertBernays:34}\index{Bernays, P.} can be applied not only to putative
1202: proofs of $0 = 1$, but generally to proofs of formulas with free-variables.
1203: If we have a proof of $A(x)$, then the following method constitutes a finitary
1204: proof that, for any $\mathfrak{z}$, $A(\mathfrak{z})$ is true. From the
1205: derivation of $A(x)$ we obtain a derivation of $A(\mathfrak{z})$ by
1206: substitution. The procedure given in the consistency proof\index{consistency
1207: proof} transforms this derivation into a variable-free derivation of
1208: $A(\frak{z})$ in the real part of the theory, which codifies a finitary
1209: calculation that $A(\mathfrak{z})$ is true.
1210:
1211: Kreisel\index{Kreisel, G.} was most influential in promoting the
1212: interpretation of the aim of Hilbert's program as an attempt to establish
1213: conservativity of the ideal theory for finitary general propositions all
1214: along. \cite{Kreisel:51} cites Bernays\index{Bernays, P.}'s results; but in
1215: \cite{Kreisel:58} and later, he instead points to an argument in
1216: \cite[474]{Hilbert:28}. This argument, unlike Bernays\index{Bernays, P.}'s,
1217: does not rely on a particular form of the consistency proof\index{consistency
1218: proof}. It assumes only that a finitary consistency proof for an ideal
1219: theory is available. Assume there is a derivation of $A(x)$. Now suppose
1220: that for a given $\mathfrak{z}$, $A(\frak{z})$ is not true. Then $\neg
1221: A(\mathfrak{z})$ would be true,\footnote{This inference uses tertium non
1222: datur, but only regarding the unproblematic finitary
1223: statement~$A(\mathfrak{z})$.} and so there would be a derivation of $\neg
1224: A(\mathfrak{z})$ in the ideal theory (which includes all real theorems). But
1225: from the derivation of $A(x)$ we obtain, by substitution, a derivation of
1226: $A(\mathfrak{z})$, and hence a contradiction. Since we assume that we have a
1227: finitary consistency proof of~$T$, this cannot be the case. Hence,
1228: $A(\mathfrak{z})$ must be true.\index{instrumentalism!and Hilbert's
1229: program|)}\index{Hilbert's program!and
1230: instrumentalism|)}\index{conservativity|)}
1231:
1232:
1233: \subsection{Hilbert's program and G\"odel's incompleteness theorems}
1234:
1235: G\"odel\index{G\"odel, K.} announced the second incompleteness
1236: theorem\index{incompleteness theorems|(}\index{incompleteness theorems!second
1237: incompleteness theorem} in an abstract published in October 1930: no
1238: consistency proof\index{consistency proof} of systems such as
1239: \emph{Principia}\index{Principia Mathematica}, Zermelo-Fraenkel set
1240: theory\index{set theory}, or the systems investigated by
1241: Ackermann\index{Ackermann, W.} and von Neumann\index{von Neumann, J.} is
1242: possible by methods which can be formulated in these systems. In the full
1243: version of his paper, \cite{Godel:31} left open the possibility that there
1244: could be finitary methods which are not formalizable in these systems and
1245: which would yield the required consistency proofs\index{consistency proof}.
1246: Bernays\index{Bernays, P.}'s first reaction in a letter to
1247: G\"odel\index{G\"odel, K.} in January 1931 was likewise that ``if, as von
1248: Neumann\index{von Neumann, J.} does, one takes it as certain that any and
1249: every finitary consideration may be formalized within the system $P$---like
1250: you, I regard that in no way as settled---one comes to the conclusion that a
1251: finitary demonstration of the consistency of $P$ is impossible''
1252: \cite[87]{Godel:03}.
1253:
1254: Through a careful (``G\"odel''-) coding of sequences of symbols (formulas,
1255: proofs) by numbers, G\"odel\index{G\"odel, K.} showed that in theories $T$
1256: which contain a sufficient amount of arithmetic, it is possible to produce a
1257: formula $\mathit{Pr}(x, y)$ which expresses that $x$ is (the code of) a proof
1258: of (the formula with code)~$y$. Specifically, if $\Godelnum{0 = 1}$ is the
1259: code of the formula $0 = 1$, then $\mathit{Con}_T \equiv \forall x\, \neg
1260: \mathit{Pr}(x, \Godelnum{0 = 1})$ expresses that $T$ is consistent (no number
1261: is the code of a derivation in $T$ of $0 = 1$). The second incompleteness
1262: theorem\index{incompleteness theorems!second incompleteness theorem} (G2) says
1263: that under certain assumptions about $T$ and the coding apparatus, $T$ does
1264: not prove $\mathit{Con}_T$. Now suppose there were a finitary consistency
1265: proof\index{consistency proof} of $T$. The methods used in such a proof would
1266: presumably be formalizable in~$T$. (``Formalizable'' means that, roughly, if
1267: the proof uses a finitary operation $f$ on derivations which transforms any
1268: derivation~$d$ into a derivation $f(d)$ of a simple form; then there is a
1269: formula~$F(x, y)$ so that, for all derivations $d$, $T \vdash F(\Godelnum{d},
1270: \Godelnum{f(d)})$.) The consistency of~$T$ would be finitarily expressed as
1271: the general hypothetical claim that, if $d$ is any given sequence of symbols,
1272: $d$ is not a derivation in $T$ of the formula~$0 = 1$. The formalization of
1273: this proposition is the formula $\neg \mathit{Pr}(x, \ulcorner 0 =
1274: 1\urcorner)$ in which the variable~$x$ occurs free. If there were a finitary
1275: proof of the consistency of~$T$, its formalization would yield a derivation in
1276: $T$ of $\neg \mathit{Pr}(x, \Godelnum{0 = 1})$, from which $Con_T$ can be
1277: derived in $T$ by simple universal generalization on~$x$. Yet, a derivation
1278: of $\mathit{Con}_T$ in $T$ is ruled out by G2.
1279:
1280: G\"odel\index{G\"odel, K.} and Bernays\index{Bernays, P.} initially thought
1281: that the difficulty for the consistency proof of Peano arithmetic
1282: $\mathit{PA}$\index{Peano arithmetic} could be overcome by employing methods
1283: which, although not formalizable in $\mathit{PA}$, are nonetheless finitary.
1284: Bernays\index{Bernays, P.} did not seem to have any particular candidates for
1285: such a method in mind, and he thought that all methods which were up to then
1286: employed in finitary considerations were in fact formalizable in
1287: $\mathit{PA}$. Another option he considered was an extension of the notion of
1288: an axiomatic theory by a finitary version of the $\omega$-rule\index{omega
1289: rule@$\omega$-rule} proposed by Hilbert \shortcite{Hilbert:31b,Hilbert:31a}.
1290: Such theories might avoid the impact of G\"odel\index{G\"odel, K.}'s
1291: incompleteness theorem since they do not satisfy the conditions of the
1292: incompleteness theorems: the set of axioms would not be decidable. It is fair
1293: to say, however, that since about 1934 it has been almost universally accepted
1294: that the methods of proof accepted as finitary prior to G\"odel\index{G\"odel,
1295: K.}'s results are all formalizable in \emph{PA} and that the incompleteness
1296: theorems do show that there can be no finitary consistency
1297: proofs\index{consistency proof} for axiomatic theories of the kind originally
1298: considered by Hilbert.
1299:
1300: The reaction to the incompleteness theorems in the Hilbert school then focused
1301: on extensions of the original finitary standpoint in which consistency
1302: proofs\index{consistency proof} for substantial theories like $\mathit{PA}$
1303: can be carried out. Such extensions have been proposed and defended on broadly
1304: finitary grounds, e.g., \cite{Gentzen:36} defended the use of transfinite
1305: induction up to $\epsilon_0$ in his consistency proof for \emph{PA} as
1306: ``indisputable,'' and \cite{Takeuti:87}\index{Takeuti, G.} gave another
1307: defense. In the Gentzen\index{Gentzen, G.}-Sch\"utte tradition of proof
1308: theory by ordinal analysis\index{ordinal analysis}, the proof methods used to
1309: give consistency proofs\index{consistency proof} are all of this sort. To wit,
1310: one uses transfinite induction on ordinal notation systems which name larger
1311: and larger ordinals. The more complicated the ordering, the more difficult it
1312: is to see that the induction principle in question is finitarily justified.
1313: Another extension of the finitary standpoint is due to \cite{Godel:58}.
1314:
1315: \cite{Smorynski:77}\index{Smory\'nski, C.}, following earlier suggestions by
1316: Kreisel\index{Kreisel, G.}, has argued that already the first incompleteness
1317: theorem\index{incompleteness theorems!first incompleteness theorem} defeats
1318: Hilbert's program. This argument uses the fact that a finitary consistency
1319: proof\index{consistency proof} of an ideal theory~$T$ implies the
1320: conservativity of~$T$ over finitary, real mathematics for general finitary
1321: statements of the form $A(x)$ (with free variable~$x$). Now
1322: G\"odel\index{G\"odel, K.}'s first incompleteness theorem (G1) states that for
1323: any sufficiently strong, consistent formal theory~$S$ there is a
1324: sentence~$G_S$ which is not derivable in~$S$ if $S$ is consistent. $G_S$ is a
1325: general real sentence. Consider a theory $T$ which formalizes ideal
1326: mathematics and contains the theory $S$, which formalizes real mathematics, as
1327: a subtheory. $S$ satisfies the conditions of G1 and hence $S$ does not
1328: derive~$G_S$. Yet~$T$, being a formalization of all of mathematics, proves
1329: (via a formalization of G1) that if $S$ is consistent, then $G_S$, but it also
1330: proves the consistency (indeed, the soundness) of $S$. Hence $T$ proves
1331: $G_S$. Thus, we have a true real statement which is provable in ideal
1332: mathematics but not in real mathematics.\footnote{The argument appeals to a
1333: number of perhaps contentious assumptions, such as that $T$ proves the
1334: soundness of $S$. For a critique, see~\cite{Detlefsen:90}\index{Detlefsen,
1335: M.}.}\index{incompleteness theorems|)}\index{Hilbert, D|)}
1336:
1337: \section{Hilbert's program now}
1338:
1339: \subsection{Detlefsen's Hilbertian instrumentalism}
1340:
1341: Detlefsen \shortcite{Detlefsen:79,Detlefsen:86,Detlefsen:01}\index{Detlefsen,
1342: M.|(}\index{instrumentalism!and Hilbert's program|(}\index{Hilbert's
1343: program!and instrumentalism|(} has proposed a wide-ranging instrumentalist
1344: account of mathematics based on Hilbert's program which is designed to escape
1345: the difficulties that G\"odel\index{G\"odel, K.}'s incompleteness
1346: theorems\index{incompleteness theorems} poses for Hilbert's original
1347: consistency project. The project has several parts: \cite{Detlefsen:86} first
1348: gives a detailed analysis and defense of a general instrumentalist view of
1349: mathematics along Hilbertian lines. This includes an analysis of the
1350: epistemic import of ideal proofs of real statements, which answers a question
1351: that was hardly addressed by Hilbert\index{Hilbert, D.}, either in his mature
1352: writings in the 1920s or in his exchange with Frege\index{Frege, G.} on
1353: formalism and consistency. This is the question of how manipulation of
1354: meaningless strings of symbols can ever lead to knowledge (of finitary
1355: truths). Detlefsen then analyzes the characteristics of formal systems of
1356: ideal mathematics \emph{qua} instruments. On Detlefsen's view, even though,
1357: say, full set theory is commonly accepted as a formalization of infinitary
1358: mathematics, only parts of set theory are in fact instrumentally useful. In
1359: particular, (1) ideal proofs of real theorems which are more complex than any
1360: real proof of the same theorem do not yield an instrumental advantage, and
1361: hence are not instrumentally useful; and (2) ideal proofs which are too long
1362: or complex to be comprehended by humans, and hence never play a role in actual
1363: mathematical reasoning, are also of no instrumental value. A proof theoretic
1364: justification of instrumental mathematics, i.e., the proof of the
1365: conservativity of the ideal theory over real mathematics, is only required, so
1366: Detlefsen, for the instrumentally useful part. Detlefsen introduces the term
1367: ``Hilbertian residue'' for that part of ideal mathematics that is
1368: instrumentally useful and hence in need of proof-theoretic justification. On
1369: his view, then, we only need a consistency proof\index{consistency proof} for
1370: the Hilbertian residue, not for all of ideal mathematics.
1371:
1372: This move from a required justification for all of infinitary
1373: mathematics to a justification of only the Hilbertian residue is one step
1374: toward Detlefsen's defense of instrumentalism against G\"odel\index{G\"odel,
1375: K.}'s incompleteness theorems\index{incompleteness theorems}. For the
1376: incompleteness theorems only apply under certain conditions, e.g., only when
1377: the theory in question contains enough basic arithmetic to carry out
1378: G\"odel\index{G\"odel, K.} coding, formalization of a proof predicate, and to
1379: prove the diagonal lemma. The Hilbertian residue of a theory, however, need
1380: not contain a sufficiently strong arithmetical subtheory because of (1) above.
1381: This provides part of Detlefsen's defense against the challenge posed by the
1382: first incompleteness theorem\index{incompleteness theorems!first
1383: incompleteness theorem} \cite[Appendix]{Detlefsen:86}. \cite{Detlefsen:90}
1384: also argues that instrumentalism escapes the argument from G1 by denying that
1385: ideal mathematics must be conservative over the real part. According to him,
1386: Hilbertian instrumentalism requires only that the ideal theory not prove
1387: anything which is in conflict with the real theory; it is not required that
1388: all its real theorems are also provable by real means. If this defense is
1389: successful, Detlefsen is right to claim that not G1, but only G2 poses a real
1390: challenge to instrumentalism.
1391:
1392: Detlefsen presents several lines of defense against the argument from G2, one
1393: of which \shortcite{Detlefsen:79} echoes \cite{Hilbert:31a}\index{Hilbert,
1394: D.}. If a version of the $\omega$-rule\index{omega rule@$\omega$-rule} is
1395: finitarily acceptable, then we would have found a finitarily acceptable method
1396: of proof which is not capable of formalization. Hence, real mathematics is
1397: not a subtheory of the ideal instrument, but this was an assumption necessary
1398: to draw the conclusion that there can be no real consistency
1399: proof\index{consistency proof} of the ideal theory.
1400: \cite{Ignjatovic:94}\index{Ignjatovi\v{c}, A.} raised serious doubts about the
1401: acceptability of Detlefsen's version of the $\omega$-rule, however.
1402: Detlefsen's other argument against the common interpretation of
1403: G\"odel\index{G\"odel, K.}'s second theorem focuses on the notion of
1404: formalization. That the particular formalization of ``$T$ is consistent'' by
1405: G\"odel\index{G\"odel, K.}'s formula $\mathit{Con}_T$ is not provable does not
1406: imply that there could not be other formulas, which \emph{are} provable
1407: in~$T$, and which have as much right to be called ``formalizations of the
1408: consistency of~$T$.'' These rely on different formalizations of the
1409: provability predicate $\mathit{Pr}_T$ than the standard ones. It is known
1410: that formalized consistency statements are unprovable whenever the provability
1411: predicate obeys certain general derivability conditions. Detlefsen argues
1412: that these conditions are not necessary for a predicate to count as a genuine
1413: provability predicate, and indeed there are provability predicates which
1414: violate the provability conditions and which give rise to consistency formulas
1415: which \emph{are} provable in their corresponding theories. These, however,
1416: depend on non-standard conceptions of provability which would likely not have
1417: been accepted by Hilbert\index{Hilbert, D.}. One quite basic example is the
1418: use of Rosser provability instead of ordinary provability. On this approach,
1419: a derivation of a formula $A$ only counts as a proof if no derivation with
1420: smaller G\"odel number is a derivation of $\lnot A$. If
1421: $\mathit{Prov}(x, \Godelnum{A})$ is the standard formalization of ``$x$ is the
1422: code of a derivation of the formula~$A$,'' then the Rosser
1423: provability\index{Rosser provability} predicate is given by
1424: \[
1425: \mathit{RPr}(\Godelnum{A}) \equiv \exists x(\mathit{Prov}(x, \Godelnum{A})
1426: \land \forall y<x\, \lnot \mathit{Prov}(y, \Godelnum{\lnot A})).
1427: \]
1428: For this provability predicate, $\lnot \mathit{RPr}(\Godelnum{0=1})$ \emph{is}
1429: provable in, e.g., first-order Peano arithmetic\index{Peano arithmetic}.
1430: Provability of a formula $A$, however, is no longer just a matter of deriving
1431: it from the axioms; one also has to check that all shorter derivations do not
1432: end in~$\lnot A$. Other ``consistency minded'' theories\index{consistency
1433: minded theory} which prove their own consistency are discussed, e.g., in
1434: \cite{Jeroslow:71,Jeroslow:75}\index{Jeroslow, R.} and especially
1435: \cite{Visser:89}\index{Visser, A.}. The Rosser provability predicate is
1436: studied in, e.g., \cite{Guaspari:79}\index{Guaspari, D.}\index{Solovay, R. M.}
1437: and \cite{Arai:90}\index{Arai, T.}.\footnote{For technical background,
1438: discussion of intensional provability predicates and examples, see
1439: \cite{Feferman:60}\index{Feferman, S.}. For discussion, see also
1440: \cite{Resnik:74a}, \cite{Auerbach:85,Auerbach:92}\index{Auerbach, D.} and
1441: \cite{Steiner:91}.}
1442:
1443: Another interesting aspect of Detlefsen's approach to instrumentalism and
1444: Hilbert's program related to technical work in proof theory is the emphasis on
1445: instrumental utility of ideal proofs. Hilbert\index{Hilbert, D.}, as we saw
1446: above, himself noted the theoretical and cognitive advantage of ideal methods,
1447: such as increased simplicity of proofs. In Detlefsen's instrumentalism, such
1448: considerations take center stage. Even if it is conceded that
1449: G\"odel\index{G\"odel, K.}'s theorems call the success of instrumentalism in
1450: its most general form into question, it would still be of substantial interest
1451: to study restricted cases of conservative extensions of real mathematics which
1452: are instrumentally useful. To flesh out the notion of ``instrumental
1453: usefulness,'' one obvious characteristic of formal proofs is length. For
1454: instance, one might take an ideal theory to be useful if its proofs are
1455: substantially shorter than proofs in, say, $\mathit{PRA}$\index{primitive
1456: recursive arithmetic} of the same theorems. This question is amenable to
1457: precise proof theoretical study. \cite{Ignjatovic:03}\index{Ignjatovi\v{c},
1458: A.}\index{Caldon, P.} prove some related, but on the whole, negative
1459: results: The subsystem of first-order arithmetic $I\Sigma_1$ in which
1460: induction is limited to $\Sigma_1$ formulas has super-exponential
1461: ``speed-up''\index{speed up}\index{proof theory!speed up} over
1462: \textit{PRA}\index{primitive recursive arithmetic}. This indicates that using
1463: induction over non-finitary formulas ($\Sigma_1$ formulas have unbounded
1464: existential quantifiers) yields significantly shorter proofs than proofs
1465: without. However, more comprehensive theories ($\mathit{RCA}$,
1466: $\mathit{WKL}$, see below) which contain some second-order apparatus, do not
1467: significantly shorten proofs vis-\`{a}-vis~$I\Sigma_1$.\index{Detlefsen,
1468: M.|)}\index{instrumentalism!and Hilbert's program|)}\index{Hilbert's
1469: program!and instrumentalism|)}
1470:
1471: \subsection{Generalized Hilbert programs}
1472:
1473: The work of Gentzen\index{Gentzen, G.} on consistency proofs\index{consistency
1474: proof} for mathematical theories using methods that go beyond the strictly
1475: finitary marks the beginning of an important line of proof-theoretic research.
1476: As outlined in \ref{impact-godel} above, Gentzen\index{Gentzen, G.}'s approach
1477: was to retain the aim of Hilbert's program, viz., to give consistency
1478: proofs\index{consistency proof} for strong mathematical theories by restricted
1479: means. Because of G\"odel\index{G\"odel, K.}'s incompleteness
1480: theorems\index{incompleteness theorems}, these restricted means are
1481: necessarily not themselves formalizable in the theories whose consistency is
1482: established by them. Nevertheless, they retain a constructive character, and
1483: attempts have been made to justify them on finitary grounds.
1484:
1485: The consistency proof\index{consistency proof} of \cite{Gentzen:36}, as
1486: discussed above, uses the principle of transfinite
1487: induction\index{induction!transfinite} up to~$\epsilon_0$\index{epsilon
1488: zero@$\epsilon_0$} in order to establish the consistency of first-order
1489: Peano arithmetic\index{Peano arithmetic}. Gentzen\index{Gentzen, G.}'s use of
1490: a system of notations for ordinals less than~$\epsilon_0$, and the proof of
1491: the termination of a reduction procedure for derivations in~$\mathit{PA}$
1492: based on induction on these ordinal notations, provide the model for the proof
1493: theoretic analysis of axiomatic systems along these lines. In order to give
1494: an ``ordinal analysis''\index{ordinal analysis}\index{proof theory!ordinal
1495: analysis} of a theory~$T$, one typically produces an ordinal notation system
1496: for ordinals less than some ordinal $\alpha$ such that for every $\beta <
1497: \alpha$, the formalization~$\mathit{TI}(\beta)$ of the transfinite
1498: induction\index{induction!transfinite} principle for~$\beta$ is provable
1499: in~$T$. In practice, using transfinite induction up to~$\alpha$ itself and
1500: otherwise only strictly finitary methods, one can prove the consistency
1501: of~$T$. The fact that induction up to $\epsilon_0$ establishes the
1502: consistency of $\mathit{PA}$, together with the result of \cite{Gentzen:43}
1503: that shows that for all $\beta < \epsilon_0$, $\mathit{PA}$ proves
1504: $\mathit{TI}(\beta)$ for all $\beta < \epsilon_0$ constitutes an ordinal
1505: analysis of~$\mathit{PA}$, and we say that $\epsilon_0$ is the proof theoretic
1506: ordinal of~$\mathit{PA}$.
1507:
1508: Proof theory in the tradition of Gentzen\index{Gentzen, G.} and
1509: Sch\"utte\index{Sch\"utte, K.} as well as Takeuti\index{Takeuti, G.} has
1510: focused on such ordinal analyses of theories of increasing strength. In
1511: recent work, Rathjen\index{Rathjen, M.} \shortcite{Rathjen:05a,Rathjen:05b}
1512: has pushed the boundaries of this approach in giving an ordinal analysis of a
1513: very strong subsystem of analysis called $\Pi_2^1$-comprehension.\footnote{See
1514: \cite{Pohlers:87}\index{Pohlers, W.} for a survey of the work in the
1515: Sch\"utte school, and \cite{Pohlers:98} for a more recent technical survey.}
1516: The consistency proofs in this tradition are, for the most part, based on the
1517: approach of \cite{Schutte:60}\index{Sch\"utte, K.}, which uses a variant of
1518: Gentzen\index{Gentzen, G.}'s formalization using infinitary derivations. A
1519: second tradition has pursued ordinal analysis using extensions of
1520: Ackermann\index{Ackermann, W.}'s $\epsilon$-substitution method\index{epsilon
1521: substitution@$\epsilon$-substitution method}
1522: \shortcite{Ackermann:40}\index{Ackermann, W.}, for examples see
1523: \cite{Mints:99}\index{Mints, G.}\index{Tupailo, S.} and
1524: \cite{Arai:03}\index{Arai, T.}.
1525:
1526: Although generalized Hilbert programs in this tradition have certainly
1527: produced important mathematical work, its philosophical underpinnings are
1528: thin. \cite{Takeuti:87} attempted to give a finitary justification for the
1529: proof theoretic ordinal~$\epsilon_0$\index{epsilon zero@$\epsilon_0$}, but it
1530: is unclear to what extent more complex ordinal notation systems are finitarily
1531: acceptable. Even if one concedes, as, e.g., Sch\"utte\index{Sch\"utte, K.}
1532: does, that the consistency proofs\index{consistency proof} in question are
1533: constructive (although no longer strictly finitary), it is still unclear what
1534: the philosophical significance of the technical results is.
1535: \cite[366]{Feferman:88a}\index{Feferman, S.} offers this assessment:
1536: \begin{quote}
1537: [A]s the systems of ordinal notation used for consistency proofs of stronger
1538: and stronger theories become more and more complicated, the significance to
1539: noncognoscenti of what is thereby accomplished decreases in inverse
1540: proportion. Thus, on the one hand, to say that one has obtained a
1541: constructive consistency proof\index{consistency proof} of a
1542: theory~$T$---without saying anything more---is too general to be
1543: informative; and, on the other hand, to say that the proof has been carried
1544: out by transfinite induction on a certain complicated recursive ordering for
1545: some very large ordinal tells us nothing about what constructive principles
1546: are involved in the proof of this well-ordering.\footnote{For a more
1547: forceful criticism of proof theory in this tradition, see
1548: \cite{Kreisel:76}\index{Kreisel, G.}.}
1549: \end{quote}
1550:
1551: Another important proof-theoretical approach in which the analysis of systems
1552: of classical mathematics is accomplished using a generalization of the
1553: finitary standpoint is that of functional interpretations\index{functional
1554: interpretation|(}. The model for this approach is G\"odel\index{G\"odel,
1555: K.}'s \emph{Dialectica} interpretation\index{Dialectica interpretation|(}
1556: \shortcite{Godel:58}. The \emph{Dialectica} interpretation shows how one can
1557: reduce an infinitary theory~$T$ (in this case, intuitionistic first-order
1558: arithmetic) to a quantifier-free theory~$F$.\footnote{Via the interpretation
1559: of classical arithmetic in intuitionistic arithmetic
1560: \cite{Gentzen:33,Godel:33b}\index{Gentzen, G.}, the \emph{Dialectica}
1561: interpretation also yields a functional interpretation of classical
1562: arithmetic.} An ordinal analysis of a theory does something similar, for
1563: instance, one can view Gentzen\index{Gentzen, G.}'s consistency
1564: proof\index{consistency proof} as reducing Peano arithmetic\index{Peano
1565: arithmetic} to a quantifier-free theory (\textit{PRA}\index{primitive
1566: recursive arithmetic}) extended by a certain infinitary induction principle
1567: ($\mathit{TI}(\epsilon_0)$). In the case of functional interpretations, the
1568: quantifier-free theory~$F$ is also not strictly finitary: it does not
1569: just mention finite objects but also certain infinitary objects, viz.,
1570: functionals of finite type. A functional interpretation can be seen as a
1571: reduction of the infinitary theory~$T$ to the theory of functionals~$F$ in
1572: question. The approach using functional interpretations has the following
1573: advantage over the Gentzen\index{Gentzen, G.}-Sch\"utte approach. It is a
1574: consequence of the reduction of $T$ to $F$ that every recursive function which
1575: can be proved to be total in~$T$ is represented by a term of~$F$. Because the
1576: functionals of~$F$ in practice characterize natural classes of functions, a
1577: functional interpretation yields an appealing analysis of the computational
1578: content of~$F$. Moreover, the conceptual import of the reduction is more
1579: apparent than in the case of ordinal analysis: already in the case of
1580: $\mathit{PA}$, G\"odel\index{G\"odel, K.}'s functionals of finite type provide
1581: a much clearer account of the character of the constructive methods appealed
1582: to than induction up to~$\epsilon_0$.\footnote{For an excellent survey of this
1583: approach, see \cite{Avigad:98}\index{Avigad, J.}\index{Feferman,
1584: S.}.}\index{Dialectica interpretation|)}\index{functional
1585: interpretation|)}
1586:
1587: \subsection{Relativized Hilbert programs}\label{relativized-hp}
1588:
1589: A philosophically more satisfactory continuation of Hilbert's program in proof
1590: theoretic terms has been suggested by Kreisel\index{Kreisel, G.}
1591: \shortcite{Kreisel:54,Kreisel:68,Kreisel:83} and has been elaborated
1592: especially by Feferman\index{Feferman, S.}. This work proceeds from a wider
1593: conception of Hilbert's program as an attempt to justify ideal mathematics by
1594: restricted means. On this conception, the aim of Hilbert's proof theory was
1595: to show that, at least as far as a certain class of real propositions is
1596: concerned, ideal mathematics does not go beyond real mathematics, and in this
1597: sense finitary mathematics is a foundation for ideal mathematics. A finitary
1598: consistency proof\index{consistency proof} of the kind envisaged by
1599: Hilbert\index{Hilbert, D.} would have accomplished this for all of classical
1600: mathematics.
1601:
1602: The scope of the foundational project, however, need not necessarily be all of
1603: higher mathematics. So-called relativized Hilbert programs are projects in
1604: which one considers certain fragments of higher mathematics as the theory for
1605: which a foundation is sought (and indeed, also theories stronger than finitism
1606: as candidates for the reducing theory, e.g., predicative theories). Examples
1607: of these are Feferman\index{Feferman, S.}'s work on explicit
1608: mathematics\index{explicit mathematics} and predicative subsystems of
1609: analysis, and to some extent also the Friedman-Simpson program of reverse
1610: mathematics (see below). What is common to these approaches to mathematical
1611: foundations is that they concentrate on so-called proof-theoretic reductions
1612: of systems of classical mathematics to more restricted systems. The reduction
1613: is carried out using finitist means, and therein lies its philosophical
1614: significance.
1615:
1616: A foundational reduction\index{foundational reduction|(} in
1617: Feferman's\index{Feferman, S.|(} sense \shortcite{Feferman:88a,Feferman:93} is
1618: accomplished if it can be shown that a body of mathematics which is justified
1619: by a foundational framework ${\cal F}_1$ (e.g, finitary, constructive,
1620: predicative, infinitary, set-theoretic) can already be justified, in a certain
1621: sense, in a weaker, or stricter foundational framework ${\cal F}_2$. This is
1622: in general not possible in a wholesale fashion, however, partial foundational
1623: reductions can and have been achieved. Suppose a theory $T_1$ is justified by
1624: a foundational framework ${\cal F}_1$, and a theory $T_2$ by a weaker
1625: framework ${\cal F}_2$. A proof theoretic reduction\index{proof theory!proof
1626: theoretic reduction} of $T_1$ to $T_2$ (conservative for $\Phi$) is a
1627: partial recursive function $f$ such that
1628: \begin{enumerate}
1629: \item Whenever $x$ is (the code of) a proof in $T_1$ of a formula
1630: (with code) $y$ in $\Phi$, then $f(x)$ is (the code of) a proof of $y$
1631: in $T_2$, and
1632: \item $T_2$ proves the formalization of (1).
1633: \end{enumerate}
1634: If there is such a function $f$, we write $T_1 \leq T_2 [\Phi]$. Now if $T_1$
1635: is directly justified by a foundational framework ${\cal F}_1$, and $T_2$ by
1636: ${\cal F}_2$, then, so Feferman\index{Feferman, S.}, a proof-theoretic
1637: reduction that establishes $T_1 \leq T_2 [\Phi]$ is a partial foundational
1638: reduction of ${\cal F}_1$ to ${\cal F}_2$. Clause (2) in the definition
1639: ensures that the reduction (the function~$f$) itself is justified by the
1640: weaker framework ${\cal F}_2$. In the reductions achieved in practice, it
1641: turns out that $f$ is actually primitive recursive and the formalization of
1642: (1) can even be proved in primitive recursive arithmetic
1643: $\mathit{PRA}$\index{primitive recursive arithmetic}. Since
1644: $\mathit{PRA}$\index{primitive recursive arithmetic} is directly justified by
1645: the finitary framework, such partial foundational reductions are therefore all
1646: finitarily justified. Feferman's\index{Feferman, S.} main philosophical
1647: conclusion from the possibility of giving such foundational reductions is
1648: this: The main argument for set-theoretical realism is the
1649: Quine-Putnam\index{Quine, W. V. O.}\index{Putnam, H.} indispensability
1650: argument\index{indispensability argument}, which proceeds from the premises
1651: that set-theory is indispensable to science. Feferman has shown, first, that
1652: much, if not all, of scientifically applicable mathematics can actually be
1653: formalized in much weaker systems (e.g., Feferman's system $W$, which is
1654: justified by a predicative foundational framework), and second, that
1655: predicative mathematics can be reduced to the countably infinite (in the sense
1656: that there is a partial foundational reduction of predicative mathematics to
1657: countably infinite mathematics, given by a proof-theoretic reduction of $W$ to
1658: Peano Arithmetic~\textit{PA})\index{Peano arithmetic}. He concludes that,
1659: \begin{quote}
1660: even if one accepts the indispensability argument, practically nothing
1661: philosophically definite can be said of the entities which are then supposed
1662: to have the same status---ontologically and epistemologically---as the
1663: entities of natural science. That being the case, what do the
1664: indispensability arguments amount to? As far as I'm concerned, they are
1665: completely vitiated. \cite{Feferman:93a}
1666: \end{quote}
1667: Independently of the question of mathematical realism and of the scope and
1668: force of the indispensability arguments, proof-theoretic reductions give
1669: precise answers to questions of the relation between foundational frameworks.
1670: Since a proof-theoretic reduction of $T_1$ to $T_2$ also yields a consistency
1671: proof\index{consistency proof} of $T_1$ in $T_2$ (i.e., a relative consistency
1672: result), establishing a proof-theoretic reduction also provides a solution to
1673: Hilbert's program relativized to $T_1$ and $T_2$. Feferman summarizes the
1674: importance of proof-theoretic reductions thus:
1675: \begin{quote}
1676: In general, the kinds of results presented here serve to sharpen what is to
1677: be said in favor of, or in opposition to, the various philosophies of
1678: mathematics such as finitism, predicativism, constructivism, and
1679: set-theoretical realism. Whether or not one takes one or another of these
1680: philosophies seriously for ontological and/or epistemological reasons, it is
1681: important to know which parts of mathematics are in the end justifiable on
1682: the basis of the respective philosophies and which are not. The uninformed
1683: common view---that adopting one of the non-platonistic positions means
1684: pretty much giving up mathematics as we know it---needs to be drastically
1685: corrected, and that should also no longer serve as the last-ditch stand of
1686: set-theoretical realism. On the other hand, would-be nonplatonists must
1687: recognize the now clearly marked sacrifices required by such a commitment
1688: and should have well-thought out reasons for making them. \cite{Feferman:93}
1689: \end{quote}
1690: Proof theorists have obtained a number of such results, including reductions
1691: of theories which on their face require a significant amount of ideal
1692: mathematics for their justification (e.g., subsystems of analysis) to finitary
1693: systems.\footnote{For a discussion of the philosophical significance of such
1694: proof theoretic reductions, see \cite{Feferman:00} and
1695: \cite{Hofweber:00}\index{Hofweber, T.}.}\index{Feferman,
1696: S.|)}\index{foundational reduction|)}
1697:
1698: The program of so-called reverse mathematics\index{proof theory!reverse
1699: mathematics}\index{reverse mathemtaics}
1700: developed by, in particular, Friedman\index{Friedman, H.} and
1701: Simpson\index{Simpson, S.}, is another continuation of Hilbert's program. In
1702: the face of G\"odel\index{G\"odel, K.}'s results showing that not all of
1703: classical mathematics can be reduced to the finitary, they seek to answer the
1704: question: how much of classical mathematics can be so reduced? Reverse
1705: mathematics aims to give a precise answer to this question by investigating
1706: which theorems of classical mathematics are provable in weak subsystems of
1707: analysis which are reducible to finitary mathematics (in the sense discussed
1708: above). A typical result is that the Hahn-Banach theorem
1709: of functional analysis is provable in a theory known as $WKL_0$ (for ``weak
1710: K\"onig lemma''); $WKL_0$ is proof-theoretically reducible to
1711: $PRA$\index{primitive recursive arithmetic} for $\Pi^0_2$ sentences (i.e.,
1712: sentences of the form $\forall x\exists y\, A(x, y)$.\footnote{See
1713: \cite{Simpson:88} for an overview, \cite{Simpson:99} for a technical
1714: introduction to reverse mathematics, and also the collection
1715: \cite{Simpson:05}.}
1716:
1717: Reverse mathematics in this tradition is primarily concerned with infinitary
1718: theories, e.g., subsystems of analysis. G\"odel's theorems show, however,
1719: that not even all truths of first-order number theory are provable in Peano
1720: arithmetic\index{Peano arithmetic}, and hence that not even the domain of all
1721: arithmetical truths can be given a foundation on finitary principles. This
1722: suggests the questions of whether there are ``mathematically interesting''
1723: statements of number theory which are not provable in systems that can be
1724: reduced to the finitary. The most celebrated result in this regard is the
1725: proof by \cite{Paris:77}\index{Paris, J.}\index{Harrington, L.} that a version
1726: of the finite Ramsey theorem is not provable in Peano arithmetic\index{Peano
1727: arithmetic}. However, this and other examples of independent number
1728: theoretic statements are constructed specifically to be independent of Peano
1729: arithmetic. It turns out that a great many ``ordinary'' number theoretic
1730: results are provable even in weak fragments of first-order number theory, and
1731: this has led Friedman to conjecture that ``every theorem published in the
1732: \emph{Annals of Mathematics} whose statement involves only finitary
1733: mathematical objects (i.e., what logicians call an arithmetical statement) can
1734: be proved in elementary arithmetic.'' (Here, elementary arithmetic is a very
1735: weak theory which can be proved consistent by primitive recursive methods.)
1736: \cite{Avigad:03}\index{Avigad, J.} gives an excellent survey of the issues and
1737: results related to this conjecture and places it in the philosophical context
1738: of Hilbert's program.\footnote{See also \cite{Raatikainen:03} on the current
1739: status of the various branches of proof-theoretic research relating to
1740: Hilbert's program.}
1741:
1742: The results surveyed in theis section are all natural continuations of
1743: Hilbert's\index{Hilbert, D.} original ideas. A central aspect recent
1744: proof-theoretical investigations and of Hilbert's original program alike that
1745: they study formalized systems using meta-mathematical tools with the aim of
1746: understanding the structure and content of these systems. Hilbert's original
1747: consistency project, the conservativity project that Kreisel\index{Kreisel,
1748: G.} and others interpret Hilbert as having been engaged in, as well as
1749: reductive proof theory are all examples of this, and this is also part of the
1750: reason why many practicing proof theorists see themselves as still working on
1751: Hilbert's program. Ordinal analysis, functional interpretations, proof
1752: theoretic reductions and reverse mathematics are only some of the most
1753: prominent areas of proof theory, and those most explicitly situated in the
1754: tradition of Hilbert's program. Many other areas of proof theory other than
1755: those directly concerned with consistency and foundational reductions of
1756: theories are related to the aims of Hilbert's program, e.g., the
1757: no-counterexample interpretation\index{no-counterexample interpretation}
1758: \cite{Kreisel:51,Tait:05a}\index{Tait, W. W.} and work on the structure and
1759: complexity of formal proofs\index{proof theory!complexity of proofs} more
1760: generally \cite{Pudlak:98}\index{Pudl\'ak, P.}.
1761:
1762:
1763: \section{Conclusion}
1764:
1765: Although it has been a commonplace in the literature on the philosophy of
1766: mathematics and logic from 1950 onward that Hilbert's program has not only
1767: been ``killed'' by G\"odel\index{G\"odel, K.}'s incompleteness
1768: theorems\index{incompleteness theorems} but that it was over-ambitions if not
1769: ill-conceived from the start, in the current literature a more positive
1770: evaluation has emerged. This is in large part due to the attention which
1771: unpublished writings in the Hilbert school (especially lecture notes to
1772: Hilbert's\index{Hilbert, D.} courses) have received recently, as well as to
1773: the availability of more of the published writings in English translation
1774: (e.g., in \cite{Ewald:96} and \cite{Mancosu:98}). But it is also due to a
1775: growing recognition that the common characterizations of Hilbert's program are
1776: a caricature, and to a clearer philosophical engagement with the recent
1777: results of proof theory. For instance, Ramsey's characterization that,
1778: according to Hilbert, ``Mathematics proper is thus regarded as a sort of game,
1779: played with meaningless marks on paper rather like noughts and crosses''
1780: \cite[231]{Ramsey:26}\index{Ramsey, F. P.}, and the view that Hilbert held a
1781: naive formalist and instrumentalist view of mathematics have been criticized
1782: by various writers. It remains to be seen in what ways Hilbert's
1783: philosophical views can be resuscitated (in the manner in which, e.g.,
1784: Frege\index{Frege, G.}'s logicist program has experienced a renaissance in the
1785: neo-logicist writings of, e.g., Boolos\index{Boolos, G.}, Heck\index{Heck,
1786: R.}, and Hale\index{Hale, B.} and Wright\index{Wright, C.}). It should be
1787: clear in any case from the discussion in the preceding section that ideas
1788: closely related to Hilbert's own \emph{have} been hugely successful. And it
1789: is also clear from the recent historical studies of Hilbert's unpublished
1790: writings as well as from the study of the proof theoretical practice of the
1791: Hilbert school that the ideas which underpin much of recent and current
1792: proof theoretical research are not merely ``inspired by'' Hilbert's program.
1793: Hilbert's fundamental aim was, all along, to make mathematical reasoning
1794: amenable to mathematical investigation, and to carry out such an investigation
1795: which yields an analysis of non-constructive reasoning in terms of restricted
1796: methods. Hilbert, of course, emphasized consistency of non-constructive
1797: systems as the most interesting property to be investigated, and emphasized
1798: finitary methods as those in terms of which such an analysis should be carried
1799: out. But even in the 1920s, in the practice of consistency
1800: proofs\index{consistency proof} in the work of Ackermann\index{Ackermann, W.},
1801: Bernays\index{Bernays, P.}, and von Neumann\index{von Neumann, J.}, among
1802: others, more broadly constructive methods were employed in this analysis, and
1803: results about properties other than consistency were obtained.
1804: Gentzen\index{Gentzen, G.}'s work of the 1930s and subsequent proof
1805: theoretical studies should thus not be seen as merely a response to
1806: G\"odel\index{G\"odel, K.}'s incompleteness results\index{incompleteness
1807: theorems}, but more broadly as advancing Hilbert's original aim of
1808: investigating the structure of mathematical reasoning. Seen in this light,
1809: again, proof theory as a foundational enterprise is very much alive. Although
1810: G\"odel\index{G\"odel, K.}'s theorems show that Hilbert's original
1811: expectations about what exactly can be analyzed in which way and with what
1812: restricted methods can not be fulfilled, proof theory and Hilbert's aims more
1813: generally have been advanced tremendously over the last
1814: half-century.\index{Hilbert's program|)}
1815:
1816: \subsection*{Acknowledgements}
1817:
1818: This paper is a substantially revised and expanded version of my entry in the
1819: \emph{Stanford Encyclopedia of Philosophy} \cite{Zach:03a}. I would like to
1820: acknowledge the support of the Social Sciences and Humanities Research Council
1821: of Canada, as well as helpful comments from Jeremy Avigad, Aleksandar
1822: Ignjatovi\v{c}, Paolo Mancosu, and William Tait.
1823:
1824: \begin{thebibliography}{}
1825:
1826: \bibitem[\protect\citeauthoryear{Ackermann}{1925}]{Ackermann:24}
1827: Wilhelm Ackermann.
1828: \newblock Begr\"undung des ``tertium non datur'' mittels der {H}ilbertschen
1829: {T}heorie der {W}iderspruchsfreiheit.
1830: \newblock {\em Mathe\-ma\-tische An\-nalen}, 93:1--36, 1925.
1831:
1832: \bibitem[\protect\citeauthoryear{Ackermann}{1940}]{Ackermann:40}
1833: Wilhelm Ackermann.
1834: \newblock Zur {W}iderspruchsfreiheit der {Z}ahlentheorie.
1835: \newblock {\em Mathe\-ma\-tische An\-nalen}, 117:162--194, 1940.
1836:
1837: \bibitem[\protect\citeauthoryear{Arai}{1990}]{Arai:90}
1838: Toshiyasu Arai.
1839: \newblock Derivability conditions on {R}osser's provability predicates.
1840: \newblock {\em Notre Dame Journal of Formal Logic}, 31:487--497, 1990.
1841:
1842: \bibitem[\protect\citeauthoryear{Arai}{2003}]{Arai:03}
1843: Toshiyasu Arai.
1844: \newblock Epsilon substitution method for
1845: ${ID}_{1}({\Pi}^{0}_{1}\lor{\Sigma}_{1}^{0})$.
1846: \newblock {\em Annals of Pure and Applied Logic}, 121:163--208, 2003.
1847:
1848: \bibitem[\protect\citeauthoryear{Auerbach}{1985}]{Auerbach:85}
1849: David Auerbach.
1850: \newblock Intentionality and the {G}\"odel theorems.
1851: \newblock {\em Philosophical Studies}, 48:337--351, 1985.
1852:
1853: \bibitem[\protect\citeauthoryear{Auerbach}{1992}]{Auerbach:92}
1854: David Auerbach.
1855: \newblock How to say things with formalisms.
1856: \newblock In Michael Detlefsen, editor, {\em Proof, Logic, and Formalization},
1857: pages 77--93. Routledge, London, 1992.
1858:
1859: \bibitem[\protect\citeauthoryear{Avigad and Feferman}{1998}]{Avigad:98}
1860: Jeremy Avigad and Solomon Feferman.
1861: \newblock G\"odel's functional (``{D}ialectica'') interpretation.
1862: \newblock In Buss \shortcite{Buss:98}.
1863:
1864: \bibitem[\protect\citeauthoryear{Avigad and Reck}{2001}]{Avigad:01}
1865: Jeremy Avigad and Erich Reck.
1866: \newblock ``clarifying the nature of the infinite'': the development of
1867: metamathematics and proof theory.
1868: \newblock Technical report cmu-phil-120, Carnegie Mellon University, 2001.
1869: \newblock Online at http://www.andrew.cmu.edu/user/avigad/Papers/infinite.pdf.
1870:
1871: \bibitem[\protect\citeauthoryear{Avigad and Zach}{2002}]{Avigad:02}
1872: Jeremy Avigad and Richard Zach.
1873: \newblock The epsilon calculus.
1874: \newblock In Edward~N. Zalta, editor, {\em The Stanford Encyclopedia of
1875: Philosophy}. Summer 2002.
1876: \newblock http://plato.stanford.edu/entries/epsilon-calculus/.
1877:
1878: \bibitem[\protect\citeauthoryear{Avigad}{2003}]{Avigad:03}
1879: Jeremy Avigad.
1880: \newblock Number theory and elementary arithmetic.
1881: \newblock {\em Philosophia Mathematica}, 11:257--284, 2003.
1882:
1883: \bibitem[\protect\citeauthoryear{Barwise}{1977}]{Barwise:77}
1884: Jon Barwise, editor.
1885: \newblock {\em Handbook of Mathematical Logic}.
1886: \newblock North-Holland, Amsterdam, 1977.
1887:
1888: \bibitem[\protect\citeauthoryear{Benacerraf and Putnam}{1983}]{Benacerraf:83}
1889: Paul Benacerraf and Hilary Putnam, editors.
1890: \newblock {\em Philosophy of Mathematics}.
1891: \newblock Cambridge University Press, Cambridge, 2nd edition, 1983.
1892:
1893: \bibitem[\protect\citeauthoryear{Bernays}{1922}]{Bernays:22}
1894: Paul Bernays.
1895: \newblock {\"U}ber {H}ilberts {G}edanken zur {G}rundlegung der {A}rithmetik.
1896: \newblock {\em Jahres\-bericht der Deut\-schen Mathe\-matiker-Ver\-eini\-gung},
1897: 31:10--19, 1922.
1898: \newblock {E}nglish translation in \Bcite{\pp{215--222}}{Mancosu:98}.
1899:
1900: \bibitem[\protect\citeauthoryear{Bernays}{1923}]{Bernays:23b}
1901: Paul Bernays.
1902: \newblock Erwiderung auf die {N}ote von {H}errn {A}loys {M}\"uller: {\"U}ber
1903: {Z}ahlen als {Z}eichen.
1904: \newblock {\em Mathe\-ma\-tische An\-nalen}, 90:159--63, 1923.
1905: \newblock {E}nglish translation in \Bcite{\pp{223--226}}{Mancosu:98}.
1906:
1907: \bibitem[\protect\citeauthoryear{Bernays}{1928a}]{Bernays:28b}
1908: Paul Bernays.
1909: \newblock {\"U}ber {N}elsons {S}tellungnahme in der {P}hilosophie der
1910: {M}athematik.
1911: \newblock {\em Die Naturwissenschaften}, 16:142--45, 1928.
1912:
1913: \bibitem[\protect\citeauthoryear{Bernays}{1928b}]{Bernays:28a}
1914: Paul Bernays.
1915: \newblock Zusatz zu {H}ilberts {V}ortrag \"uber ``{D}ie {G}rundlagen der
1916: {M}athematik''.
1917: \newblock {\em Abhandlungen aus dem Mathematischen Seminar der Universit{\"a}t
1918: Hamburg}, 6:88--92, 1928.
1919: \newblock {E}nglish translation in: \Bcite{\pp{485--489}}{Heijenoort:67}.
1920:
1921: \bibitem[\protect\citeauthoryear{Bernays}{1930}]{Bernays:30}
1922: Paul Bernays.
1923: \newblock Die {P}hilosophie der {M}athematik und die {H}ilbertsche
1924: {B}eweistheorie.
1925: \newblock {\em Bl\"atter f\"ur deutsche Philosophie}, 4:326--67, 1930.
1926: \newblock Reprinted in \Bcite{\pp{17--61}}{Bernays:76}. {E}nglish translation
1927: in \Bcite{\pp{234--265}}{Mancosu:98}.
1928:
1929: \bibitem[\protect\citeauthoryear{Bernays}{1970}]{Bernays:70}
1930: Paul Bernays.
1931: \newblock On the original {G}entzen consistency proof.
1932: \newblock In A.~Kino, J.~Myhill, and R.~E. Veseley, editors, {\em Intuitionism
1933: and Proof Theory}, pages 409--417. North-Holland, Amsterdam, 1970.
1934:
1935: \bibitem[\protect\citeauthoryear{Bernays}{1976}]{Bernays:76}
1936: Paul Bernays.
1937: \newblock {\em Abhandlungen zur Philosophie der Mathematik}.
1938: \newblock Wissenschaftliche Buchgesellschaft, Darmstadt, 1976.
1939:
1940: \bibitem[\protect\citeauthoryear{Buss}{1998}]{Buss:98}
1941: Samuel~R. Buss, editor.
1942: \newblock {\em Handbook of Proof Theory}.
1943: \newblock Elsevier, Amsterdam, 1998.
1944:
1945: \bibitem[\protect\citeauthoryear{Caldon and
1946: Ignjatovi\v{c}}{2005}]{Ignjatovic:03}
1947: Patrick Caldon and Aleksandar Ignjatovi\v{c}.
1948: \newblock On mathematical instrumentalism.
1949: \newblock {\em Journal of Symbolic Logic}, 70:778--794, 2005.
1950:
1951: \bibitem[\protect\citeauthoryear{Detlefsen}{1979}]{Detlefsen:79}
1952: Michael Detlefsen.
1953: \newblock On interpreting {G}\"odel's second theorem.
1954: \newblock {\em Journal of Philosophical Logic}, 8:297--313, 1979.
1955: \newblock Reprinted with a postscript in \Bcite{\pp{131--154}}{Shanker:88}.
1956:
1957: \bibitem[\protect\citeauthoryear{Detlefsen}{1986}]{Detlefsen:86}
1958: Michael Detlefsen.
1959: \newblock {\em Hilbert's Program}.
1960: \newblock Reidel, Dordrecht, 1986.
1961:
1962: \bibitem[\protect\citeauthoryear{Detlefsen}{1990}]{Detlefsen:90}
1963: Michael Detlefsen.
1964: \newblock On an alleged refutation of {H}ilbert's program using {G}\"odel's
1965: first incompleteness theorem.
1966: \newblock {\em Journal of Philosophial Logic}, 19:343--377, 1990.
1967:
1968: \bibitem[\protect\citeauthoryear{Detlefsen}{2001}]{Detlefsen:01}
1969: Michael Detlefsen.
1970: \newblock What does {G}\"odel's second theorem say?
1971: \newblock {\em Philosophia Mathematica}, 9:37--71, 2001.
1972:
1973: \bibitem[\protect\citeauthoryear{Detlefsen}{2005}]{Detlefsen:05}
1974: Michael Detlefsen.
1975: \newblock Formalism.
1976: \newblock In Stewart Shapiro, editor, {\em The Oxford Handbook of Philosophy of
1977: Mathematics and Logic}, pages 236--317. Oxford University Press, New York and
1978: Oxford, 2005.
1979:
1980: \bibitem[\protect\citeauthoryear{Ewald}{1996}]{Ewald:96}
1981: William~Bragg Ewald, editor.
1982: \newblock {\em From {K}ant to {H}ilbert. {A} Source Book in the Foundations of
1983: Mathematics}, volume~2.
1984: \newblock Oxford University Press, Oxford, 1996.
1985:
1986: \bibitem[\protect\citeauthoryear{Feferman}{1960}]{Feferman:60}
1987: Solomon Feferman.
1988: \newblock Arithmetization of metamathematics in a general setting.
1989: \newblock {\em Fundamenta Mathematicae}, pages 35--92, 1960.
1990:
1991: \bibitem[\protect\citeauthoryear{Feferman}{1988}]{Feferman:88a}
1992: Solomon Feferman.
1993: \newblock Hilbert's {P}rogram relativized: {P}roof-theoretical and foundational
1994: reductions.
1995: \newblock {\em Journal of Symbolic Logic}, 53(2):364--284, 1988.
1996:
1997: \bibitem[\protect\citeauthoryear{Feferman}{1993a}]{Feferman:93}
1998: Solomon Feferman.
1999: \newblock What rests on what? {T}he proof-theoretic analysis of mathematics.
2000: \newblock In Johannes Czermak, editor, {\em Philosophy of Mathematics.
2001: Proceedings of the Fifteenth International Wittgenstein-Symposium, Part~1},
2002: pages 147--171, Vienna, 1993. H\"older-Pichler-Tempsky.
2003:
2004: \bibitem[\protect\citeauthoryear{Feferman}{1993b}]{Feferman:93a}
2005: Solomon Feferman.
2006: \newblock Why a little bit goes a long way: {L}ogical foundations of
2007: scientifically applicable mathematics.
2008: \newblock {\em Proceedings of the Philosophy of Science Association 1992},
2009: 2:442--455, 1993.
2010: \newblock Reprinted in \Bcite{Ch.~14, \pp{284--298}}{Feferman:98}.
2011:
2012: \bibitem[\protect\citeauthoryear{Feferman}{1998}]{Feferman:98}
2013: Solomon Feferman.
2014: \newblock {\em In the Light of Logic}.
2015: \newblock Oxford University Press, New York and Oxford, 1998.
2016:
2017: \bibitem[\protect\citeauthoryear{Feferman}{2000}]{Feferman:00}
2018: Solomon Feferman.
2019: \newblock Does reductive proof theory have a viable rationale?
2020: \newblock {\em Erkenntnis}, 53:63--96, 2000.
2021:
2022: \bibitem[\protect\citeauthoryear{Field}{1980}]{Field:80}
2023: Hartry Field.
2024: \newblock {\em Science without Numbers. A Defence of Nominalism}.
2025: \newblock Princeton University Press, Princeton, 1980.
2026:
2027: \bibitem[\protect\citeauthoryear{Gentzen}{1933}]{Gentzen:33}
2028: Gerhard Gentzen.
2029: \newblock \"{U}ber das {V}erh\"{a}ltnis zwischen intuitionistischer und
2030: klassischer {L}ogik.
2031: \newblock First published in \emph{Archiv f\"ur mathematische Logik und
2032: Grundlagenforschung}~16 (1974), 119--132. {E}nglish translation in
2033: \Bcite{\pp{53--67}}{Gentzen:69}, 1933.
2034:
2035: \bibitem[\protect\citeauthoryear{Gentzen}{1934}]{Gentzen:34}
2036: Gerhard Gentzen.
2037: \newblock Untersuchungen \"uber das logische {S}chlie\ss en {I--II}.
2038: \newblock {\em Mathe\-mati\-sche Zeit\-schrift}, 39:176--210, 405--431, 1934.
2039: \newblock {E}nglish translation in \Bcite{\pp{68--131}}{Gentzen:69}.
2040:
2041: \bibitem[\protect\citeauthoryear{Gentzen}{1935}]{Gentzen:35}
2042: Gerhard Gentzen.
2043: \newblock Die {W}iderspruchsfreiheit der reinen {Z}ahlentheorie.
2044: \newblock Published as ``Der erste Widerspruchsfreiheitsbeweis f\"ur die
2045: klassische Zahlentheorie'' in \emph{Archiv f\"ur mathematische Logik und
2046: Grundlagenforschung}~16 (1974), 97--118. {E}nglish translation in
2047: \Bcite{\pp{132--213}}{Gentzen:69}, 1935.
2048:
2049: \bibitem[\protect\citeauthoryear{Gentzen}{1936}]{Gentzen:36}
2050: Gerhard Gentzen.
2051: \newblock Die {W}iderspruchsfreiheit der reinen {Z}ahlentheorie.
2052: \newblock {\em Mathe\-ma\-tische An\-nalen}, 112:493--565, 1936.
2053: \newblock {E}nglish translation in \Bcite{\pp{132--213}}{Gentzen:69}.
2054:
2055: \bibitem[\protect\citeauthoryear{Gentzen}{1943}]{Gentzen:43}
2056: Gerhard Gentzen.
2057: \newblock Beweisbarkeit und {U}nbeweisbarket von {A}nfangsf\"allen der
2058: transfiniten {I}nduktion in der reinen {Z}ahlentheorie.
2059: \newblock {\em Mathe\-ma\-tische An\-nalen}, 119:140--161, 1943.
2060: \newblock English translation in \Bcite{\pp{287--308}}{Gentzen:69}.
2061:
2062: \bibitem[\protect\citeauthoryear{Gentzen}{1969}]{Gentzen:69}
2063: Gerhard Gentzen.
2064: \newblock {\em The Collected Papers of {G}erhard {G}entzen}, M.~E. Szabo,
2065: editor.
2066: \newblock North-Holland, Amsterdam, 1969.
2067:
2068: \bibitem[\protect\citeauthoryear{Giaquinto}{1983}]{Giaquinto:83}
2069: Marcus Giaquinto.
2070: \newblock Hilbert's philosophy of mathematics.
2071: \newblock {\em British Journal for Philosophy of Science}, 34:119--132, 1983.
2072:
2073: \bibitem[\protect\citeauthoryear{G{\"o}del}{1931}]{Godel:31}
2074: Kurt G{\"o}del.
2075: \newblock \"{U}ber formal unentscheidbare {S}\"atze der \emph{Principia
2076: Mathematica} und verwandter {S}ysteme {I}.
2077: \newblock {\em Monatshefte f\"ur Mathematik und Physik}, 38:173--198, 1931.
2078: \newblock Reprinted and translated in \Bcite{\pp{144--195}}{Godel:86}.
2079:
2080: \bibitem[\protect\citeauthoryear{G{\"o}del}{1933}]{Godel:33b}
2081: Kurt G{\"o}del.
2082: \newblock Zur intuitionistischen {A}rithmetik und {Z}ahlentheorie.
2083: \newblock {\em Ergebnisse eines mathematisches Kolloquiums}, 4:34--38, 1933.
2084: \newblock Reprinted and translated in \Bcite{286--295}{Godel:86}.
2085:
2086: \bibitem[\protect\citeauthoryear{G{\"o}del}{1958}]{Godel:58}
2087: Kurt G{\"o}del.
2088: \newblock \"{U}ber eine bisher noch nicht ben\"utze {E}rweiterung des finiten
2089: {S}tandpunktes.
2090: \newblock {\em Dialectica}, pages 280--287, 1958.
2091: \newblock Reprinted and translated in \Bcite{\pp{217--251}}{Godel:90}.
2092:
2093: \bibitem[\protect\citeauthoryear{G{\"o}del}{1986}]{Godel:86}
2094: Kurt G{\"o}del.
2095: \newblock {\em {C}ollected Works}, volume~1, Solomon Feferman et~al., editors.
2096: \newblock Oxford University Press, Oxford, 1986.
2097:
2098: \bibitem[\protect\citeauthoryear{G{\"o}del}{1995}]{Godel:90}
2099: Kurt G{\"o}del.
2100: \newblock {\em {C}ollected Works}, volume~2, Solomon Feferman et~al., editors.
2101: \newblock Oxford University Press, Oxford, 1995.
2102:
2103: \bibitem[\protect\citeauthoryear{G{\"o}del}{2003a}]{Godel:03}
2104: Kurt G{\"o}del.
2105: \newblock {\em {C}ollected Works}, volume~4, Solomon Feferman et~al., editors.
2106: \newblock Oxford University Press, Oxford, 2003.
2107:
2108: \bibitem[\protect\citeauthoryear{G{\"o}del}{2003b}]{Godel:03a}
2109: Kurt G{\"o}del.
2110: \newblock {\em {C}ollected Works}, volume~5, Solomon Feferman et~al., editors.
2111: \newblock Oxford University Press, Oxford, 2003.
2112:
2113: \bibitem[\protect\citeauthoryear{Guaspari and Solovay}{1979}]{Guaspari:79}
2114: D.~Guaspari and R.~M. Solovay.
2115: \newblock Rosser sentences.
2116: \newblock {\em Annals of Mathematical Logic}, 16:81--99, 1979.
2117:
2118: \bibitem[\protect\citeauthoryear{Hallett}{1990}]{Hallett:90}
2119: Michael Hallett.
2120: \newblock Physicalism, reductionism and {H}ilbert.
2121: \newblock In Andrew~D. Irvine, editor, {\em Physicalism in Mathemtics}, pages
2122: 183--257. Reidel, Dordrecht, 1990.
2123:
2124: \bibitem[\protect\citeauthoryear{Hallett}{1994}]{Hallett:94}
2125: Michael Hallett.
2126: \newblock Hilbert's axiomatic method and the laws of thought.
2127: \newblock In Alexander George, editor, {\em Mathematics and Mind}, pages
2128: 158--200. Oxford University Press, Oxford, 1994.
2129:
2130: \bibitem[\protect\citeauthoryear{Herbrand}{1930}]{Herbrand:30}
2131: Jaques Herbrand.
2132: \newblock {\em Recherches sur la th{\'e}orie de la d{\'e}monstration}.
2133: \newblock Doctoral dissertation, University of Paris, 1930.
2134: \newblock {E}nglish translation in \Bcite{\pp{44--202}}{Goldfarb:71}.
2135:
2136: \bibitem[\protect\citeauthoryear{Herbrand}{1971}]{Goldfarb:71}
2137: Jaques Herbrand.
2138: \newblock {\em Logical Writings}, Warren~D. Goldfarb, editor.
2139: \newblock Harvard University Press, 1971.
2140:
2141: \bibitem[\protect\citeauthoryear{Hilbert and Ackermann}{1928}]{Hilbert:28b}
2142: David Hilbert and Wilhelm Ackermann.
2143: \newblock {\em Grundz{\"uge} der theoretischen {L}ogik}.
2144: \newblock Springer, Berlin, 1928.
2145:
2146: \bibitem[\protect\citeauthoryear{Hilbert and Bernays}{1923}]{Hilbert:22b}
2147: David Hilbert and Paul Bernays.
2148: \newblock Logische {G}rundlagen der {M}athematik.
2149: \newblock Vorlesung, Winter-Semester 1922--23. Lecture notes by Paul Bernays,
2150: with handwritten notes by Hilbert. Hilbert-Nachla\ss, Nieders\"achsische
2151: Staats- und Universit\"atsbibliothek, Cod. Ms. Hilbert 567. Published in
2152: \cite{Hilbert:06}, 1923.
2153:
2154: \bibitem[\protect\citeauthoryear{Hilbert and Bernays}{1934}]{HilbertBernays:34}
2155: David Hilbert and Paul Bernays.
2156: \newblock {\em Grundlagen der {M}athematik}, volume~1.
2157: \newblock Springer, Berlin, 1934.
2158:
2159: \bibitem[\protect\citeauthoryear{Hilbert and Bernays}{1939}]{HilbertBernays:39}
2160: David Hilbert and Paul Bernays.
2161: \newblock {\em Grundlagen der {M}athematik}, volume~2.
2162: \newblock Springer, Berlin, 1939.
2163:
2164: \bibitem[\protect\citeauthoryear{Hilbert}{1899}]{Hilbert:99}
2165: David Hilbert.
2166: \newblock Grundlagen der {G}eometrie.
2167: \newblock In {\em Festschrift zur {F}eier der {E}nth\"ullung des
2168: {G}auss-{W}eber-{D}enkmals in {G}\"ottingen}, pages 1--92. Teubner, Leipzig,
2169: 1st edition, 1899.
2170: \newblock reprinted in \cite{Hilbert:04}.
2171:
2172: \bibitem[\protect\citeauthoryear{Hilbert}{1900a}]{Hilbert:00a}
2173: David Hilbert.
2174: \newblock Mathematische {P}robleme.
2175: \newblock {\em Nachrichten von der K\"oniglichen Gesellschaft der
2176: Wissenschaften zu G\"ottingen, Math.-Phys. Klasse}, pages 253--297, 1900.
2177: \newblock Lecture given at the International Congress of Mathematicians, Paris,
2178: 1900. Partial {E}nglish translation in \Bcite{1096--1105}{Ewald:96}.
2179:
2180: \bibitem[\protect\citeauthoryear{Hilbert}{1900b}]{Hilbert:00}
2181: David Hilbert.
2182: \newblock {\"U}ber den {Z}ahlbegriff.
2183: \newblock {\em Jahres\-bericht der Deut\-schen Mathe\-matiker-Ver\-eini\-gung},
2184: 8:180--84, 1900.
2185: \newblock {E}nglish translation in \Bcite{1089--1096}{Ewald:96}.
2186:
2187: \bibitem[\protect\citeauthoryear{Hilbert}{1905}]{Hilbert:05}
2188: David Hilbert.
2189: \newblock {\"U}ber die {G}rundlagen der {L}ogik und der {A}rithmetik.
2190: \newblock In A.~Krazer, editor, {\em Verhandlungen des dritten
2191: {I}nternationalen {M}athematiker-{K}ongresses in {H}eidelberg vom 8. bis 13.
2192: {A}ugust 1904}, pages 174--85, Leipzig, 1905. Teubner.
2193: \newblock {E}nglish translation in \Bcite{\pp{129--38}}{Heijenoort:67}.
2194:
2195: \bibitem[\protect\citeauthoryear{Hilbert}{1918a}]{Hilbert:18}
2196: David Hilbert.
2197: \newblock Axiomatisches {D}enken.
2198: \newblock {\em Mathe\-ma\-tische An\-nalen}, 78:405--15, 1918.
2199: \newblock Lecture given at the Swiss Society of Mathematicians, 11 September
2200: 1917. Reprinted in \Bcite{\pp{146--56}}{Hilbert:35}. {E}nglish translation in
2201: \Bcite{\pp{1105--1115}}{Ewald:96}.
2202:
2203: \bibitem[\protect\citeauthoryear{Hilbert}{1918b}]{Hilbert:17}
2204: David Hilbert.
2205: \newblock Prinzipien der {M}athematik.
2206: \newblock Lecture notes by Paul Bernays. Winter-Semester 1917--18. Unpublished
2207: typescript. Bibliothek, Mathematisches Institut, Universit{\"a}t
2208: G{\"o}ttingen. Published in \cite{Hilbert:06}, 1918.
2209:
2210: \bibitem[\protect\citeauthoryear{Hilbert}{1920}]{Hilbert:20b}
2211: David Hilbert.
2212: \newblock Probleme der mathematischen {L}ogik.
2213: \newblock Vorlesung, Sommer-Semester 1920. Lecture notes by Paul Bernays and
2214: Moses Sch{\"o}nfinkel. Unpublished typescript. Bibliothek, Mathematisches
2215: Institut, Universit{\"a}t G{\"o}ttingen. Published in \cite{Hilbert:06},
2216: 1920.
2217:
2218: \bibitem[\protect\citeauthoryear{Hilbert}{1922a}]{Hilbert:21}
2219: David Hilbert.
2220: \newblock Grundlagen der {M}athematik.
2221: \newblock Vorlesung, Winter-Semester 1921--22. Lecture notes by Paul Bernays.
2222: Unpublished typescript. Bibliothek, Mathematisches Institut, Universit{\"a}t
2223: G{\"o}ttingen. Published in \cite{Hilbert:06}, 1922.
2224:
2225: \bibitem[\protect\citeauthoryear{Hilbert}{1922b}]{Hilbert:22a}
2226: David Hilbert.
2227: \newblock Neubegr{\"u}ndung der {M}athematik: {E}rste {M}itteilung.
2228: \newblock {\em Abhandlungen aus dem Seminar der Hamburgischen Universit{\"a}t},
2229: 1:157--77, 1922.
2230: \newblock Series of talks given at the University of Hamburg, July 25--27,
2231: 1921. Reprinted with notes by Bernays in \Bcite{\pp{157--177}}{Hilbert:35}.
2232: {E}nglish translation in \Bcite{\pp{198--214}}{Mancosu:98} and
2233: \Bcite{\pp{1115--1134}}{Ewald:96}.
2234:
2235: \bibitem[\protect\citeauthoryear{Hilbert}{1923}]{Hilbert:23}
2236: David Hilbert.
2237: \newblock Die logischen {G}rundlagen der {M}athematik.
2238: \newblock {\em Mathe\-ma\-tische An\-nalen}, 88:151--165, 1923.
2239: \newblock Lecture given at the Deutsche Naturforscher-Gesellschaft, September
2240: 1922. Reprinted in \Bcite{\pp{178--191}}{Hilbert:35}. {E}nglish translation
2241: in \Bcite{\pp{1134--1148}}{Ewald:96}.
2242:
2243: \bibitem[\protect\citeauthoryear{Hilbert}{1926}]{Hilbert:26}
2244: David Hilbert.
2245: \newblock {\"U}ber {d}as {U}nendliche.
2246: \newblock {\em Mathe\-ma\-tische An\-nalen}, 95:161--90, 1926.
2247: \newblock Lecture given M\"unster, 4 June 1925. {E}nglish translation in
2248: \Bcite{\pp{367--392}}{Heijenoort:67}.
2249:
2250: \bibitem[\protect\citeauthoryear{Hilbert}{1928}]{Hilbert:28}
2251: David Hilbert.
2252: \newblock Die {G}rundlagen der {M}athematik.
2253: \newblock {\em Abhandlungen aus dem Seminar der Hamburgischen Universit{\"a}t},
2254: 6:65--85, 1928.
2255: \newblock {E}nglish translation in \Bcite{\pp{464-479}}{Heijenoort:67}.
2256:
2257: \bibitem[\protect\citeauthoryear{Hilbert}{1929}]{Hilbert:29}
2258: David Hilbert.
2259: \newblock Probleme der {G}rundlegung der {M}athematik.
2260: \newblock {\em Mathe\-ma\-tische An\-nalen}, 102:1--9, 1929.
2261: \newblock Lecture given at the International Congress of Mathematicians, 3
2262: September 1928. {E}nglish translation in \Bcite{\pp{227--233}}{Mancosu:98}.
2263:
2264: \bibitem[\protect\citeauthoryear{Hilbert}{1931a}]{Hilbert:31b}
2265: David Hilbert.
2266: \newblock Beweis des {T}ertium non datur.
2267: \newblock {\em Nachrichten der Gesellschaft der Wissenschaften zu
2268: G{\"o}ttingen. Math.-phys. Klasse}, pages 120--25, 1931.
2269:
2270: \bibitem[\protect\citeauthoryear{Hilbert}{1931b}]{Hilbert:31a}
2271: David Hilbert.
2272: \newblock Die {G}rundlegung der elementaren {Z}ahlenlehre.
2273: \newblock {\em Mathe\-ma\-tische An\-nalen}, 104:485--94, 1931.
2274: \newblock Reprinted in \Bcite{\pp{192--195}}{Hilbert:35}. {E}nglish translation
2275: in \Bcite{\pp{1148--1157}}{Ewald:96}.
2276:
2277: \bibitem[\protect\citeauthoryear{Hilbert}{1935}]{Hilbert:35}
2278: David Hilbert.
2279: \newblock {\em Gesammelte {A}bhandlungen}, volume~3.
2280: \newblock Springer, Berlin, 1935.
2281:
2282: \bibitem[\protect\citeauthoryear{Hilbert}{1992}]{Hilbert:92}
2283: David Hilbert.
2284: \newblock {\em Natur und mathematisches {E}rkennen}.
2285: \newblock Birkh\"auser, Basel, 1992.
2286: \newblock Vorlesungen, 1919--20.
2287:
2288: \bibitem[\protect\citeauthoryear{Hilbert}{2004}]{Hilbert:04}
2289: David Hilbert.
2290: \newblock {\em David Hilbert's Lectures on the Foundations of Geometry,
2291: 1891--1902}, Ulrich Majer and Michael Hallett, editors.
2292: \newblock Springer, New York, 2004.
2293:
2294: \bibitem[\protect\citeauthoryear{Hilbert}{2006}]{Hilbert:06}
2295: David Hilbert.
2296: \newblock {\em David Hilbert's Lectures on the Foundations of Arithmetic and
2297: Logic, 1917--1933}, William Ewald and Wilfried Sieg, editors.
2298: \newblock Springer, New York, 2006.
2299: \newblock forthcoming.
2300:
2301: \bibitem[\protect\citeauthoryear{Hofweber}{2000}]{Hofweber:00}
2302: Thomas Hofweber.
2303: \newblock Proof-theoretic reduction as a philosopher's tool.
2304: \newblock {\em Erkenntnis}, 53:127--146, 2000.
2305:
2306: \bibitem[\protect\citeauthoryear{Ignjatovi\v{c}}{1994}]{Ignjatovic:94}
2307: Aleksandar Ignjatovi\v{c}.
2308: \newblock Hilbert's program and the omega-rule.
2309: \newblock {\em Journal of Symbolic Logic}, 59:322--343, 1994.
2310:
2311: \bibitem[\protect\citeauthoryear{Jeroslow}{1971}]{Jeroslow:71}
2312: Robert~G. Jeroslow.
2313: \newblock Consistency statements in formal theories.
2314: \newblock {\em Fundamenta Mathematicae}, 72:17--40, 1971.
2315:
2316: \bibitem[\protect\citeauthoryear{Jeroslow}{1975}]{Jeroslow:75}
2317: Robert~G. Jeroslow.
2318: \newblock Experimental logics and ${\Delta}^0_2$-theories.
2319: \newblock {\em Journal of Philosophical Logic}, 4:253--267, 1975.
2320:
2321: \bibitem[\protect\citeauthoryear{Kitcher}{1976}]{Kitcher:76}
2322: Philip Kitcher.
2323: \newblock Hilbert's epistemology.
2324: \newblock {\em Philosophy of Science}, 43:99--115, 1976.
2325:
2326: \bibitem[\protect\citeauthoryear{Kreisel}{1951}]{Kreisel:51}
2327: Georg Kreisel.
2328: \newblock On the interpretation of non-finitist proofs. {P}art~{I}.
2329: \newblock {\em Journal of Symbolic Logic}, 16:241--267, 1951.
2330:
2331: \bibitem[\protect\citeauthoryear{Kreisel}{1954}]{Kreisel:54}
2332: Georg Kreisel.
2333: \newblock A variant to {H}ilbert's theory of the foundations of arithmetic.
2334: \newblock {\em British Journal for the Philosophy of Science}, 4:107--129,
2335: 1954.
2336:
2337: \bibitem[\protect\citeauthoryear{Kreisel}{1960}]{Kreisel:58}
2338: Georg Kreisel.
2339: \newblock Ordinal logics and the characterization of informal notions of proof.
2340: \newblock In J.~A. Todd, editor, {\em Proceedings of the International Congress
2341: of Mathematicians. Edinburgh, 14--21 August 1958}, pages 289--299, Cambridge,
2342: 1960. Cambridge University Press.
2343:
2344: \bibitem[\protect\citeauthoryear{Kreisel}{1968}]{Kreisel:68}
2345: Georg Kreisel.
2346: \newblock A survey of proof theory.
2347: \newblock {\em Journal of Symbolic Logic}, 33:321--388, 1968.
2348:
2349: \bibitem[\protect\citeauthoryear{Kreisel}{1970}]{Kreisel:70}
2350: Georg Kreisel.
2351: \newblock Principles of proof and ordinals implicit in given concepts.
2352: \newblock In A.~Kino, J.~Myhill, and R.~E. Veseley, editors, {\em Intuitionism
2353: and Proof Theory}, pages 489--516. North-Holland, Amsterdam, 1970.
2354:
2355: \bibitem[\protect\citeauthoryear{Kreisel}{1971}]{Kreisel:71}
2356: Georg Kreisel.
2357: \newblock Review of \emph{The Collected Papers of {G}erhard {G}entzen}
2358: \cite{Gentzen:69}.
2359: \newblock {\em Journal of Philosophy}, 68:238--265, 1971.
2360:
2361: \bibitem[\protect\citeauthoryear{Kreisel}{1976}]{Kreisel:76}
2362: Georg Kreisel.
2363: \newblock Wie die {B}eweistheorie zu ihren {O}rdinalzahlen kam und kommt.
2364: \newblock {\em Jahresberichte der Deutschen Mathematiker-Vereinigung},
2365: 78:177--223, 1976.
2366:
2367: \bibitem[\protect\citeauthoryear{Kreisel}{1983}]{Kreisel:83}
2368: Georg Kreisel.
2369: \newblock Hilbert's programme.
2370: \newblock In Benacerraf and Putnam \shortcite{Benacerraf:83}, pages 207--238.
2371:
2372: \bibitem[\protect\citeauthoryear{Mancosu and Ryckman}{2002}]{Mancosu:02b}
2373: Paolo Mancosu and Thomas Ryckman.
2374: \newblock Mathematics and phenomenology: {T}he correspondence between {O}.
2375: {B}ecker and {H}. {W}eyl.
2376: \newblock {\em Philosophia Mathematica}, 10:130--202, 2002.
2377:
2378: \bibitem[\protect\citeauthoryear{Mancosu}{1998a}]{Mancosu:98}
2379: Paolo Mancosu, editor.
2380: \newblock {\em From {B}rouwer to {H}ilbert. {T}he Debate on the Foundations of
2381: Mathematics in the 1920s}.
2382: \newblock Oxford University Press, Oxford, 1998.
2383:
2384: \bibitem[\protect\citeauthoryear{Mancosu}{1998b}]{Mancosu:98c}
2385: Paolo Mancosu.
2386: \newblock Hilbert and {B}ernays on metamathematics.
2387: \newblock In {\em From Brouwer to Hilbert\/} \shortcite{Mancosu:98}, pages
2388: 149--188.
2389:
2390: \bibitem[\protect\citeauthoryear{Mancosu}{1999}]{Mancosu:99}
2391: Paolo Mancosu.
2392: \newblock Between {R}ussell and {H}ilbert: {B}ehmann on the foundations of
2393: mathematics.
2394: \newblock {\em Bulletin of Symbolic Logic}, 5(3):303--330, 1999.
2395:
2396: \bibitem[\protect\citeauthoryear{Mancosu}{2003}]{Mancosu:03}
2397: Paolo Mancosu.
2398: \newblock The {R}ussellian influence on {H}ilbert and his school.
2399: \newblock {\em Synth{\`e}se}, 137(1--2):59--101, 2003.
2400:
2401: \bibitem[\protect\citeauthoryear{Mancosu}{2004}]{Mancosu:04a}
2402: Paolo Mancosu.
2403: \newblock Review of {K}urt {G}\"odel, \emph{Collected {W}orks}, vols. {IV} and
2404: {V}, {S}olomon {F}eferman, et al., eds. {O}xford: {O}xford {U}niversity
2405: {P}ress, 2003.
2406: \newblock {\em Notre Dame Journal of Formal Logic}, 45:109--125, 2004.
2407:
2408: \bibitem[\protect\citeauthoryear{Mints and Tupailo}{1999}]{Mints:99}
2409: Grigori Mints and Sergei Tupailo.
2410: \newblock Epsilon-substitution method for the ramified language and
2411: ${\Delta_1^1}$-comprehension rule.
2412: \newblock In Andrea Cantini et~al., editors, {\em Logic and Foundations of
2413: Mathematics}, pages 107--130. Kluwer, Dordrecht, 1999.
2414:
2415: \bibitem[\protect\citeauthoryear{Moore}{1997}]{Moore:97}
2416: Gregory~H. Moore.
2417: \newblock Hilbert and the emergence of modern mathematical logic.
2418: \newblock {\em Theoria (Segunda \'Epoca)}, 12:65--90, 1997.
2419:
2420: \bibitem[\protect\citeauthoryear{M{\"u}ller}{1923}]{Muller:23}
2421: Aloys M{\"u}ller.
2422: \newblock {\"U}ber {Z}ahlen als {Z}eichen.
2423: \newblock {\em Mathematische Annalen}, 90:153--158; 163, 1923.
2424:
2425: \bibitem[\protect\citeauthoryear{Negri}{1980}]{Negri:80}
2426: Maurizio Negri.
2427: \newblock Constructive sequent reduction in {G}entzen's first consistency proof
2428: for arithmetic.
2429: \newblock In Maria~Luisa Dalla~Chiara, editor, {\em Italian Studies in the
2430: Philosophy of Science}, pages 153--168. Reidel, Dordrecht, 1980.
2431:
2432: \bibitem[\protect\citeauthoryear{Paris and Harrington}{1977}]{Paris:77}
2433: Jeff Paris and Leo Harrington.
2434: \newblock A mathematical incompleteness in {P}eano arithmetic.
2435: \newblock In Barwise \shortcite{Barwise:77}, pages 1133--1142.
2436:
2437: \bibitem[\protect\citeauthoryear{Parsons}{1998}]{Parsons:98}
2438: Charles Parsons.
2439: \newblock Finitism and intuitive knowledge.
2440: \newblock In Matthias Schirn, editor, {\em The Philosophy of Mathematics
2441: Today}, pages 249--270. Oxford University Press, Oxford, 1998.
2442:
2443: \bibitem[\protect\citeauthoryear{Peckhaus}{1990}]{Peckhaus:90}
2444: Volker Peckhaus.
2445: \newblock {\em Hilbertprogramm und {K}ritische {P}hilosophie}.
2446: \newblock Vandenhoeck und Ruprecht, G\"ottingen, 1990.
2447:
2448: \bibitem[\protect\citeauthoryear{Pohlers}{1987}]{Pohlers:87}
2449: Wolfram Pohlers.
2450: \newblock Contributions of the {S}ch\"utte school school in {M}unich to proof
2451: theory, 1987.
2452: \newblock Appendix to \cite{Takeuti:87}.
2453:
2454: \bibitem[\protect\citeauthoryear{Pohlers}{1998}]{Pohlers:98}
2455: Wolfram Pohlers.
2456: \newblock Subsystems of set theory and second-order number theory.
2457: \newblock In Buss \shortcite{Buss:98}.
2458:
2459: \bibitem[\protect\citeauthoryear{Poincar\'{e}}{1906}]{Poincare:06a}
2460: Henri Poincar\'{e}.
2461: \newblock Les math{\'e}matiques et la logique.
2462: \newblock {\em Revue de m{\'e}taphysique et de morale}, 14:294--317, 1906.
2463: \newblock {E}nglish translation in \Bcite{1038--1052}{Ewald:96}.
2464:
2465: \bibitem[\protect\citeauthoryear{Pudl\'ak}{1998}]{Pudlak:98}
2466: Pavel Pudl\'ak.
2467: \newblock The length of proofs.
2468: \newblock In Buss \shortcite{Buss:98}.
2469:
2470: \bibitem[\protect\citeauthoryear{Raatikainen}{2003}]{Raatikainen:03}
2471: Panu Raatikainen.
2472: \newblock Hilbert's program revisited.
2473: \newblock {\em Synth{\`e}se}, 137:157--177, 2003.
2474:
2475: \bibitem[\protect\citeauthoryear{Ramsey}{1926}]{Ramsey:26}
2476: Frank~P. Ramsey.
2477: \newblock Mathematical logic.
2478: \newblock {\em The Mathematical Gazette}, 13:185--94, 1926.
2479: \newblock Reprinted in \Bcite{225--244}{Ramsey:90}.
2480:
2481: \bibitem[\protect\citeauthoryear{Ramsey}{1990}]{Ramsey:90}
2482: Frank~P. Ramsey.
2483: \newblock {\em Philosophical Papers}, D.~H. Mellor, editor.
2484: \newblock Cambridge University Press, Cambridge, 1990.
2485:
2486: \bibitem[\protect\citeauthoryear{Rathjen}{2005a}]{Rathjen:05b}
2487: Michael Rathjen.
2488: \newblock An ordinal analysis of parameter free ${\Pi}^1_2$-comprehension.
2489: \newblock {\em Archive for Mathematical Logic}, 44:263--362, 2005.
2490:
2491: \bibitem[\protect\citeauthoryear{Rathjen}{2005b}]{Rathjen:05a}
2492: Michael Rathjen.
2493: \newblock An ordinal analysis of stability.
2494: \newblock {\em Archive for Mathematical Logic}, 44:1--62, 2005.
2495:
2496: \bibitem[\protect\citeauthoryear{Resnik}{1974a}]{Resnik:74}
2497: Michael~D. Resnik.
2498: \newblock The {F}rege-{H}ilbert controversy.
2499: \newblock {\em Philosophy and Phenomenological Research}, 34:386--403, 1974.
2500:
2501: \bibitem[\protect\citeauthoryear{Resnik}{1974b}]{Resnik:74a}
2502: Michael~D. Resnik.
2503: \newblock On the philosophical significance of consistency proofs.
2504: \newblock {\em Journal of Philosophical Logic}, 3:133--47, 1974.
2505:
2506: \bibitem[\protect\citeauthoryear{Resnik}{1980}]{Resnik:80}
2507: Michael Resnik.
2508: \newblock {\em Frege and the Philosophy of Mathematics}.
2509: \newblock Cornell University Press, Ithaca, 1980.
2510:
2511: \bibitem[\protect\citeauthoryear{Russell}{1902}]{Russell:02a}
2512: Bertrand Russell.
2513: \newblock Letter to {F}rege, {J}une 16, 1902.
2514: \newblock In van Heijenoort \shortcite{Heijenoort:67}, pages 124--125.
2515:
2516: \bibitem[\protect\citeauthoryear{Sch{\"u}tte}{1960}]{Schutte:60}
2517: Kurt Sch{\"u}tte.
2518: \newblock {\em Beweistheorie}.
2519: \newblock Springer, Berlin, 1960.
2520:
2521: \bibitem[\protect\citeauthoryear{Shanker}{1988}]{Shanker:88}
2522: Stuart~G. Shanker.
2523: \newblock {\em G\"odel's Theorem in Focus}.
2524: \newblock Routledge, London, 1988.
2525:
2526: \bibitem[\protect\citeauthoryear{Sieg}{1990}]{Sieg:90}
2527: Wilfried Sieg.
2528: \newblock Reflections on {H}ilbert's program.
2529: \newblock In Wilfried Sieg, editor, {\em Acting and Reflecting}, pages 171--82.
2530: Kluwer, Dordrecht, 1990.
2531:
2532: \bibitem[\protect\citeauthoryear{Sieg}{1999}]{Sieg:99}
2533: Wilfried Sieg.
2534: \newblock Hilbert's programs: 1917--1922.
2535: \newblock {\em Bulletin of Symbolic Logic}, 5(1):1--44, 1999.
2536:
2537: \bibitem[\protect\citeauthoryear{Sieg}{2002}]{Sieg:02}
2538: Wilfried Sieg.
2539: \newblock Beyond {H}ilbert's reach?
2540: \newblock In David~B. Malament, editor, {\em Reading Natural Philosophy. Essays
2541: in the History and Philosophy of Science and Mathematics}, pages 363--405.
2542: Open Court, Chicago and La Salle, Ill., 2002.
2543:
2544: \bibitem[\protect\citeauthoryear{Simpson}{1988}]{Simpson:88}
2545: Stephen~G. Simpson.
2546: \newblock Partial realizations of {H}ilbert's program.
2547: \newblock {\em Journal of Symbolic Logic}, 53(2):349--363, 1988.
2548:
2549: \bibitem[\protect\citeauthoryear{Simpson}{1999}]{Simpson:99}
2550: Stephen~G. Simpson.
2551: \newblock {\em Subsystems of Seond Order Arithmetic}.
2552: \newblock Springer, Berlin, 1999.
2553:
2554: \bibitem[\protect\citeauthoryear{Simpson}{2005}]{Simpson:05}
2555: Stephen~G. Simpson.
2556: \newblock {\em Reverse Mathematics 2001}.
2557: \newblock Lecture Notes in Logic~21. Association for Symbolic Logic and A K
2558: Peters, Wellesley, Mass., 2005.
2559:
2560: \bibitem[\protect\citeauthoryear{Smory{\'n}ski}{1977}]{Smorynski:77}
2561: Craig Smory{\'n}ski.
2562: \newblock The incompleteness theorems.
2563: \newblock In Barwise \shortcite{Barwise:77}, pages 821--865.
2564:
2565: \bibitem[\protect\citeauthoryear{Stein}{1988}]{Stein:88}
2566: Howard Stein.
2567: \newblock \emph{Logos}, logic, and \emph{logisitik\'e}: Some philosophical
2568: remarks on nineteenth-century transformation of mathematics.
2569: \newblock In William Aspray and Philip Kitcher, editors, {\em History and
2570: Philosophy of Modern Mathematics}, volume~11 of {\em Minesota Studies in the
2571: Philosophy of Science}, pages 238--259. University of Minnesota Press, 1988.
2572:
2573: \bibitem[\protect\citeauthoryear{Steiner}{1975}]{Steiner:75}
2574: Mark Steiner.
2575: \newblock {\em Mathematical Knowledge}.
2576: \newblock Cornell University Press, Ithaca, 1975.
2577:
2578: \bibitem[\protect\citeauthoryear{Steiner}{1991}]{Steiner:91}
2579: Mark Steiner.
2580: \newblock Review of \emph{Hilbert's Program: An Essay on Mathematical
2581: Instrumentalism} \cite{Detlefsen:86}.
2582: \newblock {\em Journal of Philosophy}, 88(6):331--336, 1991.
2583:
2584: \bibitem[\protect\citeauthoryear{Tait}{1981}]{Tait:81}
2585: W.~W. Tait.
2586: \newblock Finitism.
2587: \newblock {\em Journal of Philosophy}, 78:524--546, 1981.
2588: \newblock Reprinted in \Bcite{\pp{21--42}}{Tait:05}.
2589:
2590: \bibitem[\protect\citeauthoryear{Tait}{2002}]{Tait:02}
2591: W.~W. Tait.
2592: \newblock Remarks on finitism.
2593: \newblock In Wilfried Sieg, Richard Sommer, and Carolyn Talcott, editors, {\em
2594: Reflections on the Foundations of Mathematics. Essays in Honor of {S}olomon
2595: {F}eferman}, Lecture Notes in Logic~15. Association for Symbolic Logic and A
2596: K Peters, 2002.
2597: \newblock Reprinted in \Bcite{\pp{43--53}}{Tait:05}.
2598:
2599: \bibitem[\protect\citeauthoryear{Tait}{2005a}]{Tait:05a}
2600: W.~W. Tait.
2601: \newblock G\"odel's reformulation of {G}entzen's first consistency proof for
2602: arithmetic: the no-counterexample interpretation.
2603: \newblock {\em Bulletin of Symbolic Logic}, 11:225--238, 2005.
2604:
2605: \bibitem[\protect\citeauthoryear{Tait}{2005b}]{Tait:05}
2606: William Tait.
2607: \newblock {\em The Provenance of Pure Reason. Essays in the Philosophy of
2608: Mathematics and Its History}.
2609: \newblock Oxford University Press, New York, 2005.
2610:
2611: \bibitem[\protect\citeauthoryear{Takeuti}{1987}]{Takeuti:87}
2612: Gaisi Takeuti.
2613: \newblock {\em Proof Theory}.
2614: \newblock Studies in Logic~81. North-Holland, Amsterdam, 2nd edition, 1987.
2615:
2616: \bibitem[\protect\citeauthoryear{van Heijenoort}{1967}]{Heijenoort:67}
2617: Jean van Heijenoort, editor.
2618: \newblock {\em From {F}rege to {G}{\"o}del. {A} Source Book in Mathematical
2619: Logic, 1897--1931}.
2620: \newblock Harvard University Press, Cambridge, Mass., 1967.
2621:
2622: \bibitem[\protect\citeauthoryear{Visser}{1989}]{Visser:89}
2623: Albert Visser.
2624: \newblock Peano's smart children: {A} provability logical study of systems with
2625: built-in consistency.
2626: \newblock {\em Notre Dame Journal of Formal Logic}, 30:161--196, 1989.
2627:
2628: \bibitem[\protect\citeauthoryear{von Neumann}{1927}]{Neumann:27}
2629: Johann von Neumann.
2630: \newblock Zur {H}ilbertschen {B}eweistheorie.
2631: \newblock {\em Mathe\-mati\-sche Zeit\-schrift}, 26:1--46, 1927.
2632:
2633: \bibitem[\protect\citeauthoryear{von Neumann}{1931}]{Neumann:31}
2634: Johann von Neumann.
2635: \newblock Die formalistische {G}rundlegung der {M}athematik.
2636: \newblock {\em Erkenntnis}, 2:116--34, 1931.
2637: \newblock {E}nglish translation in: \Bcite{\pp{61--65}}{Benacerraf:83}.
2638:
2639: \bibitem[\protect\citeauthoryear{Webb}{1997}]{Webb:97}
2640: Judson~C. Webb.
2641: \newblock Hilbert's formalism and arithmetization of mathematics.
2642: \newblock {\em Synth\`ese}, 110:1--14, 1997.
2643:
2644: \bibitem[\protect\citeauthoryear{Weyl}{1921}]{Weyl:21}
2645: Hermann Weyl.
2646: \newblock \"{U}ber die neue {G}rundlagenkrise der {M}athematik.
2647: \newblock {\em Mathematische Zeitschrift}, 10:37--79, 1921.
2648: \newblock Reprinted in \Bcite{143-180}{Weyl:68a}. {E}nglish translation in
2649: \Bcite{\pp{86--118}}{Mancosu:98}.
2650:
2651: \bibitem[\protect\citeauthoryear{Weyl}{1925}]{Weyl:25}
2652: Hermann Weyl.
2653: \newblock Die heutige {E}rkenntnislage in der {M}athematik.
2654: \newblock {\em Symposion}, 1:1--23, 1925.
2655: \newblock Reprinted in: \Bcite{\pp{511--42}}{Weyl:68a}. {E}nglish translation
2656: in: \Bcite{\pp{123--42}}{Mancosu:98}.
2657:
2658: \bibitem[\protect\citeauthoryear{Weyl}{1928}]{Weyl:28}
2659: Hermann Weyl.
2660: \newblock Diskussionsbemerkungen zu dem zweiten {H}ilbertschen {V}ortrag \"uber
2661: die {G}rundlagen der {M}athematik.
2662: \newblock {\em Abhandlungen aus dem Mathematischen Seminar der Universit{\"a}t
2663: Hamburg}, 6:86--88, 1928.
2664: \newblock {E}nglish translation in \Bcite{\pp{480-484}}{Heijenoort:67}.
2665:
2666: \bibitem[\protect\citeauthoryear{Weyl}{1968}]{Weyl:68a}
2667: Hermann Weyl.
2668: \newblock {\em Gesammelte {A}bhandlungen}, volume~1, K.~Chandrasekharan,
2669: editor.
2670: \newblock Springer Verlag, Berlin, 1968.
2671:
2672: \bibitem[\protect\citeauthoryear{Whitehead and Russell}{1910}]{Russell:10}
2673: Alfred~North Whitehead and Bertrand Russell.
2674: \newblock {\em Principia Mathematica}, volume~1.
2675: \newblock Cambridge University Press, Cambridge, 1910.
2676:
2677: \bibitem[\protect\citeauthoryear{Whitehead and Russell}{1912}]{Russell:12}
2678: Alfred~North Whitehead and Bertrand Russell.
2679: \newblock {\em Principia Mathematica}, volume~2.
2680: \newblock Cambridge University Press, Cambridge, 1912.
2681:
2682: \bibitem[\protect\citeauthoryear{Whitehead and Russell}{1913}]{Russell:13}
2683: Alfred~North Whitehead and Bertrand Russell.
2684: \newblock {\em Principia Mathematica}, volume~3.
2685: \newblock Cambridge University Press, Cambridge, 1913.
2686:
2687: \bibitem[\protect\citeauthoryear{Zach}{1999}]{Zach:99}
2688: Richard Zach.
2689: \newblock Completeness before {P}ost: {B}ernays, {H}ilbert, and the development
2690: of propositional logic.
2691: \newblock {\em Bulletin of Symbolic Logic}, 5(3):331--366, 1999.
2692:
2693: \bibitem[\protect\citeauthoryear{Zach}{2003a}]{Zach:03a}
2694: Richard Zach.
2695: \newblock Hilbert's program.
2696: \newblock In Edward~N. Zalta, editor, {\em The Stanford Encyclopedia of
2697: Philosophy}. Fall 2003.
2698: \newblock http://plato.stanford.edu/archives/entries/hilbert-program/.
2699:
2700: \bibitem[\protect\citeauthoryear{Zach}{2003b}]{Zach:03}
2701: Richard Zach.
2702: \newblock The practice of finitism. {E}psilon calculus and consistency proofs
2703: in {H}ilbert's {P}rogram.
2704: \newblock {\em Synth{\`e}se}, 137:211--259, 2003.
2705:
2706: \bibitem[\protect\citeauthoryear{Zach}{2004}]{Zach:02}
2707: Richard Zach.
2708: \newblock Hilbert's ``{V}erungl\"uckter {B}eweis,'' the first epsilon theorem
2709: and consistency proofs.
2710: \newblock {\em History and Philosophy of Logic}, 25:79--94, 2004.
2711:
2712: \end{thebibliography}
2713:
2714:
2715:
2716: \end{document}
2717: