Movatterモバイル変換

[0]ホーム
URL:

SEP home page
Stanford Encyclopedia of Philosophy

Hilbert’s Program

First published Thu Jul 31, 2003; substantive revision Fri Sep 29, 2023

In the early 1920s, the German mathematician David Hilbert(1862–1943) put forward a new proposal for the foundation ofclassical mathematics which has come to be known as Hilbert’sProgram. It calls for a formalization of all of mathematics inaxiomatic form, together with a proof that this axiomatization ofmathematics is consistent. The consistency proof itself was to becarried out using only what Hilbert called “finitary”methods. The special epistemological character of finitary reasoningthen yields the required justification of classical mathematics.Although Hilbert proposed his program in this form only in 1921,various facets of it are rooted in foundational work of his going backuntil around 1900, when he first pointed out the necessity of giving adirect consistency proof of analysis. Work on the program progressedsignificantly in the 1920s with contributions from logicians such asPaul Bernays, Wilhelm Ackermann, John von Neumann, and JacquesHerbrand. It was also a great influence onKurt Gödel, whose work on the incompleteness theorems were motivated byHilbert’s Program. Gödel’s work is generally taken toshow that Hilbert’s Program cannot be carried out. It hasnevertheless continued to be an influential position in the philosophyof mathematics, and, starting with the work of Gerhard Gentzen in the1930s, work on so-called Relativized Hilbert Programs have beencentral to thedevelopment of proof theory.

1. Historical development of Hilbert’s Program

1.1 Early work on foundations

Hilbert’s work on the foundations of mathematics has its rootsin his work on geometry of the 1890s, culminating in his influentialtextbookFoundations of Geometry (1899) (see19th Century Geometry). Hilbertbelieved that the proper way to develop any scientific subjectrigorously required an axiomatic approach. In providing an axiomatictreatment, the theory would be developed independently of any need forintuition, and it would facilitate an analysis of the logicalrelationships between the basic concepts and the axioms. For Hilbert,the investigation of the independence and, above all, consistency ofthe axioms is of basic importance for an axiomatic treatment. For theaxioms of geometry, consistency can be proved by providing aninterpretation of the system in the real plane, and thus, theconsistency of geometry is reduced to the consistency of analysis. Thefoundation of analysis, of course, itself requires an axiomatizationand a consistency proof. Hilbert provided such an axiomatization in(1900b), but it became clear very quicklythat the consistency of analysis faced significant difficulties, inparticular because the favored way of providing a foundation foranalysis in Dedekind’s work relied on dubious assumptions akinto to those that lead to the paradoxes of set theory andRussell’s Paradox in Frege’s foundation of arithmetic.

Hilbert thus realized that adirect consistency proof ofanalysis, i.e., one not based on reduction to another theory, wasneeded. He proposed the problem of finding such a proof as the secondof his 23 mathematical problems in his address to the InternationalCongress of Mathematicians in 1900 (1900a) and presented a sketch of such a proof in his Heidelberg talk (1905). Several factors delayed the further development of Hilbert’sfoundational program. One was perhaps the criticism ofPoincaré (1906) against what he saw as a viciously circular use of induction inHilbert’s sketched consistency proof (seeSteiner 1975, Appendix). Hilbert also realized that axiomatic investigationsrequired a well worked-out logical formalism. At the time he relied ona conception of logic based on the algebraic tradition, in particular,on Schröder’s work, which was not particularly suited as aformalism for the axiomatization of mathematics. (SeePeckhaus 1990 on the early development of Hilbert’s Program.)

1.2 The influence ofPrincipia Mathematica

The publication of Russell and Whitehead’sPrincipia Mathematica provided the required logical basis for a renewed attack onfoundational issues. Beginning in 1914, Hilbert’s studentHeinrich Behmann and others studied the system ofPrincipia(seeMancosu 1999 on Behmann’s role in Hilbert’s school). Hilbert himselfreturned to work on foundational issues in 1917. In September 1917, hedelivered an address to the Swiss Mathematical Society entitled“Axiomatic Thought” (1918a). It is his first published contribution to mathematical foundationssince 1905. In it, he again emphasizes the requirement of consistencyproofs for axiomatic systems: “The chief requirement of thetheory of axioms must go farther [than merely avoiding knownparadoxes], namely, to show that within every field of knowledgecontradictions based on the underlying axiom-system areabsolutelyimpossible.” He poses the proof of the consistency ofarithmetic (and of set theory) again as the main open problems. Inboth these cases, there seems to be nothing more fundamental availableto which the consistency could be reduced other than logic itself. AndHilbert then thought that the problem had essentially been solved byRussell’s work inPrincipia. Nevertheless, otherfundamental problems of axiomatics remained unsolved, including theproblem of the “decidability of every mathematicalquestion,” which also traces back to Hilbert’s 1900address.

These unresolved problems of axiomatics led Hilbert to devotesignificant effort to work on logic in the following years. In 1917,Paul Bernays joined him as his assistant in Göttingen. In aseries of courses from 1917–1921, Hilbert, with the assistanceof Bernays and Behmann, made significant new contributions to formallogic. The course from 1917 (Hilbert, 1918b), in particular, contains a sophisticated development of first-orderlogic, and forms the basis of Hilbert and Ackermann’s textbookPrinciples of Theoretical Logic (1928) (seeEwald and Sieg 2013,Sieg 1999, and Zach1999,2003).

