Predicativity is a notable example of fruitful interaction between philosophy and mathematical logic. It originated at the beginning of the 20th century from methodological and philosophical reflections on a changing concept of set. A clarification of this notion has prompted the development of fundamental new technical instruments, from Russell's type theory to an important chapter in proof theory, which saw the decisive involvement of Kreisel, Feferman and Schütte. The technical outcomes of predica-tivity have since taken a life (...) of their own, but have also produced a deeper understanding of the notion of predicativity, therefore witnessing the " light logic throws on problems in the foundations of mathematics. " (Feferman 1998, p. vii) Predicativity has been at the center of a considerable part of Feferman's work: over the years he has explored alternative ways of explicating and analyzing this notion and has shown that predicative mathematics extends much further than expected within ordinary mathematics. The aim of this note is to outline the principal features of predicativity, from its original motivations at the start of the past century to its logical analysis in the 1950-60's. The hope is to convey why predicativity is a fascinating subject, which has attracted Feferman's attention over the years. (shrink)

On the basis of Poincaré and Weyl’s view of predicativity as invariance, we develop an extensive framework for predicative, type-free first-order set theory in which $\Gamma _0$ and much bigger ordinals can be defined as von Neumann ordinals. This refutes the accepted view of $\Gamma _0$ as the “limit of predicativity”.

Prominent constructive theories of sets as Martin-Löf type theory and Aczel and Myhill constructive set theory, feature a distinctive form of constructivity: predicativity. This may be phrased as a constructibility requirement for sets, which ought to be finitely specifiable in terms of some uncontroversial initial “objects” and simple operations over them. Predicativity emerged at the beginning of the 20th century as a fundamental component of an influential analysis of the paradoxes by Poincaré and Russell. According to this analysis (...) the paradoxes are caused by a vicious circularity in definitions; adherence to predicativity was therefore proposed as a systematic method for preventing such problematic circularity. In the following, I sketch the origins of predicativity, review the fundamental contributions by Russell and Weyl and look at modern incarnations of this notion. (shrink)

We suggest a new framework for the Weyl-Feferman predicativist program by constructing a formal predicative set theory P ZF which resembles ZF , and is suitable for mechanization. The basic idea is that the predicatively acceptable instances of the comprehension schema are those which determine the collections they define in an absolute way, independent of the extension of the “surrounding universe”. The language of P ZF is type-free, and it reflects real mathematical practice in making an extensive use of (...) statically defined abstract set terms. Another important feature of P ZF is that its underlying logic is ancestral logic (i.e. the extension of first-order logic with a transitive closure operation). (shrink)

Most axiomatizations of set theory that have been treated metamathematically have been based either entirely on classical logic or entirely on intuitionistic logic. But a natural conception of the settheoretic universe is as an indefinite (or “potential”) totality, to which intuitionistic logic is more appropriately applied, while each set is taken to be a definite (or “completed”) totality, for which classical logic is appropriate; so on that view, set theory should be axiomatized on some correspondingly mixed basis. Similarly, (...) in the case of predicative analysis, the natural numbers are considered to form a definite totality, while the universe of sets (or functions) of natural numbers are viewed as an indefinite totality, so that, again, a mixed semi-constructive logic should be the appropriate one to treat the two together. Various such semiconstructive systems of analysis and set theory are formulated here and their proof-theoretic strength is characterized. Interestingly, though the logic is weakened, one can in compensation strengthen certain principles in a way that could be advantageous for mathematical applications. (shrink)

A logic-enriched type theory is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named and , which we claim correspond closely to the classical predicative systems of second order arithmetic and . We justify this claim by translating each second order system into the corresponding LTT, and proving that these translations are conservative. This is part of an ongoing research project to investigate how LTTs may be used to formalise (...) different approaches to the foundations of mathematics.The two LTTs we construct are subsystems of the logic-enriched type theory , which is intended to formalise the classical predicative foundation presented by Herman Weyl in his monograph Das Kontinuum. The system has also been claimed to correspond to Weyl’s foundation. By casting and as LTTs, we are able to compare them with . It is a consequence of the work in this paper that is strictly stronger than .The conservativity proof makes use of a novel technique for proving one LTT conservative over another, involving defining an interpretation of the stronger system out of the expressions of the weaker. This technique should be applicable in a wide variety of different cases outside the present work. (shrink)

