Movatterモバイル変換

• Back to Entry
• Entry Contents
• Entry Bibliography
• Academic Tools
• Friends PDF Preview
• Author and Citation Info
• Back to Top

1. The evolution of this methodological perspective to formal axiomaticsis described inAppendix A.

2. The term “finit” is used without much explanation; one isled to think that it was a thoroughly familiar one. Indeed, the 1919article by Bernstein calls “finit” all considerations thathave a constructive feature, from Kronecker through Poincaré toBrouwer. It is obviously used also to emphasize the contrast with“transfinit”. The term was also prominently used by WeylinDas Kontinuum (1918).

3.Primitive recursion is given by theequations

and

whereS is the successor function andg,h arepreviously defined primitive recursive functions. The class ofprimitive recursive functions is obtained from the constant 0function,S and the projection functions\(P^i_n(x_1,\ldots,x_n)=x_i\) by closure under composition and theabove recursion schema.

The language ofPRA has the equality symbol = and function symbols for all primitive recursive functions. The axioms ofPRA consist of the defining equations for the primitive recursive functions and the induction scheme \[{A(0)} \land {\forall x[A(x)\to A(Sx)]\to \forall x A(x)}\]for atomic formulas \(A(x)\). Note that atomic formulas \(A(x)\) ofPRA are of the form \(t_1(x)=t_2(x)\) for terms \(t_1(x)\) and \(t_2(x)\).

4. Many contemporary writers consider Hilbert 1922 as the beginning ofHilbert’s finitist program; see, for example, Franks 2009. However, Hilbert’spaper is split into two parts, according to the editors of the thirdvolume of Hilbert’sGesammelte Abhandlungen in which itwas republished: the first part stems from the older considerationsthat go back to the Heidelberg talk (Hilbert 1905); seeappendix A.3. In the second part a new direction is taken that involves asignificantly expanded formal theory; however, the theory is by design“constructive”, as negation is applied only to equations.A consistency proof for this expanded theory is not presented andcould not be obtained by the old techniques; the result, when suitablyrestricted as the Editors of the volume suggest, can be obtained bythe methods introduced in early 1922. It is only then that thefinitist standpoint is taken.

5. There is a delicate evolution from “tau” to“epsilon” that can be followed in Ewald and Sieg 2013;here we use directly the epsilon terms.

6. The so-called \(\varepsilon\)-substitution method has beenre-invigorated by work of Tait and Mints; a broad survey is given inAvigad and Zach 2007.

7. The Ackermann function was included among Herbrand’s finitistfunctions. At this point, the systemF was not“identified” withPRA.

8. See, for detailed discussion, mathematical analysis and additionalreferences, Tait 2002 and Feferman & Strahm 2010. A penetratingexplication of the finitist standpoint taken by Hilbert and Bernays isgiven in Ravaglia 2003.

9. Hilbert’s considerations are analyzed in Sieg 2012 (section 5)and are also discussed in Hallett 2013.

10. For the close connections between Hilbert’s proposal andGentzen’s attempt to mould it into a consistency proof, seesection 6 of Sieg 2012. The work in Gentzen’s“Urdissertation” is described in von Plato 2008 and2009.

11. For instance through an ordinal analysis as explained inDefinition 3.4.

12. For a detailed descriptions of natural deduction calculi see Prawitz1965 or Troelstra & Schwichtenberg 2000. To achieve a moresymmetric treatment of negation one can replace in the above axiomaticformulation theprinciple of double negation by the axiom\((B\land\neg B)\to A\) (to obtain intuitionist logic) and by the axiom\((\neg A\to (B\land\neg B))\to A\) (to obtain classical logic).

13. TheHauptsatz states informally, according to Gentzen (1934/35:177), that every purelylogical proof can be transformed into a certain, by no means unique,normal form. One of the essential properties of such normal proofs isexpressed by: “It does not make detours”.