1.3 Finitism and the quest for consistency proofs

Within the next few years, however, Hilbert came to rejectRussell’s logicist solution to the consistency problem forarithmetic. At the same time,Brouwer’s intuitionistic mathematics gained currency. In particular,Hilbert’s former student Hermann Weyl converted to intuitionism.Weyl’s paper “The new foundational crisis inmathematics” (1921) was answered by Hilbert in three talks in Hamburg in the Summer of1921 (1922b). Here, Hilbert presented his own proposal for a solution to theproblem of the foundation of mathematics. This proposal incorporatedHilbert’s ideas from 1904 regarding direct consistency proofs,his conception of axiomatic systems, and also the technicaldevelopments in the axiomatization of mathematics in the work ofRussell as well as the further developments carried out by him and hiscollaborators. What was new was the way in which Hilbert wanted toimbue his consistency project with the philosophical significancenecessary to answer Brouwer and Weyl’s criticisms: the finitarypoint of view.

According to Hilbert, there is a privileged part of mathematics,contentual elementary number theory, which relies only on a“purely intuitive basis of concrete signs.” Whereas theoperating with abstract concepts was considered “inadequate anduncertain,” there is a realm of

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

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

The intuitive-contentual operations with signs forms the basis ofHilbert’s metamathematics. Just as contentual number theoryoperates with sequences of strokes, so metamathematics operates withsequences of symbols (formulas, proofs). Formulas and proofs can besyntactically manipulated, and the properties and relationships offormulas and proofs are similarly based in a logic-free intuitivecapacity which guarantees certainty of knowledge about formulas andproofs arrived at by such syntactic operations. Mathematics itself,however, operates with abstract concepts, e.g., quantifiers, sets,functions, and uses logical inference based on principles such asmathematical induction or the principle of the excluded middle. These“concept-formations” and modes of reasoning had beencriticized by Brouwer and others on grounds that they presupposeinfinite totalities as given, or that they involve impredicativedefinitions (which were considered by the critics as viciouslycircular). Hilbert’s aim was to justify their use. To this end,he pointed out that they can be formalized in axiomatic systems (suchas that ofPrincipia or those developed by Hilbert himself),and mathematical propositions and proofs thus turn into formulas andderivations from axioms according to strictly circumscribed rules ofderivation. Mathematics, so Hilbert, “becomes an inventory ofprovable formulas.” In this way the proofs of mathematics aresubject to metamathematical, contentual investigation. The goal ofHilbert’s program is then to give a contentual, metamathematicalproof that there can be no derivation of a contradiction, i.e., noformal derivations of a formula \(A\) and of its negation \(\negA\).

This sketch of the aims of the program was fleshed out by Hilbert andhis collaborators in the following 10 years. On the conceptual side,the finite standpoint and the strategy for a consistency proof wereelaborated byHilbert (1928);Hilbert (1923);Hilbert (1926) andBernays (1928b);Bernays (1922);Bernays (1930), of which Hilbert’s article “On the infinite” (1926) provides the most detailed elaboration of the finitary standpoint. Inaddition to Hilbert and Bernays, a number of other people wereinvolved in technical work on the program. In lectures given inGöttingen (Hilbert and Bernays, 1923;Hilbert, 1922a), Hilbert and Bernays developed the\(\varepsilon\)-calculus as their definitive formalism for axiom systems for arithmetic andanalysis. Hilbert there also presented his approach to givingconsistency proofs using his so-called \(\varepsilon\)-substitutionmethod.Ackermann (1924) attempted to extend Hilbert’s idea to a system of analysis. Theproof was, however, erroneous (seeZach 2003). John von Neumann, then visiting Göttingen, gave a correctedconsistency proof for a system of the \(\varepsilon\)-formalism(which, however, did not include the induction axiom) in 1925(published in1927). Building on von Neumann’s work, Ackermann devised a new\(\varepsilon\)-substitution procedure which he communicated toBernays (seeBernays 1928b). In his address “Problems of the grounding of mathematics”to the International Congress of Mathematicians in Bologna in 1928 (1929), Hilbert optimistically claimed that the work of Ackermann and vonNeumann had established the consistency of number theory and that theproof for analysis had already been carried out by Ackermann “tothe extent that the only remaining task consists in the proof of anelementary finiteness theorem that is purely arithmetical.”

1.4 The impact of Gödel’s Incompleteness Theorems

Gödel’s incompleteness theorems showed that Hilbert’s optimism was undue. In September 1930,Kurt Gödel announced his first incompleteness theorem at aconference in Königsberg. Von Neumann, who was in the audience,immediately recognized the significance of Gödel’s resultfor Hilbert’s program. Shortly after the conference he wrote toGödel, telling him that he had found a corollary toGödel’s result. Gödel had found the same resultalready independently: the second incompleteness theorem, assertingthat the system ofPrincipia does not prove the formalizationof the claim that the system ofPrincipia is consistent(provided it is). All the methods of finitary reasoning used in theconsistency proofs up till then were believed to be formalizable inPrincipia, however. Hence, if the consistency ofPrincipia were provable by the methods used inAckermann’s proofs, it should be possible to formalize thisproof inPrincipia; but this is what the secondincompleteness theorem states is impossible. Bernays also realized theimportance of Gödel’s results immediately after he studiedGödel’s paper in January 1931, writing to Gödel that(under the assumption that finitary reasoning can be formalized inPrincipia) the incompleteness theorem shows that a finitaryconsistency proof ofPrincipia is impossible. Shortlythereafter, von Neumann showed that Ackermann’s consistencyproof is flawed and provided a counterexample to the proposed\(\varepsilon\)-substitution procedure (seeZach 2003).

