Part of the ambiguity lies in the various points of view from which this question might be considered. The crudest di erence lies between the point of view of the working mathematician and that of the logician concerned with the foundations of mathematics. Now some of my fellow mathematical logicians might protest this distinction, since they consider themselves to be just more of those \working mathematicians". Certainly, modern logic has established itself as a very respectable branch of mathematics, and there (...) are quite a few highly technical journals in logic, such as The Journal of Sym-. (shrink)
In this collection of essays written over a period of twenty years, Solomon Feferman explains advanced results in modern logic and employs them to cast light on significant problems in the foundations of mathematics. Most troubling among these is the revolutionary way in which Georg Cantor elaborated the nature of the infinite, and in doing so helped transform the face of twentieth-century mathematics. Feferman details the development of Cantorian concepts and the foundational difficulties they engendered. He argues that the freedom (...) provided by Cantorian set theory was purchased at a heavy philosophical price, namely adherence to a form of mathematical platonism that is difficult to support. -/- Beginning with a previously unpublished lecture for a general audience, Deciding the Undecidable, Feferman examines the famous list of twenty-three mathematical problems posed by David Hilbert, concentrating on three problems that have most to do with logic. Other chapters are devoted to the work and thought of Kurt Gödel, whose stunning results in the 1930s on the incompleteness of formal systems and the consistency of Cantors continuum hypothesis have been of utmost importance to all subsequent work in logic. Though Gödel has been identified as the leading defender of set-theoretical platonism, surprisingly even he at one point regarded it as unacceptable. -/- In his concluding chapters, Feferman uses tools from the special part of logic called proof theory to explain how the vast part--if not all--of scientifically applicable mathematics can be justified on the basis of purely arithmetical principles. At least to that extent, the question raised in two of the essays of the volume, Is Cantor Necessary?, is answered with a resounding no. -/- This volume of important and influential work by one of the leading figures in logic and the foundations of mathematics is essential reading for anyone interested in these subjects. (shrink)
This paper presents examples of infinite diagrams (as well as infinite limits of finite diagrams) whose use is more or less essential for understanding and accepting various proofs in higher mathematics. The significance of these is discussed with respect to the thesis that every proof can be formalized, and a "pre" form of this thesis that every proof can be presented in everyday statements-only form.
The paper starts with an examination and critique of Tarski’s wellknown proposed explication of the notion of logical operation in the type structure over a given domain of individuals as one which is invariant with respect to arbitrary permutations of the domain. The class of such operations has been characterized by McGee as exactly those definable in the language L∞,∞. Also characterized similarly is a natural generalization of Tarski’s thesis, due to Sher, in terms of bijections between domains. My main (...) objections are that on the one hand, the Tarski-Sher thesis thus assimilates logic to mathematics, and on the other hand fails to explain the notion of same logical operation across domains of different sizes. A new notion of homomorphism invariant operation over functional type structures (with domains M0 of individuals and {T, F} at their base) is introduced to accomplish the latter. The main result is that an operation is definable from.. (shrink)
This paper presents examples of infinite diagrams whose use is more or less essential for understanding and accepting various proofs in higher mathematics. The significance of these is discussed with respect to the thesis that every proof can be formalized, and a “pre” form of this thesis that every proof can be presented in everyday statements-only form.
elaboration of the last part of my Tarski Lecture, “Truth unbound”, UC Berkeley, 3 April 2006, and of the lecture, “A nicer formal theory of non-hierarchical truth”, Workshop on Mathematical Methods in Philosophy, Banff , 18-23 Feb. 2007.
This is a survey of work on set-theoretical invariance criteria for logicality. It begins with a review of the Tarski-Sher thesis in terms, first, of permutation invariance over a given domain and then of isomorphism invariance across domains, both characterized by McGee in terms of definability in the language L∞,∞. It continues with a review of critiques of the Tarski-Sher thesis, and a proposal in response to one of those critiques via homomorphism invariance. That has quite divergent characterization results depending (...) on its formulation, one in terms of FOL, the other by Bonnay in terms of L∞,∞, both without equality. From that we move on to a survey of Bonnay’s work on similarity relations between structures and his results that single out invariance with respect to potential isomorphism among all such. Turning to the critique that calls for sameness of meaning of a logical operation across domains, the paper continues with a result showing that the isomorphism invariant operations that are absolutely definable with respect to KPU−Inf are exactly those definable in full FOL; this makes use of an old theorem of Manders. The concluding section is devoted to a critical discussion of the arguments for set-theoretical criteria for logicality. (shrink)
Does science justify any part of mathematics and, if so, what part? These questions are related to the so-called indispensability arguments propounded, among others, by Quine and Putnam; moreover, both were led to accept significant portions of set theory on that basis. However, set theory rests on a strong form of Platonic realism which has been variously criticized as a foundation of mathematics and is at odds with scientific realism. Recent logical results show that it is possible to directly formalize (...) almost all, if not all, scientifically applicable mathematics in a formal system that is justified simply by Peano Arithmetic (via a proof-theoretical reduction). It is argued that this substantially vitiates the indispensability arguments. (shrink)
Geometrical and physical intuition, both untutored andcultivated, is ubiquitous in the research, teaching,and development of mathematics. A number ofmathematical ``monsters'', or pathological objects, havebeen produced which – according to somemathematicians – seriously challenge the reliability ofintuition. We examine several famous geometrical,topological and set-theoretical examples of suchmonsters in order to see to what extent, if at all,intuition is undermined in its everyday roles.
This paper is mainly concerned with proof-theoretic analysis of some second-order systems of explicit mathematics with a non-constructive minimum operator. By introducing axioms for variable types we extend our first-order theory BON to the elementary explicit type theory EET and add several forms of induction as well as axioms for μ. The principal results then state: EET plus set induction is proof-theoretically equivalent to Peano arithmetic PA <0).
Following a discussion of various forms of set-theoretical foundations of category theory and the controversial question of whether category theory does or can provide an autonomous foundation of mathematics, this article concentrates on the question whether there is a foundation for “unlimited” or “naive” category theory. The author proposed four criteria for such some years ago. The article describes how much had previously been accomplished on one approach to meeting those criteria, then takes care of one important obstacle that had (...) been met in that approach, and finally explains what remains to be done if one is to have a fully satisfactory solution. (shrink)
From 1931 until late in his life (at least 1970) Godel called for the pursuit of new axioms for mathematics to settle both undecided number-theoretical propositions (of the form obtained in his incompleteness results) and undecided set-theoretical propositions (in particular CH). As to the nature of these, Godel made a variety of suggestions, but most frequently he emphasized the route of introducing ever higher axioms of in nity. In particular, he speculated (in his 1946 Princeton remarks) that there might be (...) a uniform (though non-decidable) rationale for the choice of the latter. Despite the intense exploration of the \higher in nite" in the last 30-odd years, no single rationale of that character has emerged. Moreover, CH still remains undecided by such axioms, though they have been demonstrated to have many other interesting set-theoretical consequences. (shrink)
Feferman, S. and G. Jäger, Systems of explicit mathematics with non-constructive μ-operator. Part I, Annals of Pure and Applied Logic 65 243-263. This paper is mainly concerned with the proof-theoretic analysis of systems of explicit mathematics with a non-constructive minimum operator. We start off from a basic theory BON of operators and numbers and add some principles of set and formula induction on the natural numbers as well as axioms for μ. The principal results then state: BON plus set induction (...) is proof-theoretically equivalent to Peano arithmetic PA; BON plus formula induction is proof-theoretically equivalent to the system <0 of second-order arithmetic. (shrink)
What is predicativity? While the term suggests that there is a single idea involved, what the history will show is that there are a number of ideas of predicativity which may lead to different logical analyses, and I shall uncover these only gradually. A central question will then be what, if anything, unifies them. Though early discussions are often muddy on the concepts and their employment, in a number of important respects they set the stage for the further developments, and (...) so I shall give them special attention. NB. Ahistorically, modern logical and set-theoretical notation will be used throughout, as long as it does not conflict with original intentions. (shrink)
The unfolding of schematic formal systems is a novel concept which was initiated in Feferman , Gödel ’96, Lecture Notes in Logic, Springer, Berlin, 1996, pp. 3–22). This paper is mainly concerned with the proof-theoretic analysis of various unfolding systems for non-finitist arithmetic . In particular, we examine two restricted unfoldings and , as well as a full unfolding, . The principal results then state: is equivalent to ; is equivalent to ; is equivalent to . Thus is proof-theoretically equivalent (...) to predicative analysis. (shrink)
Questions of definedness are ubiquitous in mathematics. Informally, these involve reasoning about expressions which may or may not have a value. This paper surveys work on logics in which such reasoning can be carried out directly, especially in computational contexts. It begins with a general logic of partial terms, continues with partial combinatory and lambda calculi, and concludes with an expressively rich theory of partial functions and polymorphic types, where termination of functional programs can be established in a natural way.
✤ It is the characterization of those forms of reasoning that lead invariably from true sentences to true sentences, independently of the subject matter.
Ambiguity is a property of syntactic expressions which is ubiquitous in all informal languages–natural, scientific and mathematical; the efficient use of language depends to an exceptional extent on this feature. Disambiguation is the process of separating out the possible meanings of ambiguous expressions. Ambiguity is typical if the process of disambiguation can be carried out in some systematic way. Russell made use of typical ambiguity in the theory of types in order to combine the assurance of its (apparent) consistency (“having (...) the cake”) with the freedom of the informal untyped theory of classes and relations (“eating it too”). The paper begins with a brief tour of Russell’s uses of typical ambiguity, including his treatment of the statement Cls ∈ Cls. This is generalized to a treatment in simple type theory of statements of the form A ∈ B where A and B are class expressions for which A is prima facie of the same or higher type than B. In order to treat mathematically more interesting statements of self membership we then formulate a version of typical ambiguity for such statements in an extension of Zermelo-Fraenkel set theory. Specific attention is given to how the“naive” theory of categories can thereby be accounted for. (shrink)
A notion of finitary inductively presented (f.i.p.) logic is proposed here, which includes all syntactically described logics (formal systems)met in practice. A f.i.p. theory FS0 is set up which is universal for all f.i.p. logics; though formulated as a theory of functions and classes of expressions, FS0 is a conservative extension of PRA. The aims of this work are (i)conceptual, (ii)pedagogical and (iii)practical. The system FS0 serves under (i)and (ii)as a theoretical framework for the formalization of metamathematics. The general approach (...) may be used under (iii)for the computer implementation of logics. In all cases, the work aims to make the details manageable in a natural and direct way. (shrink)
2. Various philosophical and semantical theories are candidates for axiomatization (but not all, e.g. coherence, pragmatic, fuzzy theories). NB: axiomatizations are not uniquely determined.
The goals of reduction andreductionism in the natural sciences are mainly explanatoryin character, while those inmathematics are primarily foundational.In contrast to global reductionistprograms which aim to reduce all ofmathematics to one supposedly ``universal'' system or foundational scheme, reductive proof theory pursues local reductions of one formal system to another which is more justified in some sense. In this direction, two specific rationales have been proposed as aims for reductive proof theory, the constructive consistency-proof rationale and the foundational reduction rationale. However, (...) recent advances in proof theory force one to consider the viability of these rationales. Despite the genuine problems of foundational significance raised by that work, the paper concludes with a defense of reductive proof theory at a minimum as one of the principal means to lay out what rests on what in mathematics. In an extensive appendix to the paper,various reduction relations betweensystems are explained and compared, and arguments against proof-theoretic reduction as a ``good'' reducibilityrelation are taken up and rebutted. (shrink)
I had the pleasure of renewing my acquaintance with Per Lindström at the meeting of the Seventh Scandinavian Logic Symposium, held in Uppsala in August 1996. There at lunch one day, Per said he had long been curious about the development of some of the ideas in my paper [1960] on the arithmetization of metamathematics. In particular, I had used the construction of a non-standard definition !* of the set of axioms of P (Peano Arithmetic) to show that P + (...) {¬ Con!} is interpretable in P, where ! is a standard definition of the axioms of P and Con! expresses the consistency of P via that presentation. Per pointed out that there is a simple “two-line” proof of this interpretability result which does not require the use of such formulas as !*, and he wondered whether I had been aware of that. In fact, his proof had never occurred to me, and if it had at the time, it is possible I would never have been led to the use of non-natural definitions. Per regarded this as a happy accident, since subsequent work by him and others on interpretability made essential use of such definitions. In our conversation, I enlarged a bit on the background to my work on arithmetization, and when I was invited to contribute to this special issue of Theoria dedicated to Lindström, it seemed a natural choice to use the occasion to fill out the story. One caveat, though: the following is drawn largely from memory, not always reliable, supplemented by consultation of the 1960 paper and the 1957 dissertation from which it was drawn. (shrink)
The determinism-free will debate is perhaps as old as philosophy itself and has been engaged in from a great variety of points of view including those of scientific, theological, and logical character. This chapter focuses on two arguments from logic. First, there is an argument in support of determinism that dates back to Aristotle, if not farther. It rests on acceptance of the Law of Excluded Middle, according to which every proposition is either true or false, no matter whether the (...) proposition is about the past, present or future. In particular, the argument goes, whatever one does or does not do in the future is determined in the present by the truth or falsity of the corresponding proposition. The second argument coming from logic is much more modern and appeals to Gödel's incompleteness theorems to make the case against determinism and in favour of free will, insofar as that applies to the mathematical potentialities of human beings. The claim more precisely is that as a consequence of the incompleteness theorems, those potentialities cannot be exactly circumscribed by the output of any computing machine even allowing unlimited time and space for its work. The chapter concludes with some new considerations that may be in favour of a partial mechanist account of the mathematical mind. (shrink)
The purpose of this article is to explain why I believe that the Continuum Hypothesis (CH) is not a definite mathematical problem. My reason for that is that the concept of arbitrary set essential to its formulation is vague or underdetermined and there is no way to sharpen it without violating what it is supposed to be about. In addition, there is considerable circumstantial evidence to support the view that CH is not definite.
This is a sequel to our article “Predicative foundations of arithmetic” (1995), referred to in the following as [PFA]; here we review and clarify what was accomplished in [PFA], present some improvements and extensions, and respond to several challenges. The classic challenge to a program of the sort exemplified by [PFA] was issued by Charles Parsons in a 1983 paper, subsequently revised and expanded as Parsons (1992). Another critique is due to Daniel Isaacson (1987). Most recently, Alexander George and Daniel (...) Velleman (1996) have examined [PFA] closely in the context of a general discussion of different philosophical approaches to the foundations of arithmetic. (shrink)
This is a survey of Gödel's perennial preoccupations with the limits of finitism, its relations to constructivity, and the significance of his incompleteness theorems for Hilbert's program, using his published and unpublished articles and lectures as well as the correspondence between Bernays and Gödel on these matters. There is also an important subtext, namely the shadow of Hilbert that loomed over Gödel from the beginning to the end.
I want to tell you something about the personal and scientific relationship between Alfred Tarski and Kurt Gödel, more or less chronologically. This is part of a work in progress with Anita Feferman on a biography of Alfred Tarski, and in line with most of the things we do, we’ve talked a great deal about the subject together.
Both the constructive and predicative approaches to mathematics arose during the period of what was felt to be a foundational crisis in the early part of this century. Each critiqued an essential logical aspect of classical mathematics, namely concerning the unrestricted use of the law of excluded middle on the one hand, and of apparently circular \impredicative" de nitions on the other. But the positive redevelopment of mathematics along constructive, resp. predicative grounds did not emerge as really viable alternatives to (...) classical, set-theoretically based mathematics until the 1960s. Now we have a massive amount of information, to which this lecture will constitute an introduction, about what can be done by what means, and about the theoretical interrelationships between various formal systems for constructive, predicative and classical analysis. (shrink)