often insisted existence in mathematics means logical consistency, and formal logic is the sole guarantor of rigor. The paper joins this to his view of intuition and his own mathematics. It looks at predicativity and the infinite, Poincaré's early endorsement of the axiom of choice, and Cantor's set theory versus Zermelo's axioms. Poincaré discussed constructivism sympathetically only once, a few months before his death, and conspicuously avoided committing himself. We end with Poincaré on Couturat, Russell, and Hilbert.

Russell’s critique of substance monism is an ideal starting point from which to understand some main concepts in Spinoza’s difficult metaphysics. This paper provides an in-depth examination of Spinoza’s proof that only one substance exists. On this basis, it rejects Russell’s interpretation of Spinoza’s theory of reality as founded upon the logical doctrine that all propositions consist of a predicate and a subject. An alternative interpretation is offered: Spinoza’s substance is not a bearer of properties, as Russell implied, (...) but an eternally active, self-actualizing creative power. Eventually, Spinoza the Monist and Russell the Pluralist are at one in holding that process and activity rather than enduring things are the most fundamental realities. (shrink)

I. Descriptions in Predicative Position The predicative analysis and Russell’s theory part company when it comes to the argument structure assigned to sentences like (1). (1) Washington is the greatest French soldier. On a standard Russellian analysis, (1) has the following (a) logical form and (b) truth conditions.

We present well-ordering proofs for Martin-Löf's type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength of intensional and (...) extensional version, of the version à la Tarski and à la Russell are shown to be the same. (shrink)

A free logic is one in which a singular term can fail to refer to an existent object, for example, `Vulcan' or `5/0'. This essay demonstrates the fruitfulness of a version of this non-classical logic of terms (negative free logic) by showing (1) how it can be used not only to repair a looming inconsistency in Quine's theory of predication, the most influential semantical theory in contemporary philosophical logic, but also (2) how Beeson, Farmer and Feferman, among others, (...) use it to provide a natural foundation for partial functions in programming languages. Vis à vis (2), the question is raised whether the Beeson-Farmer-Feferman approach is adequate to the treatment of partial functions in all programming languages. Gumb and the author say No, and suggest a way of handling the refractory cases by means of positive free logic. Finally, Antonelli's solution of a problem associated with the Gumb-Lambert proposal is mentioned. (shrink)

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)

In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation with (...) predicativity, predicative logic still plays an influential role in Computer Science.An important example is the proof checker Nuprl, which is basedon Martin-Löf''s Type Theory which uses type universes. Those type universes,and also degrees of expressions in AUTOMATH, are closely related toorders. In this paper, we show that orders have not disappeared from modern logic and computer science, rather, orders play a crucial role in understanding the hierarchy of modern systems. In order to achieve our goal, we concentrate on a subsystem of Nuprl.The novelty of our paper lies in: (1) a modest revival of Russell's orders, (2) the placing of the historical system RTT underlying the famous Principia Mathematica in a context with a modern system of computer mathematics (Nuprl) and modern type theories (Martin-Löf''s type theory and PTSs), and (3) the presentation of acomplex type system (Nuprl) as a simple and compact PTS. (shrink)

