On the theory of types

1938 ◽  
Vol 3 (4) ◽  
pp. 125-139 ◽  
Author(s):  
W. V. Quine
Keyword(s):  
Infinite Series ◽  
Type Theory ◽  
Simple Theory ◽  
Minimal Set ◽  
Logical Constants ◽  
Formal Restriction ◽  
Russell's Paradox ◽  
Logical Paradoxes ◽  
Finite Arithmetic ◽  
Logical Types

In this paper the theory of logical types will be examined, and certain departures from it will be suggested. Though the purpose of the paper is not primarily expository, an approach has been possible which presupposes no familiarity with special literature. Matters at variance with such an approach have been confined to appendices and footnotes.In the early pages the logical paradoxes will be considered—an infinite series of them, of which Russell's paradox is the first. Then Russell's simple theory of types will be formulated, in adaptation to a minimal set of logical primitives: inclusion and abstraction. Two aspects of the theory will be distinguished: an ontological doctrine and a formal restriction. It will be found that by repudiating the former we can avoid certain unnatural effects of the type theory—notably the reduplication of logical constants from type to type, and the apparent dependence of finite arithmetic upon an axiom of infinity. But the formal restriction itself has unnatural effects, which survive, even in an aggravated form, after the type ontology has been dropped. A liberalization of the formal restriction will be proposed which removes the more irksome of these anomalies.

Types in Logic and Mathematics Before 1940

2002 ◽  
Vol 8 (2) ◽  
pp. 185-245 ◽  
Author(s):  
Fairouz Kamareddine ◽  
Twan Laan ◽  
Rob Nederpelt
Keyword(s):  
19Th Century ◽  
Type Theory ◽  
Simple Theory ◽  
Formal Systems ◽  
Modern Notation ◽  
And Mathematics ◽  
Logical Paradoxes ◽  
The 19Th Century

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

Comparison of Russell's resolution of the semantical antinomies with that of Tarski

1976 ◽  
Vol 41 (4) ◽  
pp. 747-760 ◽  
Author(s):  
Alonzo Church
Keyword(s):  
Type Theory ◽  
Simple Theory ◽  
Vicious Circle ◽  
New Members ◽  
Domain Type ◽  
Individual Variables ◽  
The Individual ◽  
Essential Restriction

In this paper we treat the ramified type theory of Russell [6], afterwards adopted by Whitehead and Russell in Principia mathematica [12], so that we may compare Russell's resolution of the semantical antinomies by ramified type theory with the now widely accepted resolution of them by the method of Tarski in [7], [8], [9].To avoid impredicativity the essential restriction is that quantification over any domain (type) must not be allowed to add new members to the domain, as it is held that adding new members changes the meaning of quantification over the domain in such a way that a vicious circle results. As Whitehead and Russell point out, there is no one particular form of the doctrine of types that is indispensable to accomplishing this restriction, and they have themselves offered two different versions of the ramified hierarchy in the first edition of Principia (see Preface, p. vii). The version in §§58–59 of the writer's [1], which will be followed in this paper, is still slightly different.To distinguish Russellian types or types in the sense of the ramified hierarchy from types in the sense of the simple theory of types, let us call the former r-types.There is an r-type i to which the individual variables belong. If β1, β2, …, βm are any given r-types, m ≧ 0, there is an r-type (β1, β2, …, βm)/n to which there belong m-ary functional variables of level n, n ≧ 1. The r-type (α1, α2, …, αm)/k is said to be directly lower than the r-type (β1, β2, …, βm)/n if α1 = β1, α2 = β2, …, αm = βm, k < n.

Paradoxes of set and property

2018 ◽  
Author(s):  
Gregory H. Moore
Keyword(s):  
Cardinal Number ◽  
Liar Paradox ◽  
Semantic Paradoxes ◽  
Russell’S Paradox ◽  
Medieval Europe ◽  
Power Set ◽  
Semantic Concepts ◽  
Logical Paradox ◽  
Russell's Paradox ◽  
Logical Paradoxes

