This paper uses an atomistic ontology of universals, individuals, and facts to provide a semantics for ramified type theory. It is shown that with some natural constraints on the sort of universals and facts admitted into a model, the axiom of reducibility is made valid.

It is well known that Russell abandoned his multiple-relation theory of judgment, which provided the philosophical foundations for _PM_'s ramified type-theory, in response to criticisms by Wittgenstein. Their exact nature has remained obscure. An influential interpretation, put forth by Sommerville and Griffin, is that Wittgenstein showed that the theory must appeal to the very hierarchy it is intended to generate and thus collapses into circularity. I argue that this rests on a mistaken interpretation of (...) class='Hi'>type-theory and suggest an alternative one to explain Russell's reaction. (shrink)

In this article we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell’s reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this (...) purpose. One may regard the results of this article as an alternative solution to the problem of the proliferation of levels of real numbers in Russell’s theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here also suggests that there is a natural associated notion of predicative elementary topos. (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)

In this paper I examine the nature of Russell's ramified type theory resolution of paradoxes. In particular, I consider the effect of construing the types in Church's cumulative sense, that is, the range of a variable of a given type includes the range of every variable of directly lower type. Contrary to what seems to be generally assumed, I show that the decision to make the levels cumulative and allow this to be reflected in the (...) semantics is not neutral with respect to the solution of the paradoxes. I introduce a distinction between syntactical and semantical cumulativeness. It turns out that noncumulative type theories (in either sense) are equally capable of dealing with the paradoxes. Furthermore, whether cumulativeness is appropriate appears to be context dependent. (shrink)

Higher-order logic, with its type-theoretic apparatus known as the simple theory of types (STT), has increasingly come to be employed in theorizing about properties, relations, and states of affairs—or ‘intensional entities’ for short. This paper argues against this employment of STT and offers an alternative: ordinal type theory (OTT). Very roughly, STT and OTT can be regarded as complementary simplifications of the ‘ramified theory of types’ outlined in the Introduction to Principia Mathematica (on a (...) realist reading). While STT, understood as a theory of intensional entities, retains the Fregean division of properties and relations into a multiplicity of categories according to their adicities and ‘input types’ and discards the division of intensional entities into different ‘orders’, OTT takes the opposite approach: it retains the hierarchy of orders (though with some modifications) and discards the categorisation of properties and relations according to their adicities and input types. In contrast to STT, this latter approach avoids intensional counterparts of the Epimenides and related paradoxes. Fundamental intensional entities lie at the base of the proposed hierarchy and are also given a prominent part to play in the individuation of non-fundamental intensional entities. (shrink)

This paper considers two reasons that might support Russell’s choice of a ramified-type theory over a simple-type theory. The first reason is the existence of purported paradoxes that can be formulated in any simple-type language, including an argument that Russell considered in 1903. These arguments depend on certain converse-compositional principles. When we take account of Russell’s doctrine that a propositional function is not a constituent of its values, these principles turn out to be too (...) implausible to make these arguments troubling. The second reason is conditional on a substitutional interpretation of quantification over types other than that of individuals. This reason stands up to investigation: a simple-type language will not sustain such an interpretation, but a ramified-type language will. And there is evidence that Russell was tacitly inclined towards such an interpretation. A strong construal of that interpretation opens a way to make sense of Russell’s simultaneous repudiation of propositions and his willingness to quantify over them. But that way runs into trouble with Russell’s commitment to the finitude of human understanding. (shrink)

The paradox of propositions, presented in Appendix B of Russell's The Principles of Mathematics (1903), is usually taken as Russell's principal motive, at the time, for moving from a simple to a ramified theory of types. I argue that this view is mistaken. A closer study of Russell's correspondence with Frege reveals that Russell carne to adopt a very different resolution of the paradox, calling into question not the simplicity of his early type theory but the (...) simplicity of his early theory of propositions. (shrink)

The Russell–Myhill theorem threatens a familiar structured conception of propositions according to which two sentences express the same proposition only if they share the same syntactic structure and their corresponding syntactic constituents share the same semantic value. Given the role of the principle of universal instantiation in the derivation of the theorem in simple type theory, one may hope to rehabilitate the core of the structured view of propositions in ramified type theory, where the principle (...) is systematically restricted. We suggest otherwise. The ramified core of the structured theory of propositions remains inconsistent in ramified type theory augmented with axioms of reducibility. This is significant because reducibility has been thought to be perfectly consistent with the ramified approach to the intensional antinomies. Nor is the addition of reducibility to ramified type theory sufficient to restore other intensional puzzles such as Prior’s paradox or Kripke’s puzzle about time and thought. (shrink)

