Some quantitative results obtained by proof mining take the form of Herbrand disjunctions that may depend on additional parameters. We attempt to elucidate this fact through an extension to first-order arithmetic of the proof of Herbrand’s theorem due to Gerhardy and Kohlenbach which uses the functional interpretation.

The Hilbert program was actually a specific approach for proving consistency, a kind of constructive model theory. Quantifiers were supposed to be replaced by ε-terms. εxA(x) was supposed to denote a witness to ∃xA(x), or something arbitrary if there is none. The Hilbertians claimed that in any proof in a number-theoretic system S, each ε-term can be replaced by a numeral, making each line provable and true. This implies that S must not only be consistent, but also 1-consistent. Here we (...) show that if the result is supposed to be provable within S, a statement about all Pi-0-2 statements that subsumes itself within its own scope must be provable, yielding a contradiction. The result resembles Gödel's but arises naturally out of the Hilbert program itself. (shrink)

In the Handbook of Mathematical Logic, the Paris-Harrington variant of Ramsey's theorem is celebrated as the first result of a long ‘search’ for a purely mathematical incompleteness result in first-order Peano arithmetic. This paper questions the existence of any such search and the status of the Paris-Harrington result as the first mathematical incompleteness result. In fact, I argue that Gentzen gave the first such result, and that it was restated by Goodstein in a number-theoretic form.

In the early 1920s, the German mathematician David Hilbert (1862–1943) put forward a new proposal for the foundation of classical mathematics which has come to be known as Hilbert's Program. It calls for a formalization of all of mathematics in axiomatic form, together with a proof that this axiomatization of mathematics is consistent. The consistency proof itself was to be carried out using only what Hilbert called “finitary” methods. The special epistemological character of finitary reasoning then 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 back until around 1900, when he first pointed out the necessity of giving a direct consistency proof of analysis. Work on the program progressed significantly in the 1920s with contributions from logicians such as Paul Bernays, Wilhelm Ackermann, John von Neumann, and Jacques Herbrand. It was also a great influence on Kurt Gödel, whose work on the incompleteness theorems were motivated by Hilbert's Program. Gödel's work is generally taken to show that Hilbert's Program cannot be carried out. It has nevertheless continued to be an influential position in the philosophy of mathematics, and, starting with the work of Gerhard Gentzen in the 1930s, work on so-called Relativized Hilbert Programs have been central to the development of proof theory. (shrink)

Herbrand's Theorem, in the form of $$\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{\exists } $$ -inversion lemmata for finitary and infinitary sequent calculi, is the crucial tool for the determination of the provably total function(al)s of a variety of theories. The theories are (second order extensions of) fragments of classical arithmetic; the classes of provably total functions include the elements of the Polynomial Hierarchy, the Grzegorczyk Hierarchy, and the extended Grzegorczyk Hierarchy $\mathfrak{E}^\alpha $ , α < ε0. A subsidiary aim of the paper is to show (...) that the proof theoretic methods used here are distinguished by technical elegance, conceptual clarity, and wide-ranging applicability. (shrink)

I attribute an 'intensional reading' of the second incompleteness theorem to its author, Kurt G del. My argument builds partially on an analysis of intensional and extensional conceptions of meta-mathematics and partially on the context in which G del drew two familiar inferences from his theorem. Those inferences, and in particular the way that they appear in G del's writing, are so dubious on the extensional conception that one must doubt that G del could have understood his theorem extensionally. However, (...) on the intensional conception, the inferences are straightforward. For that reason I conclude that G del had an intensional understanding of his theorem. Since this conclusion is in tension with the generally accepted view of G del's understanding of mathematical truth, I explain how to reconcile that view with the intensional reading of the theorem that I attribute to G del. The result is a more detailed account of G del's conception of meta-mathematics than is currently available. (shrink)

