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.

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)

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)

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)

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 type-theory (...) and suggest an alternative one to explain Russell's reaction. (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)

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)

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

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)

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)

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.

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)

We defend hylomorphism against Maegan Fairchild’s purported proof of its inconsistency. We provide a deduction of a contradiction from SH+, which is the combination of “simple hylomorphism” and an innocuous premise. We show that the deduction, reminiscent of Russell’s Paradox, is proof-theoretically valid in classical higher-order logic and invokes an impredicatively defined property. We provide a proof that SH+ is nevertheless consistent in a free higher-order logic. It is shown that the unrestricted comprehension principle of property abstraction on which the (...) purported proof of inconsistency relies is analogous to naïve unrestricted set-theoretic comprehension. We conclude that logic imposes a restriction on property comprehension, a restriction that is satisfied by the ramified theory of types. By extension, our observations constitute defenses of theories that are structurally similar to SH+, such as the theory of singular propositions, against similar purported disproofs. (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)

This volume of Bertrand Russell's Collected Papers finds Russell focused on writing Principia Mathematica during 1905–08. Eight previously unpublished papers shed light on his different versions of a substitutional theory of logic, with its elimination of classes and relations, during 1905-06. A recurring issue for him was whether a type hierarchy had to be part of a substitutional theory. In mid-1907 he began writing up the final version of Principia , now using a ramified theory of (...) types, and eleven unpublished drafts from 1907-08 deal with this. Numerous letters show his thoughts on the process. The volume's 80-page introduction covers the evolution of his logic from 1896 until 1909, when volume I of Principia went to the printer. (shrink)

A paradox about sets of properties is presented. The paradox, which invokes an impredicatively defined property, is formalized in a free third-order logic with lambda-abstraction, through a classically proof-theoretically valid deduction of a contradiction from a single premise to the effect that every property has a unit set. Something like a model is offered to establish that the premise is, although classically inconsistent, nevertheless consistent, so that the paradox discredits the logic employed. A resolution through the ramified theory (...) of types is considered. Finally, a general scheme that generates a family of analogous paradoxes and a generally applicable resolution are proposed. (shrink)

This volume of Bertrand Russell's _Collected Papers_ finds Russell focused on writing _Principia Mathematica_ during 1905–08. Eight previously unpublished papers shed light on his different versions of a substitutional theory of logic, with its elimination of classes and relations, during 1905-06. A recurring issue for him was whether a type hierarchy had to be part of a substitutional theory. In mid-1907 he began writing up the final version of _Principia_, now using a ramified theory of (...) class='Hi'>types, and eleven unpublished drafts from 1907-08 deal with this. Numerous letters show his thoughts on the process. The volume's 80-page introduction covers the evolution of his logic from 1896 until 1909, when volume I of _Principia _went to the printer. (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 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)

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)

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)

Bertrand Russell's contributions to last century's philosophy and, in particular, to the philosophy of mathematics cannot be overestimated.Russell, besides being, with Frege and G.E. Moore, one of the founding fathers of analytical philosophy, played a major rôle in the development of logicism, one of the oldest and most resilient1 programmes in the foundations of mathematics.Among his many achievements, we need to mention the discovery of the paradox that bears his name and the identification of its logical nature; the generalization to (...) the whole of mathematics of Frege's idea that it is not possible to draw a demarcation line between logic and arithmetic; the programme, carried out with Whitehead, of derivation of mathematics from the logical system of Principia Mathematica ; and the ramified theory of types, devised by Russell to protect the system of PM from the known paradoxes.Although there is an ample literature on these topics, it is quite important to reconsider Russell's contributions to the foundations of mathematics at a time when, as a consequence of the crisis of the classical programmes in the foundations of mathematics, new trends are beginning to develop within the philosophy of mathematics. These are trends which move in a very different direction from that of logicism, intuitionism, and Hilbert's programme.To see this we need to consider that, in spite of profound disagreements on the nature of mathematical activity, on the relationship existing between logic and mathematics, on the causes of and therapies for the paradoxes, etc., logicism, intuitionism, and Hilbert's programme share an important metaphor: the idea that mathematics is an edifice built on unshakable foundations,2 an edifice which makes possible only a cumulative growth of mathematical knowledge.Such a metaphor—which, together with more specific theses belonging to these schools of thought, remained unsupported …. (shrink)

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

In this paper we define intensional models for the classical theory of types, thus arriving at an intensional type logic ITL. Intensional models generalize Henkin's general models and have a natural definition. As a class they do not validate the axiom of Extensionality. We give a cut-free sequent calculus for type theory and show completeness of this calculus with respect to the class of intensional models via a model existence theorem. After this we turn our attention to (...) applications. Firstly, it is argued that, since ITL is truly intensional, it can be used to model ascriptions of propositional attitude without predicting logical omniscience. In order to illustrate this a small fragment of English is defined and provided with an ITL semantics. Secondly, it is shown that ITL models contain certain objects that can be identified with possible worlds. Essential elements of modal logic become available within classical type theory once the axiom of Extensionality is given up. (shrink)

It is often claimed that the theory of function levels proposed by Frege in Grundgesetze der Arithmetik anticipates the hierarchy of types that underlies Church’s simple theory of types. This claim roughly states that Frege presupposes a type of functions in the sense of simple type theory in the expository language of Grundgesetze. However, this view makes it hard to accommodate function names of two arguments and view functions as incomplete entities. I propose and defend (...) an alternative interpretation of first-level function names in Grundgesetze into simple type-theoretic open terms rather than into closed terms of a function type. This interpretation offers a still unhistorical but more faithful type-theoretic approximation of Frege’s theory of levels and can be naturally extended to accommodate second-level functions. It is made possible by two key observations that Frege’s Roman markers behave essentially like open terms and that Frege lacks a clear criterion for distinguishing between Roman markers and function names. (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)

We introduce a certain extension of -calculus, and show that it has the Church-Rosser property. The associated open-term extensional combinatory algebra is used as a basis to construct models for theories of Explict Mathematics (formulated in the language of "types and names") with positive stratified comprehension. In such models, types are interpreted as collections of solutions (of terms) w.r. to a set of numerals. Exploiting extensionality, we prove some consistency results for special ontological axioms which are refutable under (...) elementary comprehension. (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)

I investigate why Frege rejected the theory of types, as Russell presented it to him in their correspondence. Frege claims that it commits one to violations of the law of excluded middle, but this complaint seems to rest on a dogmatic refusal to take Russell’s proposal seriously on its own terms. What is at stake is not so much the truth of a law of logic, but the structure of the hierarchy of the logical categories, something Frege seems (...) to neglect. To come to a better understanding of Frege’s response, I proceed to investigate his conception of the nature of the logical categories, and how it differs from Russell’s. I argue that, for Frege, our grasp of the logical categories cannot be severed from our grasp of the Begriffsschrift notation itself. Russell, on the other hand, attaches no such importance to notation. From Frege’s point of view, Russell has not succeeded in presenting an alternative conception of the logical hierarchy, since such a conception must go in tandem with the development of a notation. Moreover, Frege has good reasons to think that Russell’s proposal does not admit of a suitable notation. (shrink)