In (1936), Gentzen published a consistency proof of first-order Peano Arithmetic(\(\PA\)). As Gödel had shown was necessary, Gentzen’sproof used methods that could not be formalized in \(\PA\) itself,namely, transfinite induction along the ordinal \(\varepsilon_0\).Gentzen’s work marks the beginning of post-Gödelian prooftheory and work on Relativized Hilbert Programs. Proof theory in thetradition of Gentzen has analyzed axiomatic systems according to whatextensions of the finitary standpoint are necessary to prove theirconsistency. Usually, the consistency strength of systems has beenmeasured by the system’sproof-theoretic ordinal, i.e.,the ordinal transfinite induction along which suffices to proveconsistency. In the case of \(\PA\), that ordinal is\(\varepsilon_0\). (For further discussion, see the entries onproof theory andthe development of proof theory.)

2. The Finitary Point of View

The cornerstone of Hilbert’s philosophy of mathematics, and thesubstantially new aspect of his foundational thought from1922b onward, consisted in what he called the finitary standpoint. Thismethodological standpoint consists in a restriction of mathematicalthought to those objects which are “intuitively present asimmediate experience prior to all thought,” and to thoseoperations on and methods of reasoning about such objects which do notrequire the introduction of abstract concepts, in particular, withoutappeal to completed infinite totalities.

There are several basic and interrelated issues in understandingHilbert’s finitary standpoint:

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

2.1 Finitary objects and finitist epistemology

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

[A]s a condition for the use of logical inferences and the performanceof logical operations, something must already be given to our facultyof representation, certain extralogical concrete objects that areintuitively present as immediate experience prior to all thought. Iflogical inference is to be reliable, it must be possible to surveythese objects completely in all their parts, and the fact that theyoccur, that they differ from one another, and that they follow eachother, or are concatenated, is immediately given intuitively, togetherwith the objects, as something that can neither be reduced to anythingelse nor requires reduction. This is the basic philosophical positionthat I consider requisite for mathematics and, in general, for allscientific thinking, understanding, and communication. (Hilbert, 1926, 376)

These objects are, for Hilbert, thesigns. For the domain ofcontentual number theory, the signs in question are numerals suchas

1, 11, 111, 11111

The question of how exactly Hilbert understood the numerals isdifficult to answer. They are not physical objects (actual strokes onpaper, for instance), since it must always be possible to extend anumeral by adding another stroke (and, as Hilbert also argues in“On the infinite” (1926), it is doubtful that the physical universe is infinite). According toHilbert (1922b, 202), their “shape can be generally and certainly recognized byus—independently of space and time, of the special conditions ofthe production of the sign, and of the insignificant differences inthe finished product.” They are not mental constructions, sincetheir properties are objective, yet their existence is dependent ontheir intuitive construction (seeBernays 1923, 226). What is clear in any case is that they are logically primitive,i.e., they are neither concepts (as Frege’s numbers are) norsets. What is important here is not primarily their metaphysicalstatus (abstract versus concrete in the current sense of these terms),but that they do not enter into logical relations, e.g., they cannotbe predicated of anything. In Bernays’s most maturepresentations of finitism (Hilbert and Bernays, 1939;Bernays, 1930), the objects of finitism are characterized asformalobjects which are recursively generated by a process ofrepetition; the stroke symbols are then concrete representations ofthese formal objects.

The question of what Hilbert thought the epistemological status of theobjects of finitism was is equally difficult. In order to carry outthe task of providing a secure foundation for infinitisticmathematics, access to finitary objects must be immediate and certain.Hilbert’s philosophical background was broadly Kantian, as wasBernays’s, who was closely affiliated with the neo-Kantianschool of philosophy around Leonard Nelson in Göttingen.Hilbert’s characterization of finitism often refers to Kantianintuition, and the objects of finitism as objects given intuitively.Indeed, in Kant’s epistemology, immediacy is a definingcharacteristic of intuitive knowledge. The question is, what kind ofintuition is at play?Mancosu (1998b) identifies a shift in this regard. He argues that whereas theintuition involved in Hilbert’s early papers was a kind ofperceptual intuition, in later writings (e.g.,Bernays 1928a) it is identified as a form of pure intuition in the Kantian sense.However, at roughly the same timeHilbert (1928, 469) still identifies the kind of intuition at play as perceptual. In (1931b, 266–267), Hilbert sees the finite mode of thought as a separatesource ofa priori knowledge in addition to pure intuition(e.g., of space) and reason, claiming that he has “recognizedand characterized the third source of knowledge that accompaniesexperience and logic.” Both Bernays and Hilbert justify finitaryknowledge in broadly Kantian terms (without however going so far as toprovide a transcendental deduction), characterizing finitary reasoningas the kind of reasoning that underlies all mathematical, and indeed,scientific, thinking, and without which such thought would beimpossible. (SeeKitcher 1976 andParsons 1998 on the epistemology of finitism,Patton 2014 for historical and philosophical context of Hilbert’s theory ofsigns, andEder (forthcoming) specifically on the ensuing debate with the German philosopher AloysMüller.)