Emerging around 1900, the paradoxes of set and property have greatly influenced logic and generated a vast literature. A distinction due to Ramsey in 1926 separates them into two categories: the logical paradoxes and the semantic paradoxes. The logical paradoxes use notions such as set or cardinal number, while the semantic paradoxes employ semantic concepts such as truth or definability. Both often involve self-reference. The best known logical paradox is Russell’s paradox concerning the set S of all sets x such that x is not a member of x. Russell’s paradox asks: is S a member of itself? A moment’s reflection shows that S is a member of itself if and only if S is not a member of itself – a contradiction. Russell found this paradox by analysing the paradox of the largest cardinal. The set U of all sets has the largest cardinal number, since every set is a subset of U. But there is a cardinal number greater than that of any given set M, namely the cardinal of the power set, or set of all subsets, of M. Thus the cardinal of the power set of U is greater than that of U, a contradiction. (The paradox of the largest ordinal, discussed below, is similar in structure.) Among the semantic paradoxes, the best known is the liar paradox, found by the ancient Greeks. A man says that he is lying. Is what he says true or false? Again, either conclusion leads to its opposite. Although this paradox was debated in medieval Europe, its modern interest stems from Russell, who placed it in the context of a whole series of paradoxes, including his own.

A formulation of the simple theory of types

1940 ◽  
Vol 5 (2) ◽  
pp. 56-68 ◽  
Author(s):  
Alonzo Church
Keyword(s):  
Type Theory ◽  
Point Of View ◽  
Simple Theory ◽  
And Mathematics

The purpose of the present paper is to give a formulation of the simple theory of types which incorporates certain features of the calculus of λ-conversion. A complete incorporation of the calculus of λ-conversion into the theory of types is impossible if we require that λx and juxtaposition shall retain their respective meanings as an abstraction operator and as denoting the application of function to argument. But the present partial incorporation has certain advantages from the point of view of type theory and is offered as being of interest on this basis (whatever may be thought of the finally satisfactory character of the theory of types as a foundation for logic and mathematics).For features of the formulation which are not immediately connected with the incorporation of λ-conversion, we are heavily indebted to Whitehead and Russell, Hilbert and Ackermann, Hilbert and Bernays, and to forerunners of these, as the reader familiar with the works in question will recognize.The class of type symbols is described by the rules that ı and o are each type symbols and that if α and β are type symbols then (αβ) is a type symbol: it is the least class of symbols which contains the symbols ı and o and is closed under the operation of forming the symbol (αβ) from the symbols α and β.

scholarly journals Sufficient Conditions for Absolute Cesàro Summable Factor

2019 ◽  
Vol 4 (3) ◽  
pp. 627-634
Author(s):  
Smita Sonker ◽  
Alka Munjal
Keyword(s):  
Impulse Response ◽  
Infinite Series ◽  
Sufficient Conditions ◽  
Absolute Summability ◽  
Sufficient Condition ◽  
Necessary And Sufficient Condition ◽  
Minimal Set ◽  
Bibo Stability ◽  
Necessary And Sufficient ◽  
Bounded Input

Quasi-f-power increasing sequence has been used for infinite series to establish a theorem on a minimal set of sufficient conditions for absolute Cesàro φ-|〖C,α;δ;l|〗_k summable factor. Further, a set of new and well-known arbitrary results have been obtained by using the main theorem. The presented main result has been validated by the previous result under suitable conditions. In this way, the Bounded Input Bounded Output (BIBO) stability of impulse response has been improved by finding a minimal set of sufficient conditions for absolute summability because absolute summable is the necessary and sufficient condition for BIBO stability.

On the axiom of extensionality – Part I

1956 ◽  
Vol 21 (1) ◽  
pp. 36-48 ◽  
Author(s):  
R. O. Gandy
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Formal System ◽  
Free Variable ◽  
Simple Theory ◽  
Predicate Calculus ◽  
Simple System ◽  
System A ◽  
Image Position

In part I of this paper it is shown that if the simple theory of types (with an axiom of infinity) is consistent, then so is the system obtained by adjoining axioms of extensionality; in part II a similar metatheorem for Gödel-Bernays set theory will be proved. The first of these results is of particular interest because type theory without the axioms of extensionality is fundamentally rather a simple system, and it should, I believe, be possible to prove that it is consistent.Let us consider — in some unspecified formal system — a typical expression of the axiom of extensionality; for example:where A(h) is a formula, and A(f), A(g) are the results of substituting in it the predicate variagles f, g for the free variable h. Evidently, if the system considered contains the predicate calculus, and if h occurs in A(h) only in parts of the form h(t) where t is a term which lies within the range of the quantifier (x), then 1.1 will be provable. But this will not be so in general; indeed, by introducing into the system an intensional predicate of predicates we can make 1.1 false. For example, Myhill introduces a constant S, where ‘Sϕψχω’ means that (the expression) ϕ is the result of substituting ψ for χ in ω.