Church’s type theory, aka simple type theory, is a formal logical language which includes classical first-order and propositional logic, but is more expressive in a practical sense. It is used, with some modifications and enhancements, in most modern applications of type theory. It is particularly well suited to the formalization of mathematics and other disciplines and to specifying and verifying hardware and software. It also plays an important role in the study of the formal semantics of natural (...) language. When utilizing it as a meta-logic to semantically embed expressive non-classical logics further topical applications are enabled in artificial intelligence and philosophy. A great wealth of technical knowledge can be expressed very naturally in it. With possible enhancements, Church’s type theory constitutes an excellent formal language for representing the knowledge in automated information systems, sophisticated automated reasoning systems, systems for verifying the correctness of mathematical proofs, and a range of projects involving logic and artificial intelligence. Some examples and further references are given in Sections 1.2.2 and 5 below. Type theories are also called higher-order logics, since they allow quantification not only over individual variables, but also over function, predicate, and even higher order variables. Type theories characteristically assign types to entities, distinguishing, for example, between numbers, sets of numbers, functions from numbers to sets of numbers, and sets of such functions. As illustrated in Section 1.2.2 below, these distinctions allow one to discuss the conceptually rich world of sets and functions without encountering the paradoxes of naive set theory. Church’s type theory is a formulation of type theory that was introduced by Alonzo Church in Church 1940. In certain respects, it is simpler and more general than the type theory introduced by Bertrand Russell in Russell 1908 and Whitehead & Russell 1927a. Since properties and relations can be regarded as functions from entities to truth values, the concept of a function is taken as primitive in Church’s type theory, and the λ-notation which Church introduced in Church 1932 and Church 1941 is incorporated into the formal language. Moreover, quantifiers and description operators are introduced in a way so that additional binding mechanisms can be avoided, λ-notation is reused instead. λ-notation is thus the only binding mechanism employed in Church’s type theory. (shrink)

Constructive set theory a' la Myhill-Aczel has been extended in (Cantini and Crosilla 2008, Cantini and Crosilla 2010) to incorporate a notion of (partial, non--extensional) operation. Constructive operational set theory is a constructive and predicative analogue of Beeson's Inuitionistic set theory with rules and of Feferman's Operational set theory (Beeson 1988, Feferman 2006, Jaeger 2007, Jaeger 2009, Jaeger 1009b). This paper is concerned with an extension of constructive operational set theory (Cantini and Crosilla 2010) by (...) a uniform operation of Transitive Closure, \tau. Given a set a, \tau produces its transitive closure \tau a. We show that the theory ESTE of (Cantini and Crosilla 2010) augmented by \tau is still conservative over Peano Arithmetic. (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)

Questions concerning the proof-theoretic strength of classical versus nonclassical theories of truth have received some attention recently. A particularly convenient case study concerns classical and nonclassical axiomatizations of fixed-point semantics. It is known that nonclassical axiomatizations in four- or three-valued logics are substantially weaker than their classical counterparts. In this paper we consider the addition of a suitable conditional to First-Degree Entailment—a logic recently studied by Hannes Leitgeb under the label HYPE. We show in particular that, by formulating the (...) theory PKF over HYPE, one obtains a theory that is sound with respect to fixed-point models, while being proof-theoretically on a par with its classical counterpart KF. Moreover, we establish that also its schematic extension—in the sense of Feferman—is as strong as the schematic extension of KF, thus matching the strength of predicative analysis. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:russell: the Journal of Bertrand Russell Studies n.s. 33 (summer 2013): 59–94 The Bertrand Russell Research Centre, McMaster U. issn 0036–01631; online 1913–8032 oeviews PRINCIPIA’S SECOND EDITION Russell Wahl English and Philosophy / Idaho State U. Pocatello, id 83209, usa wahlruss@isu.edu Bernard Linsky. The Evolution of Principia Mathematica: Bertrand Russell’s Manuscripts and Notes for the Second Edition. Cambridge: Cambridge U. P., 2011. Pp. vii, 407; 2 plates. isbn: 978-1-10700-327-9. (...) £96; us$159. ussell and Whitehead’s Principia Mathematica was a pioneering work which was in many ways overtaken by the success of the new discipline it helped found. There is little doubt that Principia Mathematica was one of the most important works in the development of symbolic logic, as even Quine, one of the critics of the foundations proposed in it, said: “This is the book that has meant the most to me.”Yet few mathematicians or logicians follow the theory of types proposed in Principia as the foundation of mathematics, nor the logicist project of which it is a variant. While much of Principia ’s notation has been incorporated into modern formal logic and set theory, much of it also is dated and not easy for contemporary mathematicians and logicians to read. Among those who were dissatisfied with the philosophical foundations of the first edition were the authors themselves.1 During 1923 and 1924 Russell revised and updated Principia, and the second edition of the first volume appeared in 1925 with the other two volumes appearing in 1927. What resulted was a new edition with the philosophical underpinning modi- fied, but with the superstructure, that is, the resulting theorems of the three volumes, unchanged. Russell wrote a new Introduction and added three Appendices, but other than that made only minor changes.The new philosophy of logic had as its core idea a principle of extensionality which Russell expressed as the view that “functions of propositions are always truth-functions and a function can only occur in a proposition through its values” (PM2 1: ______ 1 Russell wrote the new material for the second edition, but it is clear from a letter to him byWhitehead on 24 May 1923, quoted by Linsky, that he, too, thought the foundational system needed tweaking: “I don’t think that ‘types’ are quite right” (p. 16). o= 60 Reviews xiv). It is interesting that at times Russell seems to have been hesitant about even endorsing this change.2 The second edition of Principia has not been well received; by and large it has either been ignored or scorned. Linsky cites especially negative remarks by Monk, but others have dismissed the second edition additions and it has generally been thought a failure since 1944, when Gödel pointed out an error in the Appendix B proof that mathematical induction can be “rectified” even without the axiom of reducibility. The Evolution of Principia Mathematica makes available to scholars Russell’s notes and manuscripts of the new material added to the second edition. Linsky also seeks to redress the indifference to the second edition, to set the record straight about several misunderstandings, and to give an account of the new material.The book he has produced will be very valuable to scholars of Russell and to anyone interested in the development of type theory and indeed of logic as a whole during this time. This is also a difficult book, both because the material can get quite technical at times and also because the new material included in the introduction to the second edition is somewhat sketchy, and there are philosophical and technical points about which Russell himself is less than clear. As a result there have been disagreements about how the second edition is best to be interpreted. Linsky recognizes that the interpretive issues are under-determined by the text and wants to stay relatively neutral with respect to the different alternatives about the various controversies. At times it can be difficult to keep the various positions straight.The difficulty lies with the material, and Linsky does a very good job of explaining the issues to the layman. The work is divided into... (shrink)

