This is a critical analysis of the first part of Go¨del’s 1951 Gibbs lecture on certain philosophical consequences of the incompleteness theorems. Go¨del’s discussion is framed in terms of a distinction between objective mathematics and subjective mathematics, according to which the former consists of the truths of mathematics in an absolute sense, and the latter consists of all humanly demonstrable truths. The question is whether these coincide; if they do, no formal axiomatic system (or Turing machine) can comprehend the mathematizing (...) potentialities of human thought, and, if not, there are absolutely unsolvable mathematical problems of diophantine form. (shrink)

In [10] Friedman showed that is a conservative extension of <ε0for-sentences wherei= min, i.e.,i= 2, 3, 4 forn= 0, 1, 2 +m. Feferman [5], [7] and Tait [11], [12] reobtained this result forn= 0, 1 and even with instead of. Feferman and Sieg established in [9] the conservativeness of over <ε0for-sentences for alln. In each paper, different methods of proof have been used. In particular, Feferman and Sieg showed how to apply familiar proof-theoretical techniques by passing through (...) languages with Skolem functionals.In this paper we study the same choice principles in the presence of theBar Rule, which permits one to infer the scheme of transfinite induction on a primitive recursive relation ≺ when it has been proved that ≺ is wellfounded. The main result characterizes + as a conservative extension of a system of the autonomously iterated-comprehension axiom for-sentences. Forn= 0 this has been proved by Feferman in the form that + is a conservative extension of <Γ0; this was first done in [8] by use of the Gödel functional interpretation for the stronger systemZω+μ+ + and then more recently by the simpler methods of [9]. Jäger showed how the latter methods could also be used to obtain the general result of Theorem 1 below. (shrink)

In his book Shadows of the Mind: A search for the missing science of con- sciousness [SM below], Roger Penrose has turned in another bravura perfor- mance, the kind we have come to expect ever since The Emperor’s New Mind [ENM ] appeared. In the service of advancing his deep convictions and daring conjectures about the nature of human thought and consciousness, Penrose has once more drawn a wide swath through such topics as logic, computa- tion, artificial intelligence, quantum physics (...) and the neuro-physiology of the brain, and has produced along the way many gems of exposition of difficult mathematical and scientific ideas, without condescension, yet which should be broadly appealing. 1 While the aims and a number of the topics in SM are the same as in ENM, the focus now is much more on the two axes that Pen- rose grinds in earnest. Namely, in the first part of SM he argues anew and at great length against computational models of the mind and more specifi- cally against any account of mathematical thought in computational terms. Then in the second part, he argues that there must be a scientific account of consciousness but that will require a (still to be found) non-computational extension or modification of present-day quantum physics. (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)

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)

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)

Kurt Gödel (1906-1978) did groundbreaking work that transformed logic and other important aspects of our understanding of mathematics, especially his proof of the incompleteness of formalized arithmetic. This book on different aspects of his work and on subjects in which his ideas have contemporary resonance includes papers from a May 2006 symposium celebrating Gödel's centennial as well as papers from a 2004 symposium. Proof theory, set theory, philosophy of mathematics, and the editing of Gödel's writings are among the topics covered. (...) Several chapters discuss his intellectual development and his relation to predecessors and contemporaries such as Hilbert, Carnap, and Herbrand. Others consider his views on justification in set theory in light of more recent work and contemporary echoes of his incompleteness theorems and the concept of constructible set"--Provided by publisher. (shrink)

In the sole extended break from his life and varing in this way we can associate a sysied career in England, Alan Turing spent the tem of logic with any constructive ordinal. It may be asked whether such a years 1936–1938 doing graduate work at..

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)

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)

Tarski's general conception of logic placed it at the center of all rational thought, and he took its aim to be the creation of a unified conceptual apparatus. In pursuit of this conviction, from his base at the University of California in Berkeley in the post-war years he campaigned vigorously on behalf of logic, locally, nationally and internationally. Though Tarski was ecumenical in his efforts to establish the importance of logic in these various ways, in his own work—even that part (...) of it which is considered to be philosophically significant—he was first and foremost a mathematician, and, even more so, a set-theoretical one. The paper traces this particular conception of logic back to the influence of his teachers in set theory and topology in Warsaw, and then details how it affected his explication of the notions of satisfaction, truth, logical consequence and logical term. (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.

Though deceptively simple and plausible on the face of it, Craig's interpolation theorem (published 50 years ago) has proved to be a central logical property that has been used to reveal a deep harmony between the syntax and semantics of first order logic. Craig's theorem was generalized soon after by Lyndon, with application to the characterization of first order properties preserved under homomorphism. After retracing the early history, this article is mainly devoted to a survey of subsequent generalizations and applications, (...) especially of many-sorted interpolation theorems. Attention is also paid to methodological considerations, since the Craig theorem and its generalizations were initially obtained by proof-theoretic arguments while most of the applications are model-theoretic in nature. The article concludes with the role of the interpolation property in the quest for "reasonable" logics extending first-order logic within the framework of abstract model theory. (shrink)