The paper first formalizes the ramified type theory as (informally) described in the Principia Mathematica [32]. This formalization is close to the ideas of the Principia, but also meets contemporary requirements on formality and accuracy, and therefore is a new supply to the known literature on the Principia (like [25], [19], [6] and [7]).As an alternative, notions from the ramified type theory are expressed in a lambda calculus style. This situates the type system (...) of Russell and Whitehead in a modern setting. Both formalizations are inspired by current developments in research on type theory and typed lambda calculus; see [3]. (shrink)

It is already known that Fitch’s knowability paradox can be solved by typing knowledge within ramified theory of types. One of the aims of this paper is to provide a greater defence of the approach against recently raised criticism. My second goal is to make a sufficient support for an assumption which is needed for this particular application of typing knowledge but which is not inherent to ramified theory of types as such.

As emphasized by Alonzo Church and David Kaplan (Church 1974, Kaplan 1975), the philosophies of language of Frege and Russell incorporate quite different methods of semantic analysis with different basic concepts and different ontologies. Accordingly we distinguish between a Fregean and a Russellian tradition in intensional semantics. The purpose of this paper is to pursue the Russellian alternative and to provide a language of intensional logic with a model-theoretic semantics. We also discuss the so-called Russell-Myhill paradox that threatens simple Russellian (...) type theory if propositions satisfies very strict principles of individuation. One way of avoiding the paradox is to adopt a ramified rather than a simple theory of types. (shrink)

This paper examines the quantification theory of *9 of Principia Mathematica. The focus of the discussion is not the philosophical role that section *9 plays in Principia's full ramified type-theory. Rather, the paper assesses the system of *9 as a quantificational theory for the ordinary predicate calculus. The quantifier-free part of the system of *9 is examined and some misunderstandings of it are corrected. A flaw in the system of *9 is discovered, but it is (...) shown that with a minor repair the system is semantically complete. Finally, the system is contrasted with the system of *8 of Principia's second edition. (shrink)

This reissue, first published in 1971, provides a brief historical account of the Theory of Logical Types; and describes the problems that gave rise to it, its various different formulations (Simple and Ramified), the difficulties connected with each, and the criticisms that have been directed against it. Professor Copi seeks to make the subject accessible to the non-specialist and yet provide a sufficiently rigorous exposition for the serious student to see exactly what the theory is and how (...) it works. (shrink)

Tichý’s Transparent Intensional Logic (TIL) is an overarching logical framework apt for the analysis of all sorts of discourse, whether colloquial, scientific, mathematical or logical. The theory is a procedural (as opposed to denotational) one, according to which the meaning of an expression is an abstract, extra-linguistic procedure detailing what operations to apply to what procedural constituents to arrive at the product (if any) of the procedure that is the object denoted by the expression. Such procedures are rigorously defined (...) as TIL constructions. Though TIL analytical potential is very large, deduction in TIL has been rather neglected. Tichý defined a sequent calculus for pre-1988 TIL, that is TIL based on the simple theory of types. Since then no other attempt to define a proof calculus for TIL has been presented. The goal of this paper is to propose a generalization and adjustment of Tichý’s calculus to TIL 2010. First, I briefly recapitulate the rules of simple-typed calculus as presented by Tichý. Then, I propose the adjustments of the calculus so that it be applicable to hyperintensions within the ramified hierarchy of types. TIL operates with a single procedural semantics for all kinds of logical-semantic context, be it extensional, intensional or hyperintensional. I show that operating in a hyperintensional context is far from being technically trivial. Yet, it is feasible. To this end, we introduce a substitution method that operates on hyperintensions. It makes use of a four-place substitution function (called Sub) defined over hyperintensions. (shrink)

This is part two of a two-part paper in which we develop an axiomatic theory of the relation of partial ground. The main novelty of the paper is the of use of a binary ground predicate rather than an operator to formalize ground. In this part of the paper, we extend the base theory of the first part of the paper with hierarchically typed truth-predicates and principles about the interaction of partial ground and truth. We show that our (...) theory is a proof-theoretically conservative extension of the ramified theory of positive truth up to. (shrink)