In the early years of this century, Poincaré and Russell engaged in a debate concerning the nature of mathematical reasoning. Siding with Kant, Poincaré argued that mathematical reasoning is characteristically non-logical in character. Russell urged the contrary view, maintaining that (i) the plausibility originally enjoyed by Kant's view was due primarily to the underdeveloped state of logic in his (i.e., Kant's) time, and that (ii) with the aid of recent developments in logic, it is possible to demonstrate its falsity. This (...) refutation of Kant's views consists in showing that every known theorem of mathematics can be proven by purely logical means from a basic set of axioms. In our view, Russell's alleged refutation of Poincaré's Kantian viewpoint is mistaken. Poincaré's aim (as Kant's before him) was not to deny the possibility of finding a logical ‘proof’ for each theorem. Rather, it was to point out that such purely logical derivations fail to preserve certain of the important and distinctive features of mathematical proof. Against such a view, programs such as Russell's, whose main aim was to demonstrate the existence of a logical counterpart for each mathematical proof, can have but little force. For what is at issue is not whether each mathematical theorem can be fitted with a logical ‘proof’, but rather whether the latter has the epistemic features that a genuine mathematical proof has. (shrink)

This paper sets out a predicative response to the Russell-Myhill paradox of propositions within the framework of Church’s intensional logic. A predicative response places restrictions on the full comprehension schema, which asserts that every formula determines a higher-order entity. In addition to motivating the restriction on the comprehension schema from intuitions about the stability of reference, this paper contains a consistency proof for the predicative response to the Russell-Myhill paradox. The models used to establish this consistency also model other (...) axioms of Church’s intensional logic that have been criticized by Parsons and Klement: this, it turns out, is due to resources which also permit an interpretation of a fragment of Gallin’s intensional logic. Finally, the relation between the predicative response to the Russell-Myhill paradox of propositions and the Russell paradox of sets is discussed, and it is shown that the predicative conception of set induced by this predicative intensional logic allows one to respond to the Wehmeier problem of many non-extensions. (shrink)

In his article, “Stroll on Russell's ‘Proof’”, Robert Fahrnkopf takes issue with four comments I made about Russell's theory of descriptions in a paper, “Russell's ‘Proof,’” which appeared in the June 1975 issue of this Journal. Though I disagree with Fahrnkopf on the points in question, there would be no point in washing our private conceptual linen in a public place were it not for the ingenious and highly original suggestions he makes in his defense of Russell. (...) I think some additional discussion may be useful in carrying the current debate about the theory a step further. In what follows, I will therefore deal with each of the four points he speaks to. (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)

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)