14. Though the crucial paper was published only in 1958, the centralideas of the “Dialectica Interpreation” go back tolectures Gödel presented at Yale in April of 1941. See Gödel1942 in volume III of hisCollected Works.

15. Both Brouwer (1927) and Zermelo (1932), from dramatically differentfoundational perspectives, considered infinite proofs. Indeed, Brouwerasserted concerning his infinite proofs:

These mental mathematical proofs that in general contain infinitelymany terms must not be confused with their linguistic accompaniments,which are finite and necessarily inadequate, hence do not belong tomathematics. (Brouwer 1927: 460, note 8).

He added that this remark contains his “main argument againstthe claims of Hilbert’s metamathematics”.

16. “Because of Gödel’s result consistency proofs nowrequire a method that is finite (or constructive) but which isnevertheless very strong when formalized. People think this isimpossible or at least unlikely and extremely difficult. The situationis somewhat similar to that of finding a new axiom that carriesconviction and decides the continuum hypothesis”. (Takeuti 1975:366)

17. Terms have to be of appropriate type, e.g., in (2) below,tandr have to be of type 0 while in (3)s andthave to be of type \(\sigma\) and \(\tau\), respectively. The requiredtyping should always be clear from the context.

18. “Having proposed the fundamental conjecture, I concentrated onits proof and spent several years in an anguished struggle trying toresolve the problem day and night” (Takeuti 2003: 133).

19. Below in \((\forall_2\bL)\) and \((\exists_2\rR)\), \(A(a)\) is anarbitrary formula. The variableU in \((\forall_2\rR)\) and\((\exists_2\bL)\) is an eigenvariable of the respective inference,i.e.,U is not to occur in the lower sequent.

20. Meaning that it proves the same formulae as the system with cuts.

21. In the 1970s Martin-Löf gave a normalization proof for a typetheory with a universe that contained itself. The metatheory for thisproof was basically a slight extension of the same type theory.Ironically, it turned out that the type theory was inconsistent.

22. Below Con(T) andProof\(_\bT\)are arithmetized formalizations of the consistency ofT andprovability inT, respectively, as explained inDefinition 1.3. \(\Corner{F}\) denotes the Gödel number of a formulaF.For every numbern, \(\bar{n}\) denotes the \(n^{th}\) numeral,i.e., the term obtained from 0 by puttingn successor functionsymbols in front of it.

23. This is straightforward for languages allowing for quantifiers oversets of natural numbers, but for theories likePA onewould have to add a new predicate symbol to the language.

24. Recall that the class of arithmetical formulae is denoted by\(\Pi^1_0\). These formulae can still contain free set variables whichcan be utilized to show that\((\Pi^1_0\Hy\bCA)_0=(\Pi^0_1\Hy\bCA)_0\).

25. They were re-obtained in purely proof-theoretic ways (andgeneralized) by Feferman & Sieg (1981b).

26. The attribute “reverse” comes from this additionalobjective:When a theorem is proved from the right axioms, theaxioms can be proved from the theorem.

27. Ironically, the counterexamples that come to mind as soon as onebegins to think about it come from one of the main inventors ofreverse mathematics.

28. Using classical logic and just the connectives \(\land\),\(\lor\),\(\neg\) and quantifiers \(\forall\), \(\exists\), any formula can bere-written in such a way that the negation sign occurs only in frontof atomic formulas. A formula of the latter form isP-positiveifP does not appear negated in it.

29. The extension then has ordinals \(\Omega_{\alpha}\) for all\(\alpha\leq\nu\) and each ordinal of the form \(\Omega_{\beta+1}\)gets furnished with its own collapsing function\(\psi_{\!_{\Omega_{\beta+1}}}\).

30. For a detailed account of the history of the proof theory of iteratedinductive definitions see Buchholz et al. 1981.

31. Upper bounds for (i) and (iii) are due to Takeuti (1967) while upperbounds for (iv) and (v) are owed to Takeuti and Yasugi (1973). Theexacts bound in (iii) and (ii) are due to Pohlers (1977) and Buchholz(1977a), respectively. Otherexact bounds involve the work of several people.