In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910-1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating (...) on Frege's Grundgesetze der Arithmetik for which Russell applied his famous paradox and this led him to introduce the first theory of types, the Ramified Type Theory (RTT). We present RTT formally using the modern notation for type theory and we discuss how Ramsey, Hilbert and Ackermann removed the orders from RTT leading to the simple theory of types STT. We present STT and Church's own simply typed λ-calculus (λ → C) and we finish by comparing RTT, STT and λ → C. (shrink)

This open access book examines the many contributions of Paul Lorenzen, an outstanding philosopher from the latter half of the 20th century. It features papers focused on integrating Lorenzen's original approach into the history of logic and mathematics. The papers also explore how practitioners can implement Lorenzen’s systematical ideas in today’s debates on proof-theoretic semantics, databank management, and stochastics. Coverage details key contributions of Lorenzen to constructive mathematics, Lorenzen’s work on lattice-groups and divisibility theory, and modern set theory (...) and Lorenzen’s critique of actual infinity. The contributors also look at the main problem of Grundlagenforschung and Lorenzen’s consistency proof and Hilbert’s larger program. In addition, the papers offer a constructive examination of a Russell-style Ramified Type Theory and a way out of the circularity puzzle within the operative justification of logic and mathematics. Paul Lorenzen's name is associated with the Erlangen School of Methodical Constructivism, of which the approach in linguistic philosophy and philosophy of science determined philosophical discussions especially in Germany in the 1960s and 1970s. This volume features 10 papers from a meeting that took place at the University of Konstanz. (shrink)

The axiom of reducibility plays an important role in the logic of Principia Mathematica, but has generally been condemned as an ad hoc non-logical axiom which was added simply because the ramified type theory without it would not yield all the required theorems. In this paper I examine the status of the axiom of reducibility. Whether the axiom can plausibly be included as a logical axiom will depend in no small part on the understanding of propositional functions. (...) If we understand propositional functions as constructions of the mind, it is clear that the axiom is clearly not a logical axiom and in fact makes an implausible claim. I look at two other ways of understanding propositional functions, a nominalist interpretation along the lines of Landini and a realist interpretation along the lines of Linsky and Mares. I argue that while on either of these interpretations it is not easy to see the axiom as a non-logical claim about the world, there are also appear to be difficulties in accepting it as a purely logical axiom. (shrink)

Since virtually every mathematical theory can be interpreted in Zermelo-Fraenkel set theory, it is a foundation for mathematics. There are other foundations, such as alternate set theories, higher-order logic, ramified type theory, and category theory. Whether set theory is the right foundation for mathematics depends on what a foundation is for. One purpose is to provide the ultimate metaphysical basis for mathematics. A second is to assure the basic epistemological coherence of all mathematical (...) knowledge. A third is to serve mathematics, by lending insight into the various fields and suggesting fruitful techniques of research. A fourth purpose of a foundation is to provide an arena for exploring relations and interactions between mathematical fields. While set theory does better with regard to some of these and worse with regard to others, it has become the de facto arena for deciding questions of existence, something one might expect of a foundation. Given the different goals, there is little point to determining a single foundation for all of mathematics. (shrink)

We discuss Lorenzen’s consistency proof for ramified type theory without reducibility, published in 1951, in its historical context and highlight Lorenzen’s contribution to the development of modern proof theory, notably by the introduction of the ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\omega$$\end{document}-rule.

The present paper is concerned with a ramified type theory (cf. (Lorenzen 1955), (Russell), (Schütte), (Weyl), e.g.,) in a cumulative version. §0 deals with reasoning in first order languages. is introduced as a first order set.

In this article, I examine the ramified-type theory set out in the first edition of Russell and Whitehead's Principia Mathematica. My starting point is the ‘no loss of generality’ problem: Russell, in the Introduction (Russell, B. and Whitehead, A. N. 1910. Principia Mathematica, Volume I, 1st ed., Cambridge: Cambridge University Press, pp. 53–54), says that one can account for all propositional functions using predicative variables only, that is, dismissing non-predicative variables. That claim is not self-evident at all, (...) hence a problem. The purpose of this article is to clarify Russell's claim and to solve the ‘no loss of generality’ problem. I first remark that the hierarchy of propositional functions calls for a fine-grained conception of ramified types as propositional forms (‘ramif-types’). Then, comparing different important interpretations of Principia’s theory of types, I consider the question as to whether Principia allows for non-predicative propositional functions and variables thereof. I explain how the distinction between the formal system of the theory, on the one hand, and its realizations in different epistemic universes, on the other hand, makes it possible to give us a more satisfactory answer to that question than those given by previous commentators, and, as a consequence, to solve the ‘no loss of generality’ problem. The solution consists in a substitutional semantics for non-predicative variables and non-predicative complex terms, based on an epistemic understanding of the order component of ramified types. The rest of the article then develops that epistemic understanding, adding an original epistemic model theory to the formal system of types. This shows that the universality sought by Russell for logic does not preclude semantical considerations, contrary to what van Heijenoort and Hintikka have claimed. (shrink)