“Small” large cardinal notions in the language of ZFC are those large cardinal notions that are consistent with V = L. Besides their original formulation in classical set theory, we have a variety of analogue notions in systems of admissible set theory, admissible recursion theory, constructive set theory, constructive type theory, explicit mathematics and recursive ordinal notations (as used in proof theory). On the face of it, it is surprising that such distinctively set-theoretical (...) notions have analogues in such disaparate and relatively constructive contexts. There must be an underlying reason why that is possible (and, incidentally, why “large” large cardinal notions have not led to comparable analogues). My long term aim is to develop a common language in which such notions can be expressed and can be interpreted both in their original classical form and in their analogue form in each of these special constructive and semi-constructive cases. This is a program in progress. What is done here, to begin with, is to show how that can be done to a considerable extent in the settings of classical and admissible set theory (and thence, admissible recursion theory). The approach taken here is to expand the language of set theory to allow us to talk about (possibly partial) operations applicable both to sets and to operations and to formulate the large cardinal notions in question in terms of operational closure conditions; at the same time only minimal existence axioms are posited for sets. The resulting system, called Operational Set Theory, is a partial adaptation to the set-theoretical framework of the explicit mathematics framework Feferman (1975). The.. (shrink)

In this paper we study proofs of some general forms of the Second Incompleteness Theorem. These forms conform to the Feferman format, where the proof predicate is fixed and the representation of the set of axioms varies. We extend the Feferman framework in one important point: we allow the interpretation of number theory to vary.

This essay considers Richard Calder’s Dead trilogy as an important contribution to the argument concerning how pornography’s pernicious effects might be mitigated or disrupted. Paying close attention to the way that Calder uses the rhetoric of fiction to challenge pornographic stereotypes that have achieved hegemonic status, the essay argues that Calder’s trilogy provides an important link between debates about pornography and contemporary philosophical discussions of alterity and community. Finally, it argues that, for Calder, sexuality is implicitly predicated on a reconceptualization (...) of social relations in general – a reconceptualization achieved through the exhaustion of that decadent shadow of the Enlightenment, pornography. (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 (...) class='Hi'>proof-theoretically equivalent to predicative analysis. (shrink)

ExcerptI then looked more closely at the picture of the child and realized to my inexpressible horror that it was a picture of me as a child. This was proof of my guilt… . I wasted no time with denials but said at once to Agathe that only two possibilities remained: either immediate flight and concealment, or suicide. She said very firmly that only the latter came into consideration. Overcome by fear and horror, I awoke.1So ends the account of (...) a dream from early July of 1942, written less than eight months after Adorno's…. (shrink)

The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. The application of this undervalued formalism has been hampered by the absence of well-behaved proof systems on the one hand, and accessible presentations of its theory on the other. One significant early result for the original axiomatic proof system for the epsilon-calculus is the first epsilon theorem, for which a proof is sketched. The system itself is discussed, also relative to possible semantic (...) interpretations. The problems facing the development of proof-theoretically well-behaved systems are outlined. (shrink)

A loose analogy relates the work of Laplace and Hilbert. These thinkers had roughly similar objectives. At a time when so much of our analytic effort goes to distinguishing mathematics and logic from physical theory, such an analogy can still be instructive, even though differences will always divide endeavors such as those of Laplace and Hilbert.

In this paper we apply proof theoretic methods used for classical systems in order to obtain upper bounds for systems in partial logic. We focus on a truth predicate interpreted in a Kripke style way via strong Kleene; whereas the aim is to connect harmoniously the partial version of Kripke–Feferman with its intended semantics. The method we apply is based on infinitary proof systems containing an ω-rule.

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)

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

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)

