Hilbert’s program was an ambitious and wide-ranging project in the philosophy and foundations of mathematics. In order to “dispose of the foundational questions in mathematics once and for all,” Hilbert proposed a two-pronged approach in 1921: first, classical mathematics should be formalized in axiomatic systems; second, using only restricted, “finitary” means, one should give proofs of the consistency of these axiomatic systems. Although Gödel’s incompleteness theorems show that the program as originally conceived cannot be carried out, it had many partial (...) successes, and generated important advances in logical theory and metatheory, both at the time and since. The article discusses the historical background and development of Hilbert’s program, its philosophical underpinnings and consequences, and its subsequent development and influences since the 1930s. (shrink)

Elementary Recursive Nonstandard Analysis, in short ERNA, is a constructive system of nonstandard analysis with a PRA consistency proof, proposed in around 1995 by Patrick Suppes and Richard Sommer. It is based on an earlier system developed by Rolando Chuaqui and Patrick Suppes. Here, we discuss the inherent problems and limitations of the classical nonstandard framework and propose a much-needed refinement of ERNA, called , in the spirit of Karel Hrbacek’s stratified set theory. We study the metamathematics of and its (...) extensions. In particular, we consider several transfer principles, both classical and ‘stratified’, which turn out to be related. Finally, we show that the resulting theory allows for a truly general, elegant and elementary treatment of basic analysis. (shrink)

This paper addresses the question whether the past couple of decades of formal research in belief revision offers evidence of a new psychologism in logic. In the first part I examine five potential arguments in favour of this thesis and find them all wanting. In the second part of the paper I argue that belief revision research has climbed up a hierarchy of models for the change of doxastic states that appear to be clearly normative at the bottom, but are (...) more amenable to an empirical-descriptive interpretation on higher levels. I conclude that this observation might offer a foothold for the thesis that there is a new psychologism in logic. (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.

The infinite regress of Carroll’s ‘What the Tortoise said to Achilles’ is interpreted as a problem in the epistemology of mathematical proof. An approach to the problem that is both diagrammatic and non-logical is presented with respect to a specific inference of elementary geometry.

This paper critically examines two arguments against the generic multiverse, both of which are due to W. Hugh Woodin. Versions of the first argument have appeared a number of times in print, while the second argument is relatively novel. We shall investigate these arguments through the lens of two different attitudes one may take toward the methodology and metaphysics of set theory; and we shall observe that the impact of these arguments depends significantly on which of these attitudes is upheld. (...) Our examination of the second argument involves the development of a new model for Steel’s multiverse theory, which is delivered in the Appendix. (shrink)

This paper explores the set theoretic assumptions used in the current published proof of Fermat's Last Theorem, how these assumptions figure in the methods Wiles uses, and the currently known prospects for a proof using weaker assumptions.

We study Fermat's last theorem and Catalan's conjecture in the context of weak arithmetics with exponentiation. We deal with expansions of models of arithmetical theories (in the language ) by a binary (partial or total) function e intended as an exponential. We provide a general construction of such expansions and prove that it is universal for the class of all exponentials e which satisfy a certain natural set of axioms. We construct a model and a substructure with e total and (...) (Presburger arithmetic) such that in both and Fermat's last theorem for e is violated by cofinally many exponents n and (in all coordinates) cofinally many pairwise linearly independent triples. On the other hand, under the assumption of ABC conjecture (in the standard model), we show that Catalan's conjecture for e is provable in (even in a weaker theory) and thus holds in and. Finally, we also show that Fermat's last theorem for e is provable (again, under the assumption of ABC in ) in “coprimality for e”. (shrink)

I offer a critical analysis of a contemporary work in analytic philosophy applied to epistemology of logic and mathematics. I discuss the reach and limits of Paolo Mancosu’s work, as recently published in a French translation.

Dans cet article, je compare les vues de Lautman et Herbrand sur la théorie des nombres et la philosophie de l’arithmétique. Je montre que, bien que Lautman eût avoué avoir été marqué par l’influence de Herbrand, les postures fondationnelles des deux amis divergent considérablement. Alors que Lautman versait dans un réalisme platonicien, Herbrand est resté fidèle au finitisme hilbertien. Il est vrai que Lautman était philosophe et que Herbrand était avant tout arithméticien et logicien, mais il demeure que l’oeuvre de (...) Herbrand a une portée philosophique mieux accordée à la logique et aux mathématiques contemporaines.In this paper, I am contrasting Lautman’s and Herbrand’s views on number theory and philosophy of arithmetic. It is argued that despite the fact that Lautman had acknowledged Herbrand’s major influence on his own work, their foundational stances diverge profoundly. Lautman defended a variety of Platonism and Herbrand advocated a personal version of Hilbertian finitism. Of course, Lautman was a philosopher while Herbrand dealt mainly with number theory and logic. It remains though that Herbrand’s work is more in tune with contemporary logic and mathematics from a philosophical perspective. (shrink)

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)

Of all the demands that mathematics imposes on its practitioners, one of the most fundamental is that proofs ought to be correct. It has been common since the turn of the twentieth century to take correctness to be underwritten by the existence of formal derivations in a suitable axiomatic foundation, but then it is hard to see how this normative standard can be met, given the differences between informal proofs and formal derivations, and given the inherent fragility and complexity of (...) the latter. This essay describes some of the ways that mathematical practice makes it possible to reliably and robustly meet the formal standard, preserving the standard normative account while doing justice to epistemically important features of informal mathematical justification. (shrink)

A variety of projects in proof theory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.

At the turn of the nineteenth century, mathematics exhibited a style of argumentation that was more explicitly computational than is common today. Over the course of the century, the introduction of abstract algebraic methods helped unify developments in analysis, number theory, geometry, and the theory of equations; and work by mathematicians like Dedekind, Cantor, and Hilbert towards the end of the century introduced set-theoretic language and infinitary methods that served to downplay or suppress computational content. This shift in emphasis away (...) from calculation gave rise to concerns as to whether such methods were meaningful, or appropriate to mathematics. The discovery of paradoxes stemming from overly naive use of set-theoretic language and methods led to even more pressing concerns as to whether the modern methods were even consistent. This led to heated debates in the early twentieth century and what is sometimes called the “crisis of foundations.” In lectures presented in 1922, David Hilbert launched his Beweistheorie, or Proof Theory, which aimed to justify the use of modern methods and settle the problem of foundations once and for all. This, Hilbert argued, could be achieved as follows. (shrink)

The philosophy of mathematics has long been concerned with deter- mining the means that are appropriate for justifying claims of mathemat- ical knowledge, and the metaphysical considerations that render them so. But, as of late, many philosophers have called attention to the fact that a much broader range of normative judgments arise in ordinary math- ematical practice; for example, questions can be interesting, theorems important, proofs explanatory, concepts powerful, and so on. The as- sociated values are often loosely classied as (...) aspects of \mathematical understanding." Meanwhile, in a branch of computer science known as \formal ver- ication," the practice of interactive theorem proving has given rise to software tools and systems designed to support the development of com- plex formal axiomatic proofs. Such eorts require one to develop models of mathematical language and inference that are more robust than the the simple foundational models of the last century. This essay explores some of the insights that emerge from this work, and some of the ways that these insights can inform, and be informed by, philosophical theories of mathematical understanding. (shrink)