In a 2010 paper Daley argues, contra Fodor, that several syntactically simple predicates express structured concepts. Daley develops his theory of structured concepts within Tichý’s Transparent Intensional Logic . I rectify various misconceptions of Daley’s concerning TIL. I then develop within TIL an improved theory of how structured concepts are structured and how syntactically simple predicates are related to structured concepts.

This paper offers an interpretation of Russell's multiple-relation theory of judgment which characterizes it as direct application of the 1905 theory of definite descriptions. The paper maintains that it was by regarding propositional symbols (when occurring as subordinate clauses) as disguised descriptions of complexes, that Russell generated the philosophical explanation of the hierarchy of orders and the ramified theory of types of _Principia mathematica (1910). The interpretation provides a new understanding of Russell's abandoned book _Theory of (...) Knowledge (1913), the 'direction problems' and Wittgenstein's criticisms. (shrink)

Although everyone knows that Russell had an immense influence upon Wittgenstein's early philosophy, the degree to which Wittgenstein is either adopting or renouncing Russell's views is still largely a matter of dispute. Recent commentators have been in nearly univocal agreement that the Tractatus should be understood as a rejection of Russell's philosophy, and that Wittgenstein was instead more influenced by the "great works of Frege." In his earlier work, Gregory Landini has proposed a more nuanced way to understand Russell than (...) is commonly assumed. In his new book, Landini directs his attention at re-thinking Wittgenstein's early philosophy in light of his revolutionary interpretation of Russell.Too often Russell is read backwards, as it were; that is, his views in later published works are assimilated back into Principia Mathematica. And this leads commentators to interpret the Tractatus as criticizing views which Russell simply did not hold. Two "dogmas" that are commonly perpetuated about Russell are: first, that Principia features a ramified type-theory of entities; and second, that logical atomism is a theory of reductive empiricism, grounded upon "knowledge by acquaintance.". (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)

This paper presents an exposition of subsystems and of Quine's , originally defined and shown to be consistent by Crabbé, along with related systems and of type theory. A proof that (and so ) interpret the ramified theory of types is presented (this is a simplified exposition of a result of Crabbé). The new result that the consistency strength of is the same as that of is demonstrated. It will also be shown that cannot be finitely (...) axiomatized (as can and ). (shrink)

The problematic features of Quine's set theories NF and ML are a result of his replacing the higher-order predicate logic of type theory by a first-order logic of membership, and can be resolved by returning to a second-order logic of predication with nominalized predicates as abstract singular terms. We adopt a modified Fregean position called conceptual realism in which the concepts (unsaturated cognitive structures) that predicates stand for are distinguished from the extensions (or intensions) that their nominalizations denote (...) as singular terms. We argue against Quine's view that predicate quantifiers can be given a referential interpretation only if the entities predicates stand for on such an interpretation are the same as the classes (assuming extensionality) that nominalized predicates denote as singular terms. Quine's alternative of giving predicate quantifiers only a substitutional interpretation is compared with a constructive version of conceptual realism, which with a logic of nominalized predicates is compared with Quine's description of conceptualism as a ramified theory of classes. We argue against Quine's implicit assumption that conceptualism cannot account for impredicative concept-formation and compare holistic conceptual realism with Quine's class Platonism. (shrink)

In Appendix B of Russell's The Principles of Mathematics occurs a paradox, the paradox of propositions, which a simple theory of types is unable to resolve. This fact is frequently taken to be one of the principal reasons for calling ramification onto the Russellian stage. The paper presents a detaiFled exposition of the paradox and its discussion in the correspondence between Frege and Russell. It is argued that Russell finally adopted a very simple solution to the paradox. This solution (...) had nothing to do with ramified types but marked an important shift in his theory of propositions. (shrink)