2.2 Finitarily meaningful propositions and finitary reasoning

The most basic judgments about finitary numerals are those aboutequality and inequality. In addition, the finite standpoint allowsoperations on finitary objects. Here the most basic is that ofconcatenation. The concatenation of the numerals 11 and 111 iscommunicated as “\(2 + 3\),” and the statement that 11concatenated with 111 results in the same numeral as 111 concatenatedwith 11 by “\(2 + 3 = 3 + 2\).” In actual proof-theoreticpractice, as well as explicitly in (Hilbert and Bernays, 1934;Bernays, 1930), these basic operations are generalized to operationsdefined by recursion, paradigmatically, primitive recursion, e.g.,multiplication and exponentiation (seeParsons 1998 for philosophical difficulties in relation to exponentiation and2007 for an extended discussion of intuitive mathematics and finitism).Similarly, finitary judgments may involve not just equality orinequality but also basic decidable properties, such as “is aprime.” This is finitarily acceptable as long as thecharacteristic function of such a property is itself finitary: Forinstance, the operation which transforms a numeral to 1 if it is primeand 11 otherwise can be defined by primitive recursion and is hencefinitary. Such finitary propositions may be combined by the usuallogical operations of conjunction, disjunction, negation, but alsobounded quantification. (Hilbert, 1926) gives the example of the proposition that “there is a primenumber between \(p + 1\) and \(p! + 1\)” where \(p\) is acertain large prime. This statement is finitarily acceptable since it“serves merely to abbreviate the proposition” that either\(p + 1\) or \(p + 2\) or \(p + 3\) or … or \(p! + 1\) is aprime.

The problematic finitary propositions are those that express generalfacts about numerals such as that, for any given numeral \(n, 1+n =n+1\). It is problematic because, as Hilbert puts it, it “isfrom the finitist point of viewincapable of beingnegated” (1926, 378). By this he means that the contradictory proposition that thereis a numeral \(n\) for which \(1+n \ne n+1\) is not finitarilymeaningful. “One cannot, after all, try out all numbers” (1928, 470). For the same reason, a finitary general proposition is not tobe understood as an infinite conjunction but “only as ahypothetical judgment that comes to assert something when a numeral isgiven” (ibid.). Even though they are problematic in this sense,general finitary statements are of particular importance toHilbert’s proof theory, since the statement of consistency of aformal system \(S\) is of such a general form: for any given sequenceof formulas \(P, P\) is not a derivation of a contradiction in\(S\).

2.3 Finitary operations and finitary proof

Of crucial importance to both an understanding of finitism and ofHilbert’s proof theory is the question of what operations andwhat principles of proof should be allowed from the finitiststandpoint. That a general answer is necessary is clear from thedemands of Hilbert’s proof theory, i.e., it is not to beexpected that given a formal system of mathematics (or even a singlesequence of formulas) one can “see” that it is consistent(or that it cannot be a genuine derivation of an inconsistency) theway we can see, e.g., that \(11 + 111 = 111 + 11\). What is requiredfor a consistency proof is an operation which, given a formalderivation, transforms such a derivation into one of a special form,plus proofs that the operation in fact does this and that proofs ofthe special kind cannot be proofs of an inconsistency. To count as afinitary consistency proof, the operation itself must be acceptablefrom the finitist standpoint, and the proofs required must use onlyfinitarily acceptable principles.

Hilbert never gave a general account of which operations and methodsof proof are acceptable from the finitist standpoint, but onlyexamples of operations and methods of inference in contentual finitarynumber theory which he accepted as finitary. Contentual induction wasaccepted in its application to finitary statements of thehypothetical, general kind explicitly inHilbert (1922b). He (1923, 1139) said that intuitive thought “includes recursion andintuitive induction for finite existing totalities,” and usedexponentiation in an example in1928.Bernays (1930) explained how exponentiation may be understood as afinitary operation on numerals.Hilbert and Bernays (1934) give the only general account of finitary contentual number theory;according to it, operations defined by primitive recursion and proofsusing induction are finitarily acceptable. All of these methods can beformalized in a system known as primitive recursive arithmetic(\(\PRA\)), which allows definitions of functions by primitiverecursion and induction on quantifier-free formulas (ibid.). However,neither Hilbert nor Bernays ever claimed thatonly primitiverecursive operations count as finitary, and they in fact did use somenon-primitive recursive methods in ostensibly finitary consistencyproofs already in 1923 (seeTait 2002 andZach 2003).