Machine generated contents note: -- Series Editors' PrefaceAcknowledgementsNotes on ContributorsHow Things Are Elsewhere; W. Schwarz Information Change and First-Order Dynamic Logic; B.Kooi Interpreting and Applying Proof Theories for Modal Logic; F.Poggiolesi & G.Restall The Logic(s) of Modal Knowledge; D.Cohnitz On Probabilistically Closed Languages; H.Leitgeb Dogmatism, Probability and Logical Uncertainty; B.Weatherson & D.Jehle Skepticism about Reasoning; S.Roush, K.Allen & I.HerbertLessons in Philosophy of Logic from Medieval Obligations; C.D.Novaes How to Rule Out Things with Words: Strong Paraconsistency and the Algebra of (...) Exclusion; F.Berto Lessons from the Logic of Demonstratives; G.RussellThe Multitude View on Logic; M.Eklund Index. (shrink)

The concept of the (full) unfolding of a schematic system is used to answer the following question: Which operations and predicates, and which principles concerning them, ought to be accepted if one has accepted ? The program to determine for various systems of foundational significance was previously carried out for a system of nonfinitist arithmetic, ; it was shown that is proof-theoretically equivalent to predicative analysis. In the present paper we work out the unfolding notions for a basic schematic (...) system of finitist arithmetic, , and for an extension of that by a form of the so-called Bar Rule. It is shown that and are proof-theoretically equivalent, respectively, to Primitive Recursive Arithmetic, , and to Peano Arithmetic,. (shrink)

We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the (...) West or the original presentation can be improved using notions or results which appeared later. This includes such topics as Novikov's cut-elimination method (regular formulas) and Maslov's inverse method for the predicate logic. (shrink)

Russell's philosophy is rightly described as a programme of reduction of mathematics to logic. Now the theory of geometry developed in 1903 does not fit this picture well, since it is deeply rooted in the purely synthetic projective approach, which conflicts with all the endeavours to reduce geometry to analytical geometry. The first goal of this paper is to present an overview of this conception. The second aim is more far-reaching. The fact that such a theory of geometry (...) was sustained by Russell compels us to question the meaning of logicism: how is it possible to reconcile Russell's global reductionist standpoint with his local defence of the specificities of geometry? * This paper was first presented at the conference ‘Qu'est ce que la géométrie aux époques modernes et contemporaines?’, organized by the Universität Köln and the Archives Poincaré. I would like to thank Philippe Nabonnand for having enlightened me about the issues relative to projective geometry. I would like also to thank Nicholas Griffin, Brice Halimi, Bernard Linsky, Marco Panza, Ivahn Smadja for their helpful discussions. Many thanks also to the two anonymous referees for their useful suggestions. CiteULike Connotea Del.icio.us What's this? (shrink)

Hermann's Weyl Das Kontinuum has inspired several studies in logic and foundations of mathematics over the last century. The book provides a remarkable reconstruction of a large portion of classical mathematics on a predicative basis. However, diverging interpretations of the predicative system formulated by Weyl have been proposed in the literature. In the present work, I analyze an early formalization of Weyl's ideas proposed by [Casari, E. 1964. Questioni di Filosofia Della Matematica, Milano: Feltrinelli] and compare it with other, more (...) well-known, accounts, such as those proposed respectively by Feferman and Avron. In this way, I fill a gap in the literature on Weyl's predicative mathematics by shedding light on an interpretation that has never been studied. Moreover, Casari's work is plausibly the first systematic reconstruction of Weyl's system. In particular, I highlight the different insights about predicativity that can be found in Weyl's work. Casari's reconstruction focuses on the logical and mathematical processes described by Weyl in the first part of his book. Through the analysis of this unexplored perspective, I shed light on fundamental aspects of Weyl's work and elucidate the alleged ambiguities it presents. In particular, in line with Avron's most recent reconstruction of Weyl's ideas, this analysis supports a stronger conception of predicativity than what is commonly attributed to Weyl in the literature. As a result, this work not only provides an analysis of a neglected interpretation of Das Kontinuum, but also contributes to elucidating Weyl's classical conception of predicativity. (shrink)