Though deceptively simple and plausible on the face of it, Craig's interpolation theorem has proved to be a central logical property that has been used to reveal a deep harmony between the syntax and semantics of first order logic. Craig's theorem was generalized soon after by Lyndon, with application to the characterization of first order properties preserved under homomorphism. After retracing the early history, this article is mainly devoted to a survey of subsequent generalizations and applications, especially of many-sorted interpolation (...) theorems. Attention is also paid to methodological considerations, since the Craig theorem and its generalizations were initially obtained by proof-theoretic arguments while most of the applications are model-theoretic in nature. The article concludes with the role of the interpolation property in the quest for "reasonable" logics extending first-order logic within the framework of abstract model theory. (shrink)

Alfred Tarski’s influence on computer science was indirect but significant in a number of directions and was in certain respects fundamental. Here surveyed is Tarski’s work on the decision procedure for algebra and geometry, the method of elimination of quantifiers, the semantics of formal languages, model-theoretic preservation theorems, and algebraic logic; various connections of each with computer science are taken up.

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)

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¨.

1. One theory or many? In 2004 a very interesting and readable article by Lenore Blum, entitled “Computing over the reals: Where Turing meets Newton,” appeared in the Notices of the American Mathematical Society. It explained a basic model of computation over the reals due to Blum, Michael Shub and Steve Smale (1989), subsequently exposited at length in their influential book, Complexity and Real Computation (1997), coauthored with Felipe Cucker. The ‘Turing’ in the title of Blum’s article refers of course (...) to Alan Turing, famous for his explication of the notion of mechanical computation on discrete data such as the integers. The ‘Newton’ there has to do to with the well known numerical method due to Isaac Newton for approximating the zeros of continuous functions under suitable conditions that is taken to be a paradigm of scientific computing. Finally, the meaning of “Turing meets Newton” in the title of Blum’s article has another, more particular aspect: in connection with the problem of controlling errors in the numerical solution of linear equations and inversion of matrices,Turing (1948) defined a notion of condition for the relation of changes in the output of a computation due to small changes in the input that is analogous to Newton’s definition of the derivative. The thrust of Blum’s 2004 article was that the BSS model of computation on the reals is the appropriate foundation for scientific computing in general. By way of response, two years later another very interesting and equally readable article appeared in the Notices, this time by Mark Braverman and Stephen Cook (2006) entitled “Computing over the reals: Foundations for scientific computing,” in which the authors argued that the requisite foundation is provided by a quite different “bit computation” model, that is in fact prima facie incompatible with the BSS model. The bit computation model goes back to ideas due to Stefan Banach and Stanislaw Mazur in the latter part of the 1930s, but the first publication was not made until Mazur (1963).. (shrink)

What Gödel accomplished in the decade of the 1930s before joining the Institute changed the face of mathematical logic and continues to influence its development. As you gather from my title, I’ll be talking about the most famous of his results in that period, but first I want to indulge in some personal reminiscences. In many ways this is a sentimental journey for me. I was a member of the Institute in 1959-60, a couple of years after receiving my PhD (...) at the University of California in Berkeley, where I had worked with Alfred Tarski, another great logician. The subject of my dissertation was directly concerned with the method of arithmetization that Gödel had used to prove his theorems, and my main concern after that was to study systematic ways of overcoming incompleteness. Mathematical logic was going through a period of prodigious development in the 1950s and 1960s, and Berkeley and Princeton were two meccas for researchers in that field. For me, the prospect of meeting with Gödel and drawing on him for guidance and inspiration was particularly exciting. I didn’t know at the time what it took to get invited. Hassler Whitney commented for an obituary notice in 1978 that “it was hard to appoint a new member in logic at the Institute because Gödel could not prove to himself that a number of candidates shouldn’t be members, with the evidence at hand.” That makes it sound like the problem for Gödel was deciding who not to invite. Anyhow, I ended up being one of the lucky few. (shrink)

The background to the development of proof theory since 1960 is contained in the article (MATHEMATICS, FOUNDATIONS OF), Vol. 5, pp. 208- 209. Brie y, Hilbert's program (H.P.), inaugurated in the 1920s, aimed to secure the foundations of mathematics by giving nitary consistency proofs of formal systems such as for number theory, analysis and set theory, in which informal mathematics can be represented directly. These systems are based on classical logic and implicitly or explicitly depend on the assumption of \completed (...) in nite" totalities. Consistency of a system S (containing a modicum of elementary number theory) is su cient to ensure that any nitary meaningful statement about the natural numbers which is provable in S is correct under the intended interpretation. Thus, in Hilbert's view, consistency of S would serve to eliminate the \completed in nite" in favor of the \potential in nite" and thus secure the body of mathematics represented in S. Hilbert established the subject of proof theory as a technical part of mathematical logic by means of which his program was to be carried out its methods will be described below. In 1931, Godel's second incompleteness theorem raised a prima facieobstacle to H.P. for the system Z of elementary number theory (also called Peano Arithmetic, and denoted below by PA) since all previously recognized forms of nitary reasoning could be formalized within it. In any case, Hilbert's program could not possibly succeed for any system such as set theory in which all nitary notions and reasoning could unquestionably be formalized. These obstacles led workers in proof theory to modify H.P. in two kinds of ways. The rst was to seek reductions of various formal systems S to more constructive systems S 0. The second was to shift the aims from foundational ones to more mathematical ones. Examples of 1 the former move are the reductions of PA to intuitionistic arithmetic HA, and Gentzen's consistency proof of PA by nitary reasoning coupled with quanti er-free trans nite induction up to the ordinal , TI( 0), both obtained in the 1930s (cf.. (shrink)