The Analytic Tradition in Philosophy is an excellent successor to an excellent book : It is a fine an example of the necromantic style in the history of philosophy where the object of the exercise is to resurrect the mighty dead in order to get into an argument with them, either because we think them importantly right or instructively wrong. However what was a pardonable a simplification and a reasonable omission in the earlier book has now metamorphosed into a sin (...) of omission and an oversimplification in its successor—the book lacks is an adequate discussion of the Ramified Theory of Types and Russell’s reasons for adopting it. I conclude with a brief meditation on Open Question Arguments and the threats that they pose to some of the analyses proposed by Russell and Moore themselves. (shrink)

RésuméLa théorie des expressions incomplétes dans Principia Mathematica, se fonde sur le principe déja appliqué par Russell dans “On Denoting”, selon lequel il est souhaitable dans certains cas, ?on;établir le statut syntaxique des expressions catégorématiques. Grâce à la théorie intensionnelle ramifyée des types, les expressions incomplétes réféientiellement pourront être logiquement caractérisées par un mode de dérivation principalement basé sur la quantification non‐objectuelle. Ľintroduction des classes cependant, n'est en aucune façon reliée à ce mode intensionnel de dérivation; il en résulte qu'elles (...) fonctionnent en réalité dans ce contexte comme des expressions pourvues de dénotation et ce n'est que par une analogie grammaticale que Russell peut les comparer, du point de vue de leur élimination, aux expressions incomplétes de Principia Mathematica.SummaryThe theory of incomplete symbols in Principia Mathematica is founded on the principle already applied by Russell in “On Denoting“ that it is desirable in certain cases, to establish the syntactical status of “categorematic” expressions. Thanks to the intensional ramified theory of types, the referentially incomplete expressions could be logically caracterised by a mode of derivation primarily based on non‐objectual quantification. The introduction of classes, however, is by no way linked to that intensional mode of derivation; as a result, they function, in that context, like denotative expressions and it is only by a “grammatical” analogy that Russell can compare them, as regards their elimination, to the incomplete symbols in Principia Mathematica.ZusammenfassungDie Theorie der unvollstandigen Symbole in den Principia Mathematica gründet auf dem von Russell schon in “On Denoting” angewendeten Prinzip, wonach es in gewissen Fällen wün‐schenswert ist, den syntaktischen Status kategorematischer Ausdrücke festzulegen. Aufgrund der intensionalen verzweigten Typentheorie könnte man die referentiell unvollständigen Ausdrücke logisch durch eine im wesentlichen auf die nicht objektuelle Quantifi‐kation abstellende Ableitungsart charakterisieren. Die Einführung der Klassen dagegen hüngt keineswegs von dieser intensionalen Ableitungsart ab; daraus geht hervor, dass sie in diesem Kontext wie denotative Ausdrücke funktionieren, und es gelingt Russell nur vermittels einer grammatische Analogie, sie hinsichtlich ihrer Elimination mit den unvollständigen Symbolen der Principia Mathematica zu vergleichen. (shrink)

There is an apparent dilemma for hierarchical accounts of propositions, raised by Bruno Whittle : either such accounts do not offer adequate treatment of connectives and quantifiers, or they eviscerate the logic. I discuss what a plausible hierarchical conception of propositions might amount to, and show that on that conception, Whittle’s dilemma is not compelling. Thus, there are good reasons why proponents of hierarchical accounts of propositions did not see the difficulty Whittle raises.

본 연구는 논리학 및 수리논리학의 토대 개념인 동일성 원리에 대한 역사적인 논쟁들의 교육학적 함의를 도출하는 것이다. 이때 필자가 사용할 중심 방법은 구조-구성주의 인식론이다. 따라서 필자는 구조-구성주의 인식론의 관점에서 동일성 원리에 대한 핵심 논쟁들을 역사-비판적으로 재구성함으로써, 필자가 지속적으로 논변해 온 구조-구성주의 교수학습이론의 확고한 토대를 제공하고자 한다. 이를 위해 본고는 동일성 원리에 대한 역사발생학적 탐구와 정신발생학적 탐구를 종합한다. 구체적인 내용은 피아제의 발생학적 인식론의 관점에서 논리적 개념들 및 공리화에 대한 프레게-러셀의 선험주의적 논리주의와 비트겐슈타인의 회의론적 유명론을 동시에 비판하면서, 구조-구성주의 인식론 및 이것의 교육학적 함의를 (...) 도출하는 것이다. 본고의 최종 결론은 이것이다. 논리적 법칙 또는 공리들은 초인적인 논리학자의 선험적인 직관에 의해서 구성된 것도 아니고, 유명론적 입장의 순수 기호게임으로 환원되는 것도 아니라, 정신 발달과 함께 발달되는 주체와 대상의 상호작용의 결과물, 즉 조작적 구조들의 형식화에 근거한다. 따라서 논리학적 개념들뿐만 아니라, 모든 일반적인 개념을 교육할 때, 교사는 실체와 술어, 개념과 판단, 판단과 추론 사이에 성립되는 미시적 상호의존성과 순환성뿐만 아니라, 이들 전체들 사이에 성립하는 거시적 상호의 존성과 순환성을 동시에 고려해야 한다. (shrink)