Hermann's Weyl Das Kontinuum has inspired several studies in logic and foundations of mathematics over the last century. The book provides a remarkable reconstruction of a large portion of classical mathematics on a predicative basis. However, diverging interpretations of the predicative system formulated by Weyl have been proposed in the literature. In the present work, I analyze an early formalization of Weyl's ideas proposed by [Casari, E. 1964. Questioni di Filosofia Della Matematica, Milano: Feltrinelli] and compare it with other, more (...) well-known, accounts, such as those proposed respectively by Feferman and Avron. In this way, I fill a gap in the literature on Weyl's predicative mathematics by shedding light on an interpretation that has never been studied. Moreover, Casari's work is plausibly the first systematic reconstruction of Weyl's system. In particular, I highlight the different insights about predicativity that can be found in Weyl's work. Casari's reconstruction focuses on the logical and mathematical processes described by Weyl in the first part of his book. Through the analysis of this unexplored perspective, I shed light on fundamental aspects of Weyl's work and elucidate the alleged ambiguities it presents. In particular, in line with Avron's most recent reconstruction of Weyl's ideas, this analysis supports a stronger conception of predicativity than what is commonly attributed to Weyl in the literature. As a result, this work not only provides an analysis of a neglected interpretation of Das Kontinuum, but also contributes to elucidating Weyl's classical conception of predicativity. (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)

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)

It would be an understatement to say that Russell was interested in Cantorian diagonal paradoxes. His discovery of the various versions of Russell’s paradox—the classes version, the predicates version, the propositional functions version—had a lasting effect on his views in philosophical logic. Similar Cantorian paradoxes regarding propositions—such as that discussed in §500 of The Principles of Mathematics—were surely among the reasons Russell eventually abandoned his ontology of propositions.1 However, Russell’s reasons for abandoning what he called “denoting concepts”, and his rejection (...) of similar “semantic dualisms” such as Frege’s theory of sense and reference—at least in “On Denoting”—made no explicit mention of any Cantorian paradox. My aim in this paper is to argue that such paradoxes do pose a problem for certain theories such as Frege’s, and early Russell’s, about how definite descriptions are meaningful. My first aim is simply to lay out the problem I have in mind. Next, I shall turn to arguing that the theories of descriptions endorsed by Frege and by Russell prior to “On Denoting” are susceptible to the problem. Finally, I explore what responses a.. (shrink)

When I was a teenager growing up in Los Angeles in the early 1940s, my dream was to become a mathematical physicist: I was fascinated by the ideas of relativity theory and quantum mechanics, and I read popular expositions which, in those days, besides Einstein’s The Meaning of Relativity, was limited to books by the likes of Arthur S. Eddington and James Jeans. I breezed through the high-school mathematics courses (calculus was not then on offer, and my teachers barely (...) understood it), but did less well in physics, which I should have taken as a reality check. On the philosophical side I read a mixed bag of Bertrand Russell, John Dewey and Alfred Korzybski (the missionary for “General Semantics” in Science and Sanity, a mish-mash of the theory of types, non-. (shrink)

Deductive Logic is an introductory textbook in formal logic. The book is divided into four parts covering (i) truth-functional logic, (ii) monadic quantifi- cation, (iii) polyadic quantification and (iv) names and identity, and there are exercises for all these topics at the end of the book. In the truth-functional logic part, the reader learns to produce paraphrases of English statements and arguments in logical notation (this subsection is called “analysis”), then about the semantic properties of such paraphrased statements and arguments, (...) such as satisfiability, implication and equivalence (“logical assessment”) and finally (“reflection”) there is an axiomatic proof method and some important extras such as disjunctive normal form and expressive adequacy. Parts two and three mirror this analysis/assessment/reflection structure for monadic and polyadic quantification, though this time the proof system is a natural deduction one, and part three contains a completeness proof for that system. The fourth part of the book introduces names, the identity predicate and descriptions and examines the additional expressive power which these provide. (shrink)