• Definite totalities are set-like. If definite totalities are sets then the totality of all sets is indefinite (Russell).

This is a critical reexamination of several pieces in van Heijenoort’s Selected Essays that are directly or indirectly concerned with the philosophy of logic or the relation of logic to natural language. Among the topics discussed are absolutism and relativism in logic, mass terms, the idea of a rational dictionary, and sense and identity of sense in Frege.

Four requirements are suggested for an axiomatic system S to provide the foundations of category theory: (R1) S should allow us to construct the category of all structures of a given kind (without restriction), such as the category of all groups and the category of all categories; (R2) It should also allow us to construct the category of all functors between any two given categories including the ones constructed under (R1); (R3) In addition, S should allow us to establish the (...) existence of the usual basic mathematical structures and carry out the usual set-theoretical operations; and (R4) S should be shown to be consistent relative to currently accepted systems of set theory. This paper explains how all but parts of (R3) can be met using a system S extending NFU enriched by a stratified pairing operation; to meet more of (R3) a stronger system S∗ is introduced, but there are still some real obstacles to meeting this requirement in full. For (R4) it is sketched how both S and S∗ are shown to be consistent. (shrink)

In his 1918 monograph \Das Kontinuum", Hermann Weyl initiated a program for the arithmetical foundations of mathematics. In the years following, this was overshadowed by the foundational schemes of Hilbert's nitary consistency program and Brouwer's intuitionistic redevelopment of mathematics. In fact, not long after his own venture, Weyl became a convert to Brouwerian intuitionism and criticized his old teacher's program. Over the years, though, he became more and more pessimistic about the practical possibilities of reworking mathematics along intuitionistic lines, and (...) pointed to the value of his own early foundational e orts. Weyl 's work in Das Kontinuum has come to be recognized for its importance as the opening chapter in the actual development of predicative mathematics, whose extent has been plumbed both mathematically and logically since the 1960s. (shrink)

In the year 1900, the German mathematician David Hilbert gave a dramatic address in Paris, at the meeting of the 2nd International Congress of Mathematicians—an address which was to have lasting fame and importance. Hilbert was at that point a rapidly rising star, if not superstar, in mathematics, and before long he was to be ranked with Henri Poincar´.

The final two volumes, numbers IV and V, of the Oxford University Press edition of the Collected Works of Kurt Gödel [3]-[7] appeared in 2003, thus completing a project that started over twenty years earlier. What I mainly want to do here is trace, from the vantage point of my personal involvement, the at some times halting and at other times intense development of the Gödel editorial project from the first initiatives following Gödel’s death in 1978 to its completion last (...) year. It may be useful to scholars mounting similar editorial projects for other significant figures in our field to learn how and why various decisions were made and how the work was carried out, though of course much is particular to who and what we were dealing with. My hope here is also to give the reader who is not already familiar with the Gödel Works a sense of what has been gained in the process, and to encourage dipping in according to interest. Given the absolute importance of Gödel for mathematical logic, students should also be pointed to these important source materials to experience first hand the exercise of his genius and the varied ways of his thought and to see how scholarly and critical studies help to expand their significance. Though indeed much has been gained in our work there is still much that can and should be done; besides some indications below, for that the reader is referred to [2]. (shrink)

1. Two kinds of logic. To a first approximation there are two main kinds of pursuit in logic. The first is the traditional one going back two millennia, concerned with characterizing the logically valid inferences. The second is the one that emerged most systematically only in the twentieth century, concerned with the semantics of logical operations. In the view of modern, model-theoretical eyes, the first requires the second, but not vice-versa. According to Tarski’s generally accepted account of logical consequence, inference (...) from some statements as hypotheses to a statement as conclusion is logically valid if the truth of the hypotheses ensures the truth of the conclusion, in a way that depends only on the form of the statements involved, not on their content. Interpreted model-theoretically this means that every model of the hypotheses is a model of the conclusion. However, there is an ambiguity in Tarski’s explication, as he himself emphasized, since for the specification of form one needs to determine what are the logical notions. Once those are isolated and their semantical roles are settled, one can see how the truth of a statement is composed from the truth of its basic parts, in whatever way those are specified. The problem of what are the logical notions is an unsettled and controversial one. In the classical truthfunctional perspective, proposals range from those of first-order logic to generalized quantifiers to second and higher-order quantifiers to infinitary languages and beyond. Many of these stronger semantical notions have been treated in the volume Model Theoretic Logics. In a series of singular, thought-provoking publications in recent years, Jaakko Hintikka has vigorously promoted consideration of an extension of first-order logic called IF logic, along with claims that its adoption promises to have revolutionary consequences. (shrink)