The following note has on purpose to introduce interested students to logicism. Our objective is not to show any new interpretation or thesis about logicism or its rebirth between the 60s and 80s of the last century. What we will do is systematically show the evolution of logicism from Frege to Russell-Whitehead, with greater emphasis on this latest development, and approach some problems that arise within that movement, for example: The logical paradoxes and the principle of intuitive comprehension, the impredicative (...) definitions and the semantic paradoxes, the Ramified Hierarchy and real numbers, the axiom of reducibility and the impossibility of reducing mathematics to logic, etc. (shrink)

Standard Type Theory, STT, tells us that b^n(a^m) is well-formed iff n=m+1. However, Linnebo and Rayo have advocated the use of Cumulative Type Theory, CTT, has more relaxed type-restrictions: according to CTT, b^β(a^α) is well-formed iff β > α. In this paper, we set ourselves against CTT. We begin our case by arguing against Linnebo and Rayo’s claim that CTT sheds new philosophical light on set theory. We then argue that, while CTT ’s (...) class='Hi'>type-restrictions are unjustifiable, the type-restrictions imposed by STT are justified by a Fregean semantics. What is more, this Fregean semantics provides us with a principled way to resist Linnebo and Rayo’s Semantic Argument for CTT. We end by examining an alternative approach to cumulative types due to Florio and Jones; we argue that their theory is best seen as a misleadingly formulated version of STT. (shrink)

Recent debates in metaphysics have highlighted the significance of type theories, such as Simple Type Theory (STT), for our philosophical analysis. In this chapter, I present the salient features of a constructive type theory in the style of Martin-Löf, termed CTT. My principal aim is to convey the flavour of this rich, flexible and sophisticated theory and compare it with STT. I especially focus on the forms of quantification which are available in CTT. A (...) further aim is to argue that a comparison between a plurality of theories is beneficial to the philosophical analysis. We may, for example, discover helpful features of one theory that we may want to import into another context, thus enriching our repertoire of formal tools. Or, through comparison with a less well-known theory, we may gain a better understanding of the characteristics of the theories we are familiar with. As argued in this chapter, CTT has much to offer in all of these respects. (shrink)

Type theory is a fast-evolving field at the crossroads of logic, computer science and mathematics. This gentle step-by-step introduction is ideal for graduate students and researchers who need to understand the ins and outs of the mathematical machinery, the role of logical rules therein, the essential contribution of definitions and the decisive nature of well-structured proofs. The authors begin with untyped lambda calculus and proceed to several fundamental type systems culminating in the well-known and powerful Calculus of (...) Constructions. The book also covers the essence of proof checking and proof development, and the use of dependent type theory to formalize mathematics. The only prerequisites are a good knowledge of undergraduate algebra and analysis. Carefully chosen examples illustrate the theory throughout. Each chapter ends with a summary of the content, some historical context, suggestions for further reading and a selection of exercises to help readers familiarize themselves with the material. (shrink)

Selection type theories solve adaptation problems. Natural selection, clonal selection for antibody production, and selective theories of higher brain function are examples. An abstract characterization of typical selection processes is generated by analyzing and extending previous work on the nature of natural selection. Once constructed, this abstraction provides a useful tool for analyzing the nature of other selection theories and may be of use in new instances of theory construction. This suggests the potential fruitfulness of research to find (...) other theory types and construct their abstractions. (shrink)

We introduce a predicative version of topos based on the notion of small maps in algebraic set theory, developed by Joyal and one of the authors. Examples of stratified pseudotoposes can be constructed in Martin-Löf type theory, which is a predicative theory. A stratified pseudotopos admits construction of the internal category of sheaves, which is again a stratified pseudotopos. We also show how to build models of Aczel-Myhill constructive set theory using this categorical structure.