In the course of ten short sections, we comment on Gödel's seminal dialectica paper of fifty years ago and its aftermath. We start by suggesting that Gödel's use of functionals of finite type is yet another instance of the realistic attitude of Gödel towards mathematics, in tune with his defense of the postulation of ever increasing higher types in foundational studies. We also make some observations concerning Gödel's recasting of intuitionistic arithmetic via the dialectica interpretation, discuss the extra principles that (...) the interpretation validates and comment on extensionality and higher order equality. The latter sections focus on the role of majorizability considerations within the dialectica and related interpretations for extracting computational information from ordinary proofs in mathematics. (shrink)

The last section of “Lecture at Zilsel’s” [9, §4] contains an interesting but quite condensed discussion of Gentzen’s first version of his consistency proof for P A [8], reformulating it as what has come to be called the no-counterexample interpretation. I will describe Gentzen’s result (in game-theoretic terms), fill in the details (with some corrections) of Godel's reformulation, and discuss the relation between the two proofs.

The best known and most widely discussed aspect of Kurt Gödel's philosophy of mathematics is undoubtedly his robust realism or platonism about mathematical objects and mathematical knowledge. This has scandalized many philosophers but probably has done so less in recent years than earlier. Bertrand Russell's report in his autobiography of one or more encounters with Gödel is well known:Gödel turned out to be an unadulterated Platonist, and apparently believed that an eternal “not” was laid up in heaven, where virtuous logicians (...) might hope to meet it hereafter.On this Gödel commented:Concerning my “unadulterated” Platonism, it is no more unadulterated than Russell's own in 1921 when in the Introduction to Mathematical Philosophy … he said, “Logic is concerned with the real world just as truly as zoology, though with its more abstract and general features.” At that time evidently Russell had met the “not” even in this world, but later on under the infuence of Wittgenstein he chose to overlook it.One of the tasks I shall undertake here is to say something about what Gödel's platonism is and why he held it.A feature of Gödel's view is the manner in which he connects it with a strong conception of mathematical intuition, strong in the sense that it appears to be a basic epistemological factor in knowledge of highly abstract mathematics, in particular higher set theory. Other defenders of intuition in the foundations of mathematics, such as Brouwer and the traditional intuitionists, have a much more modest conception of what mathematical intuition will accomplish. (shrink)

The paper undertakes to characterize Hao Wang's style, convictions, and method as a philosopher, centering on his most important philosophical work From Mathematics to Philosophy, 1974. The descriptive character of Wang's characteristic method is emphasized. Some specific achievements are discussed: his analyses of the concept of set, his discussion, in connection with setting forth Gödel's views, of minds and machines, and his concept of ‘analytic empiricism’ used to criticize Carnap and Quine. Wang's work as interpreter of Gödel's thought and the (...) importance of his writings as a source are also discussed. (shrink)

is a fragment of first-order aritlimetic so weak that it cannot prove the totality of an iterated exponential fimction. Surprisingly, however, the theory is remarkably robust. I will discuss formal results that show that many theorems of number theory and combinatorics are derivable in elementary arithmetic, and try to place these results in a broader philosophical context.

In the 1920s, Ackermann and von Neumann, in pursuit of Hilbert's programme, were working on consistency proofs for arithmetical systems. One proposed method of giving such proofs is Hilbert's epsilon-substitution method. There was, however, a second approach which was not reflected in the publications of the Hilbert school in the 1920s, and which is a direct precursor of Hilbert's first epsilon theorem and a certain "general consistency result" due to Bernays. An analysis of the form of this so-called "failed proof" (...) sheds further light on an interpretation of Hilbert's programme as an instrumentalist enterprise with the aim of showing that whenever a "real" proposition can be proved by ?ideal? means, it can also be proved by "real", finitary means. (shrink)

In 1958 Gödel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type. Here we extend Gödel's T to theories Pn of “predicative” functionals, which are defined using Martin-Löf's universes of transfinite types. We then extend Gödel's interpretation to the theories of arithmetic inductive definitions IDn, so that each IDn is interpreted in the corresponding Pn. Since the strengths of the theories IDn are cofinal in the ordinal Γ0, as (...) a corollary this analysis provides an ordinal-free characterization of the <Γ0-recursive functions. (shrink)