The more interesting conceptual issue is which operationsshould be considered as finitary. Since Hilbert was less thancompletely clear on what the finitary standpoint consists in, there issome leeway in setting up the constraints, epistemological andotherwise, an analysis of finitist operation and proof must fulfill.Hilbert characterized (see above) the objects of finitary numbertheory as “intuitively given,” as “surveyable in alltheir parts,” and said that their having basic properties must“exist intuitively” for us.Bernays (1922, 216) suggests that in finitary mathematics, only “primitiveintuitive cognitions come into play,” and uses the term“point of view of intuitive evidence” in connection withfinitism1930, 250. This characterization of finitism as primarily to do withintuition and intuitive knowledge has been emphasized inparticular by (Parsons, 1998) who argues that what can count as finitary on this understanding isnot more than those arithmetical operations that can be defined fromaddition and multiplication using bounded recursion. In particular,according to him, exponentiation and general primitive recursion arenot finitarily acceptable.

The thesis that finitism coincides with primitive recursive reasoninghas received a forceful defense by (Tait 1981; see also2002,2005b,2019). Tait, in contrast to Parsons, rejects the aspect of representabilityin intuition as the hallmark of the finitary; instead he takesfinitary reasoning to be “a minimal kind of reasoningpresupposed by all non-trivial mathematical reasoning aboutnumbers.” and analyzes finitary operations and methods of proofas those that are implicit in the very notion of number as the form ofa finite sequence. This analysis of finitism is supported byHilbert’s contention that finitary reasoning is a preconditionfor logical and mathematical, indeed any scientific thinkingHilbert (1931b, 267). Since finitary reasoning is that part of mathematics which ispresupposed by all non-trivial reasoning about numbers, it is, soTait, “indubitable” in a Cartesian sense, and thisindubitability as all that would be required of finitary reasoning toprovide the epistemological grounding of mathematics Hilbert intendedit for.

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

Tait’s technical analysis yields that the finitistic functionsare exactly the primitive recursive ones, and the finitisticnumber-theoretic truths are exactly those provable in the theory ofprimitive recursive arithmetic \(\PRA.\) It is important to stressthat this analysis is not carried out from within the finitistviewpoint itself. Since the general notions of “function”and “proof” are not themselves finitary, the finitist isunable to make sense of Tait’s thesis that everything provablein \(\PRA\) is finitistically true. According to Tait, a properanalysis of finitistic provability must not assume that finitismitself has access to such non-finitistic notions. Kreisel’sapproach and some criticisms of Tait that rely on reflectionprinciples or \(\omega\)-rules run afoul of this requirement (see Tait2002,2005b). On the other hand, one could argue that \(\PRA\) is toostrong a theory to count as a formalization of what is“presupposed by all non-trivial mathematical reasoning aboutnumbers”: there are weaker but non-trivial theories which arerelated to smaller classes of functions than the primitive recursiveones, such as \(\PV\) and \(\EA\), related to the polynomial-time andKalmar-elementary functions respectively (seeAvigad 2003 on how much mathematics can be carried out in \(\EA)\). Using ananalysis along the same lines as Tait’s,Ganea (2010) has arrived at the corresponding class of Kalmar-elementary functionsas those that are finitistic. See alsoIncurvati (2019) for further analysis of different notions of finitism.

3. Formalism, reductionism and instrumentalism

Weyl (1925) was a conciliatory reaction to Hilbert’s proposal in1922b and1923, which nevertheless contained some important criticisms. Weyldescribed Hilbert’s project as replacing contentual mathematicsby a meaningless game of formulas. He noted that Hilbert wanted to“secure nottruth, but theconsistency ofanalysis” and suggested a criticism that echoes an earlier oneby Frege: Why should we take consistency of a formal system ofmathematics as a reason to believe in the truth of the pre-formalmathematics it codifies? Is Hilbert’s meaningless inventory offormulas not just “the bloodless ghost of analysis”? Weylsuggested a solution:

[I]f mathematics is to remain a serious cultural concern, then somesense must be attached to Hilbert’s game of formulae,and I see only one possibility of attributing it (including itstransfinite components) an independent intellectual meaning. Intheoretical physics we have before us the great example of a [kind of]knowledge of completely different character than the common orphenomenal knowledge that expresses purely what is given in intuition.While in this case every judgment has its own sense that is completelyrealizable within intuition, this is by no means the case for thestatements of theoretical physics. In that case it is ratherthesystem as a whole that is in question if confronted withexperience. (Weyl, 1925, 140)

The analogy with physics is striking, and one can find similar ideasin Hilbert’s own writing—perhaps Hilbert was influenced inthis by Weyl. Although Hilbert’s first proposals focusedexclusively on consistency, there is a noticeable development inHilbert’s thinking in the direction of a general reductivistproject of a sort quite common in the philosophy of science at thetime (as was pointed out byGiaquinto 1983). In the second half of the 1920s, Hilbert replaced the consistencyprogram with a conservativity program: Formalized mathematics was tobe considered by analogy with theoretical physics. The ultimatejustification for the theoretical part lies in its conservativity over“real” mathematics: whenever theoretical,“ideal” mathematics proves a “real”proposition, that proposition is also intuitively true. This justifiesthe use of transfinite mathematics: it is not only internallyconsistent, but it proves only true intuitive propositions (and indeedall, since a formalization of intuitive mathematics is part of theformalization of all mathematics).