32. The Hilbert project has produced three volumes of unpublished lecturenotes and material that is no longer easily accessible, for examplethe original first edition ofGrundlagen der Geometrie andthat of the 1928 book of Hilbert and Ackermann. Associated with theedition and study of that material is also a rich secondary literaturewith papers, for example, by Mancosu (1998, 1999a) and Zach (2003,2004).

33. Proof-theoretic studies play an important role in areas such astemporal and modal logics with applications to software verification.Linear logic and the other substructural logics are being usedsuccessfully in linguistics. Here the computational aspects of thelogics are important, and the development of proof systems for suchlogics aims to find systems that are both expressive and efficient.Our list of “Related Entries” below points the interestedreader to information concerning these logics and theirapplications.

34. The best-known systems are Coq, Isabel, HOL, and the more recenttheorem prover Lean. Sieg has developed with collaborators and students the system AProS; see www.phil.cmu.edu/projects/apros.

35. These four conditions correspond to the conditions \((\alpha)\)through \((\delta)\) of \(\#71\) in Dedekind 1888; they are easilyseen to be equivalent to the so-called Peano axioms. Thechain of the system \(\{1\}\) (with respect to the mapping\(\varphi\) ofN) is the intersection of all systems thatcontain 1 as an element and are closed under \(\varphi\).

36. In Torretti 1978 [1984: 234], for example, one finds the followingobservation:

… the completeness axiom is what nowadays one would call ametamathematical statement, though one of a rather peculiar sort,since the theory with which it is concerned includes Axiom V2 [i.e.,the completeness axiom] itself.

37. We have modified the translation one finds in theCollectedWorks. In particular, logical expression stands forlogischerAusdruck, satisfy forerfüllen, domain of thoughtforDenkbereich, statement forAussage, andproposition forSatz.

38. InOn the Infinite Hilbert writes retrospectively:

In particular, a contradiction discovered by Zermelo and Russell had,when it became known, a downright catastrophic effect in the world ofmathematics. (Hilbert 1926: 375)

More can be learnt about Hilbert’s reaction at the time fromvarious reports in 1902 and 1903 (cf. Peckhaus 1990: 57).

39. One should keep in mind that the “existence of sets” wasthe central issue, and it was to be guaranteed by the consistency ofan appropriate axiom system, a viewpoint shared by Poincaré.The latter was, on the whole, impressed by Hilbert’s novelapproach.

40. See Mancosu 1999b. Not only the details ofPrincipiaMathematica were of significance; on the contrary, the broadlogicist outlook had a real impact on Hilbert. Hilbert’s notesfor a course onSet Theory (from the summer term 1917) andhis talkAxiomatisches Denken reveal a logicist direction inhis work. In the latter essay Hilbert writes:

The examination of consistency is an unavoidable task; thus, it seemsto be necessary to axiomatize logic itself andto show that numbertheory as well as set theory are just parts of logic. (Hilbert 1918: 153).

If we try to achieve such a reduction to logic, Hilbert says at thevery end of the set theory notes, “… we are facing one ofthe most difficult problems of mathematics”. (Hilbert 1917)

41. This is reported in Dawson 1997 (p. 68) based on doc 023-73-04 in theCarnap Nachlass at the University of Pittsburgh.

42. Volume III of Gödel’s Collected Works contains a paperentitled “Vortrag über Vollständigkeit desFunktionenkalkül’s” that is taken to be themanuscript for his talk in Königsberg. However,Gödel’s talk was a contributed talk of just 20 minutes;only a small part of the paper could have been delivered.

43. The historical context and relevant details are presented in Sieg2012.

44. More precisely, we define a functionCODEby recursion on formulae that associateswith each formula \(\varphi\) a term in the language of\(T\), which is also denoted by \({\Corner{\varphi}}\).

45. The representability conditions forPROOFare as follows: IfPROOF\((D,\varphi)\) then \(T \vdash\iproof(\Corner{D},\Corner{\varphi})\), and ifNOTPROOF\((D,\varphi)\) then \(T\vdash \neg\iproof(\Corner{D},\Corner{\varphi})\).

46. Note thatG is, as Dawson put it (on p. 68), “aninvolved combinatorial statement expressed in the richer language ofthe system ofPrincipia Mathematica” (or set theory).It is only after the “arithmetization of syntax” and therepresentation of the syntactic notions in elementary number theorythatG is turned into an arithmetical statement; section 3 ofGödel 1931a. See the remarks below from Wang 1981 concerning thisdevelopment after the Königsberg conference, and the further verydetailed description of howG is equivalent to a Diophantineequation in section 8 of Gödel’s 1934 Princeton lecturesand in Gödel 1938/9.

47. The letter, to the best of our knowledge, has not been published. One of the authors, Sieg, had received a copy from Chevalley’s daughter quite a few years ago.

48. As to the details of their interaction, see the Introductory Notes toGödel’s correspondence with von Neumann and Herbrand, involume V of theCollected Works. Gödel’s contraryperspective on the formalizability of finitist proofs is expressed notonly at the end of his 1931 paper, but also in his letters to vonNeumann and Herbrand, as well as in his contribution to the meeting ofthe Schlick Circle on 15 January 1931 and in the“Nachtrag” to his Königsberg remarks. In thelatter he wrote:

For a system in which all finitist (i.e., intuitionistically proper)forms of proof are formalized, a finitist consistency proof as soughtby the formalists would be altogether impossible. However, it seemsdoubtful, whether one of the systems formulated up to now, sayPrincipia Mathematica, is so comprehensive (or whether such acomprehensive system exists at all). (Gödel 1931b: 204).

49. The usual recursion theorem is formulated for partial recursivefunctions but there is a version, due to Kleene (1958), that works forprimitive recursive functions.

50. Accessible accounts can be found in Torkel Franzén’sbook (2004a) and his paper (2004b).

51. Brouwer did not include (Hyp 2) among the hypothesis. It expressesthe “monotonicity” of the bar. Classically it’srather superfluous but intuitionistically it is essential as Kleeneobserved: \(\BI_{\igen}\) formulated without (Hyp 2) yields instancesof excluded middle that are incompatible with Brouwer’scontinuity principles (Kleene & Vesley 1965: 7.14).

52. A barB gives rise to a well-founded ordering \(\prec\) on\(\bbN^*\) where \(t\prec s\) means thatt is a node aboves and \(t\notin B\). Viewed in this way, \(\BI_{\igen}\) is aprinciple of transfinite induction along \(\prec\). For theimplication \(\BI_{\igen}\to{\bCA}\) to hold it is important thatB can be of arbitrary complexity. Thus the moral drawable fromthis is that impredicative comprehension can be deduced fromtransfinite induction on impredicatively defined orderings.

53. Girard is also very skeptical about the intuitionistic setting ofSpector’s interpretation: “all these topics havenothing to do with intuitionism” (Girard 1987:479).

54. As a matter of clarification, cut free proofs are not allowed tocontain other instances of \(\tilde{\Omega}\).

55. For more background information see Takeuti 1985: 259; Feferman 1989:362,and Pohlers 1991: 374.

56. For more details see Rathjen 1999a.

57. For more details see Rathjen 2015. As for the unprovability of\(\Con(\PA)\) inPA, Gentzen (1943) explicitly statesthat his proof makes no appeal to the second incompletenesstheorem.

58. In Rathjen 2015 the question is pondered whether the latter resultcould have been proved much earlier (from a technical as well associological point of view).

59. For extensions and reflections see Sieg 1991.

60.Theorem F.4 can be extracted from Kreisel, Mints and Simpson (1975),Lopez-Escobar (1976) or Schwichtenberg (1977) and was certainly knownto these authors.