In 1958, G¨ odel published in the journal Dialectica an interpretation of intuitionistic number theory in a quantifier-free theory of functionals of finite type; this subsequently came to be known as G¨ odel’s functional or Dialectica interpretation. The article itself was written in German for an issue of that journal in honor of Paul Bernays’ 70th birthday. In 1965, Bernays told G¨.

The metamathematical tradition, tracing back to Hilbert, employs syntactic modeling to study the methods of contemporary mathematics. A central goal has been, in particular, to explore the extent to which infinitary methods can be understood in computational or otherwise explicit terms. Ergodic theory provides rich opportunities for such analysis. Although the field has its origins in seventeenth century dynamics and nineteenth century statistical mechanics, it employs infinitary, nonconstructive, and structural methods that are characteristically modern. At the same time, computational concerns (...) and recent applications to combinatorics and number theory force us to reconsider the constructive character of the theory and its methods. This paper surveys some recent contributions to the metamathematical study of ergodic theory, focusing on the mean and pointwise ergodic theorems and the Furstenberg structure theorem for measure preserving systems. In particular, I characterize the extent to which these theorems are nonconstructive, and explain how proof-theoretic methods can be used to locate their "constructive content.". (shrink)

In the course of ten short sections, we comment on Gödel's seminal dialectica paper of fifty years ago and its aftermath. We start by suggesting that Gödel's use of functionals of finite type is yet another instance of the realistic attitude of Gödel towards mathematics, in tune with his defense of the postulation of ever increasing higher types in foundational studies. We also make some observations concerning Gödel's recasting of intuitionistic arithmetic via the dialectica interpretation, discuss the extra principles that (...) the interpretation validates and comment on extensionality and higher order equality. The latter sections focus on the role of majorizability considerations within the dialectica and related interpretations for extracting computational information from ordinary proofs in mathematics. (shrink)

Critical study of Michael Potter, Reason's Nearest Kin. Philosophies of Arithmetic from Kant to Carnap. Oxford University Press, Oxford, 2000. x + 305 pages.

William Tait's standing in the philosophy of mathematics hardly needs to be argued for; for this reason the appearance of this collection is especially welcome. As noted in his Preface, the essays in this book ‘span the years 1981–2002’. The years given are evidently those of publication. One essay was not previously published in its present form, but it is a reworking of papers published during that period. The Introduction, one appendix, and some notes are new. Many of the essays (...) will be familiar to the readers of this journal; indeed two first appeared here.It should be no surprise to those who know Tait's work that this is a very rich collection, with contributions on a wide variety of issues, both systematic and historical. That poses a problem for a reviewer, because a serious discussion of even all the major issues would be beyond the scope of a review.Before the essays in this collection, Tait's publications were almost all in mathematical logic, especially proof theory. He was a leading actor in the work on the revised Hilbert program stimulated after the war by Georg Kreisel, Kurt Schütte, and Gaisi Takeuti. Tait thus has an experience in mathematical research that is rare among those whose careers have been institutionally in philosophy. In the 1970s Tait became disillusioned with the proof-theoretic program on which he had worked. However, he draws on that background in several of these essays, and he has continued to work on mathematical questions. In particular, the set-theoretic project reflected in essay 6 is as much mathematical as philosophical.It is not easy to characterize Tait's philosophical viewpoint briefly. Both the title of the book and some of its content mark him as a rationalist. His hero in the earlier history …. (shrink)

We discuss Kunen’s algorithmic implementation of a proof for the Paris–Harrington theorem, and the author’s and da Costa’s proposed “exotic” formulation for the P = NP hypothesis. Out of those two examples we ponder the relation between mathematics within an axiomatic framework, and intuitive or informal mathematics.