In1926, Hilbert introduced a distinction between real and ideal formulas.This distinction was not present in1922b and only hinted at in1923. In the latter, Hilbert presents first a formal system ofquantifier-free number theory about which he says that “Theprovable formulae we acquire in this way all have the character of thefinite” (1139). Then the transfinite axioms (i.e., quantifiers)are added to simplify and complete the theory (1144). Here he drawsthe analogy with the method of ideal elements for the first time:“In my proof theory, the transfinite axioms and formulae areadjoined to the finite axioms, just as in the theory of complexvariables the imaginary elements are adjoined to the real, and just asin geometry the ideal constructions are adjoined to the actual”(ibid). When Hilbert, in1926 explicitly introduces the notion of an ideal proposition, and in1928, when he first speaks ofreal propositions in addition to theideal, he is quite clear that the real part of the theory consistsonly of decidable, variable-free formulas. They are supposed to be“directly capable of verification”—akin topropositions derived from laws of nature which can be checked byexperiment (1928, 475). The new picture of the program was this: Classical mathematicsis to be formalized in a system which includes formalizations of allthe directly verifiable (by calculation) propositions of contentualfinite number theory. The consistency proof should show that all realpropositions which can be proved by ideal methods are true, i.e., canbe directly verified by finite calculation. (Actual proofs such as the\(\varepsilon\)-substitution had always been of such a kind: providefinitary procedures which eliminate transfinite elements from proofsof real statements, in particular, of \(0 = 1\).) Indeed, Hilbert sawthat something stronger is true: not only does a consistency proofestablish truth of real formulas provable by ideal methods, but ityields finitary proofs of finitary general propositions if thecorresponding free-variable formula is derivable by ideal methods (1928, 474).

Hilbert suggested further restrictions on the theory in addition toconservativity: simplicity, brevity of proofs, “economy ofthought” and mathematical productivity. The formal system oftransfinite logic is not arbitrary: “This formula game iscarried out according to certain definite rules, in which thetechnique of our thinking is expressed. […] Thefundamental idea of my proof theory is none other than to describe theactivity of our understanding, to make a protocol of the rulesaccording to which our thinking actually proceeds” (Hilbert 1928, 475). WhenWeyl (1928) eventually turned away from intuitionism, he emphasized thismotivation of Hilbert’s proof theory: not to turn mathematicsinto a meaningless game of symbols, but to turn it into a theoreticalscience which codifies scientific (mathematical) practice (seeMancosu and Ryckman 2002 andKish Bar-On 2021 on Weyl’s relationship to intuitionism and Hilbert’sformalism).

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

Most philosophers of mathematics writing on Hilbert have read him asan instrumentalist (includingKitcher 1976,Resnik 1980,Giaquinto 1983,Sieg 1990, and in particularDetlefsen 1986) in that they read Hilbert’s explanation that the idealpropositions “have no meaning in themselves” (Hilbert, 1926, 381) as claiming that classical mathematics is amereinstrument, and that statements of transfinite mathematics have notruth value. To the extent that this is accurate, it must beunderstood as a methodological instrumentalism: A successful executionof the proof-theoretic program would show that one could pretendas if mathematics was meaningless. The analogy with physicsis therefore not: transfinite propositions have no meaning just aspropositions involving theoretical terms have no meaning, but:transfinite propositions require no direct intuitive meaning just asone does not have to directly see electrons in order to theorize aboutthem.Hallett (1990), taking into account the 19th century mathematical background fromwhich Hilbert came as well as published and unpublished sources fromHilbert’s entire career (in particularHilbert 1992, the most extensive discussion of the method of ideal elements) comesto the following conclusion:

[Hilbert’s treatment of philosophical questions] isnotmeant as a kind of instrumentalist agnosticism about existence andtruth and so forth. On the contrary, it is meant to provide anon-skeptical and positive solution to such problems, a solutioncouched in cognitively accessible terms. And, it appears, the samesolution holds for both mathematical and physical theories. Once newconcepts or “ideal elements” or new theoretical terms havebeen accepted, then they exist in the sense in whichanytheoretical entities exist. (Hallett, 1990, 239)

4. Hilbert’s Program and Gödel’s incompleteness theorems

There has been some debate over the impact ofGödel’s incompleteness theorems on Hilbert’s Program, and whether it was the first or thesecond incompleteness theorem that delivered thecoup degrâce. Undoubtedly the opinion of those most directlyinvolved in the developments were convinced that the theorems did havea decisive impact. Gödel announced the second incompletenesstheorem in an abstract published in October 1930: no consistency proofof systems such asPrincipia,Zermelo-Fraenkel set theory, or the systems investigated by Ackermann and vonNeumann is possible by methods which can be formulated in thesesystems. In the full version of his paper,Gödel (1931) left open the possibility that there could be finitary methods whichare not formalizable in these systems and which would yield therequired consistency proofs. Bernays’s first reaction in aletter to Gödel in January 1931 was likewise that “if, asvon Neumann does, one takes it as certain that any and every finitaryconsideration may be formalized within the system \(P\)—likeyou, I regard that in no way as settled—one comes to theconclusion that a finitary demonstration of the consistency of \(P\)is impossible” (Gödel, 2003a, 87).