General models, descriptions, and choice in type theory

1972 ◽  
Vol 37 (2) ◽  
pp. 385-394 ◽  
Author(s):  
Peter B. Andrews
Keyword(s):  
General Model ◽  
Type Theory ◽  
Combinatory Logic ◽  
Logical Constants ◽  
Simple Idea ◽  
Nonstandard Models ◽  
Selection Operator ◽  
Definition Of

In [4] Alonzo Church introduced an elegant and expressive formulation of type theory with λ-conversion. In [8] Henkin introduced the concept of a general model for this system, such that a sentence A is a theorem if and only if it is true in all general models. The crucial clause in Henkin's definition of a general model ℳ is that for each assignment φ of values in ℳ to variables and for each wff A, there must be an appropriate value of A in ℳ. Hintikka points out in [10, p. 3] that this constitutes a rather strong requirement concerning the structure of a general model. Henkin draws attention to the problem of constructing nonstandard models for the theory of types in [9, p. 324].We shall use a simple idea of combinatory logic to find a characterization of general models which does not directly refer to wffs, and which is easier to work with in certain contexts. This characterization can be applied, with appropriate minor and obvious modifications, to a variety of formulations of type theory with λ-conversion. We shall be concerned with a language ℒ with extensionality in which there is no description or selection operator, and in which (for convenience) the sole primitive logical constants are the equality symbols Qoαα for each type α.

Is Russell's Paradox Genuine?

Philosophy ◽  
1974 ◽  
Vol 49 (189) ◽  
pp. 295-302 ◽  
Author(s):  
James Moulder
Keyword(s):  
State Standard ◽  
Russell’S Paradox ◽  
Logical Paradox ◽  
Russell's Paradox ◽  
Three Stages ◽  
Logical Paradoxes

Copi, Quine and van Heijenoort have each claimed that there are two fundamentally different kinds of logical paradox; namely, genuine paradoxes like Russell's and pseudo-paradoxes like the Barber of Seville. I want to contest this claim and will present my case in three stages. Firstly, I will characterize the logical paradoxes; state standard versions of three of them; and demonstrate that a symbolic formulation of each leads to a formal contradiction. Secondly, I will discuss the reasons Copi, Quine and van Heijenoort have given for the distinction between genuine and pseudo-paradoxes. Thirdly, I will attempt to explain why there is no such class as the class of all and only those classes which are not members of themselves.

On the relative consistency of set theory

1956 ◽  
Vol 21 (3) ◽  
pp. 280-290 ◽  
Author(s):  
Steven Orey
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Simple Theory ◽  
Relative Consistency ◽  
System L

We present a method for demonstrating the consistency of von Neuman-Gödel set theory Σ (or Zermelo set theory Σ′) relative to various other formal set theories. When a model for a logic L1 is constructed, there are two other logics involved: L2, the system which contains the model, and L3, the metalogic in which the argument that L2 contains a model for L1 is carried out. These three systems need not of course all be distinct. In [2] L1 is Σ strengthened by the axiom ∨ = L, L2 is Σ, and L3 is unformalized. In the present paper L1 will be either Σ or Σ′. The basic idea for proving the relative consistency of L1 with respect to some other system L2 is to construct in L2 a model for L1 similar to the model constructed in [2]. Since L2 may be some kind of type theory, the function corresponding to Gödel's function F must be modified in a suitable manner. In verifying the relativized versions of axioms of L1 in L2, we shall have to overcome certain special problems depending on the system L2 and not met with in [2]. Except for the remarks at the end of Section 2, we shall not consider the question of formalizing L3, i.e. we use intuitive logic as our metalogic.In Section 1 we illustrate the method by demonstrating the consistency of Σ relative to the system ML″ obtained by adding E of [4] as an axiom to ML′ of [4]. We use the notation and results of [4] and [7].Section 2 discusses the use of certain other systems for L2. It will be noted that the systems used for L2 are always slightly strengthened versions of well known systems ([5], [6], and the simple theory of types); it is of course to be hoped that modifications may be discovered which would make the method work in the original, unstrengthened systems, or that the relative consistency of the strengthened systems with respect to the original systems can be established.

Sign in / Sign up

Export Citation Format

Share Document