How do Gödel’s theorems impact Hilbert’s program?Through a careful (“Gödel”-) coding of sequences ofsymbols (formulas, proofs), Gödel showed that in theories \(T\)which contain a sufficient amount of arithmetic, it is possible toproduce a formula \(Pr(x, y)\) which “says” that \(x\) is(the code of) a proof of (the formula with code) \(y\). Specifically,if \(\ulcorner 0 = 1\urcorner\) is the code of the formula \(0 = 1\),then \(Con_T = \forall x \neg Pr(x,\ulcorner 0 = 1\urcorner)\) may betaken to “say” that \(T\) is consistent (no number is thecode of a derivation in \(T\) of \(0 = 1)\). The second incompletenesstheorem (G2) says that under certain assumptions about \(T\) and thecoding apparatus, \(T\) does not prove \(Con_T\). Now suppose therewere a finitary consistency proof of \(T\). The methods used in such aproof would presumably be formalizable in \(T\).(“Formalizable” means that, roughly, if the proof uses afinitary operation \(f\) on derivations which transforms anyderivation \(D\) into a derivation \(f (D)\) of a simple form; thenthere is a formula \(F(x, y)\) so that, for all derivations \(D,T\vdash F(\ulcorner D\urcorner ,\ulcorner f (D)\urcorner)\).) Theconsistency of \(T\) would be finitarily expressed as the generalhypothetical that, if \(D\) is any given sequence of symbols, \(D\) isnot a derivation in \(T\) of the formula \(0 = 1\). The formalizationof this proposition is the formula \(\neg Pr(x,\ulcorner 0 =1\urcorner)\) in which the variable \(x\) occurs free. If there were afinitary proof of the consistency of \(T\), its formalization wouldyield a derivation in \(T\) of \(\neg Pr_T (x,\ulcorner 0 =1\urcorner),\) from which \(Con_T\) can be derived in \(T\) by simpleuniversal generalization on \(x\). Yet, a derivation of \(Con_T\) in\(T\) is ruled out by G2.

As mentioned above, initially Gödel and Bernays thought that thedifficulty for the consistency proof of \(\PA\) could be overcome byemploying methods which, although not formalizable in \(\PA\), arenonetheless finitary. Whether such methods would be consideredfinitary according to the original conception of finitism orconstitute an extension of the original finitist viewpoint is a matterof debate. The new methods considered included a finitary version ofthe \(\omega\)-rule proposed by Hilbert (1931b;1931a). It is fair to say, however, that after about 1934 ithas been almost universally accepted that the methods of proofaccepted as finitary prior to Gödel’s results are allformalizable in \(\PA\). Extensions of the original finitiststandpoint have been proposed and defended on broadly finitarygrounds, e.g.,Gentzen (1936) defended the use of transfinite induction up to \(\varepsilon_0\) inhis consistency proof for \(\PA\) as “indisputable,”Takeuti (1987) gave another defense.Gödel (1958) presented another extension of the finitist standpoint; the work ofKreisel mentioned above may be seen as another attempt to extendfinitism while retaining the spirit of Hilbert’s originalconception.

A different attempt at providing a way around Gödel’ssecond theorem for Hilbert’s Program was proposed by Detlefsen (1986;2001;1979). Detlefsen presents several lines of defense, one of which is similarto the one just described: arguing that a version of the\(\omega\)-rule is finitarily acceptable, although not capable offormalization (however, seeIgnjatovic 1994). Detlefsen’s other argument against the common interpretation ofGödel’s second theorem focuses on the notion offormalization: That the particular formalization of “\(T\) isconsistent” by Gödel’s formula \(Con_T\) is notprovable does not imply that there couldn’t be other formulas,whichare provable in \(T\), and which have as much right tobe called “formalizations of the consistency of \(T\).”These rely on different formalizations of the provability predicate\(Pr_T\) than the standard ones. It is known that formalizedconsistency statements are unprovable whenever the provabilitypredicate obeys certain general derivability conditions. Detlefsenargues that these conditions are not necessary for a predicate tocount as a genuine provability predicate, and indeed there areprovability predicates which violate the provability conditions andwhich give rise to consistency formulas whichare provable intheir corresponding theories. These, however, depend on non-standardconceptions of provability which would likely not have been acceptedby Hilbert (see alsoResnik 1974,Auerbach 1992 andSteiner 1991).

Smorynski (1977) has argued that already the first incompleteness theorem defeatsHilbert’s Program. Hilbert’s aim was not merely to showthat formalized mathematics is consistent, but to do so in a specificway by showing that ideal mathematics can never lead to conclusionsnot in accord with real mathematics. Thus, to succeed, idealmathematics must beconservative over the real part: wheneverformalized ideal mathematics proves a real formula \(P, P\) itself (orthe finitary proposition it expresses) must be finitarily provable.For Smorynski the real formulas include not just numerical equalitiesand combinations thereof, but also general formulas with freevariables but without unbounded quantifiers.

Now Gödel’s first incompleteness theorem (G1) states thatfor any sufficiently strong, consistent formal theory \(S\) there is asentence \(G_S\) which is true but not derivable in \(S\). \(G_S\) isa real sentence according to Smorynski’s definition. Nowconsider a theory \(T\) which formalizes ideal mathematics and itssubtheory \(S\) which formalizes real mathematics. \(S\) satisfies theconditions of G1 and hence \(S\) does not derive \(G_S\). Yet, \(T\),being a formalization of all of mathematics (including what isrequired to see that \(G_S\) is true), does derive \(G_S\). Hence, wehave a real statement which is provable in ideal mathematics and notin real mathematics.

Detlefsen (1986, Appendix; see also1990) has defended Hilbert’s Program against this argument as well.Detlefsen argues that “Hilbertian” instrumentalism escapesthe argument from G1 by denying that ideal mathematics must beconservative over the real part; all that is required isreal-soundness. Hilbertian instrumentalism requires only that theideal theory not prove anything which is in conflict with the realtheory; it is not required that it proveonly real statementswhich the real theory also proves.

Franks (2009) has provided a related defense and re-evaluation of Hilbert’sproject, andMcCarthy (2016) an alternative approach to the provability of consistency and G2 dueto Gödel himself.Kripke (forthcoming) shows how Hilbert’s own approach to consistency proofsnaturally lead to Gödelian incompleteness.Santos et al. (forthcoming), expanding on work byArtemov (2020), argue that a “partial finitism” allows for consistencyproofs compatible with G2, and is in line with Hilbert’s ownpost-Gödelian views. See alsoSchirn and Niebergall (2001) andSchirn (2019)for related proposals.Zach (2004) provides historical detail on the issue of conservativity andconsistency in Hilbert’s program. See the entries onGödel andGödel’s incompleteness theorem, as well asCheng (2021), for further discussion on Gödel’s theorems and consistencyproofs.

5. Revised Hilbert Programs

Even if no finitary consistency proof of arithmetic can be given, thequestion of finding consistency proofs is nevertheless of value: themethods used in such proofs, although they must go beyondHilbert’s original sense of finitism, might provide genuineinsight into the constructive content of arithmetic and strongertheories. What Gödel’s result showed was that there can beno absolute consistency proof of all of mathematics; hence work inproof theory after Gödel concentrated on relative results, both:relative to the system for which a consistency proof was given, andrelative to the proof methods used.

Reductive proof theory in this sense has followed two traditions: thefirst, mainly carried out by proof theorists following Gentzen andSchütte, has pursued a program of what is calledordinalanalysis, and is exemplified by Gentzen’s first consistencyproof of \(\PA\) by induction up to \(\varepsilon_0 . \varepsilon_0\)is a certain transfinite (though countable) ordinal, however,“induction upto\(\varepsilon_0\)” in the sense usedhere is not a genuinely transfinite procedure. Ordinal analysis doesnot operate with infinite ordinal numbers, but rather withordinalnotation systems which themselves can be formalized in very weak(essentially, finitary) systems. An ordinal analysis of a system \(T\)is given if: (a) one can produce an ordinal notation system whichmimics the ordinals less than some ordinal \(\alpha_T\) so that (b) itcan be proved finitarily that the formalization \(TI(\alpha_T)\) ofthe principle of induction up to \(\alpha_T\) implies the consistencyof \(T\) (i.e., \(S \vdash TI(\alpha_T)\rightarrow Con_T)\) and (c)\(T\) proves \(TI(\beta)\) for all \(\beta \lt \alpha_T\) (\(S\) is atheory formalizing finitary metamathematics and is generally a weaksub-theory of \(T)\). To have any foundational significance it is alsorequired that one can give a constructive argument for transfiniteinduction up to \(\alpha_T\). As mentioned above, this was done for byGentzen and Takeuti for \(\varepsilon_0\), the proof theoretic ordinalof \(\PA\), but becomes more difficult and of progressivelyquestionable philosophical significance for stronger theories. See theentry onproof theory for a survey of Gentzen’s consistency proof,Mancosu et al. 2021 for an accessible textbook presentation, andThomas-Bolduc and Darnell 2022 on Takeuti’s well-ordering proof.

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

The program of so-called reverse mathematics developed by, inparticular, Friedman and Simpson, is another continuation ofHilbert’s program. In the face of Gödel’s resultsshowing that not all of classical mathematics can be reduced to thefinitary, they seek to answer the question: how much of classicalmathematics can be so reduced? Reverse mathematics seeks to give aprecise answer to this question by investigating which theorems ofclassical mathematics are provable in weak subsystems of analysiswhich are reducible to finitary mathematics (in the sense discussed inthe preceding paragraph). A typical result is that the Hahn-Banachtheorem of functional analysis is provable in a theory known as\(WKL_0\) (for “weak König lemma”); \(WKL_0\) isconservative over \(\PRA\) for \(\Pi^{0}_2\) sentences (i.e.,sentences of the form \(\forall x\exists yA(x, y)\). (SeeSimpson 1988 for an overview andSimpson 1999 for a technical treatment.)

Bibliography

An extended version of the first revision of this entry can be foundinZach (2006).

Other Internet Resources

[Please contact the author with suggestions.]

Copyright © 2023 by
Richard Zach<rzach@ucalgary.ca>

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free

Browse

About

Support SEP

Mirror Sites

View this site from another server:

USA (Main Site)Philosophy, Stanford University

The Stanford Encyclopedia of Philosophy iscopyright © 2023 byThe Metaphysics Research Lab, Department of Philosophy, Stanford University

Library of Congress Catalog Data: ISSN 1095-5054

[8]ページ先頭
©2009-2025 Movatter.jp