Search

Cet article est une suite a Outline of a revised formulation of logic of sense and denotation (Nous, 1973-1974).

In this paper we treat the ramified type theory of Russell [6], afterwards adopted by Whitehead and Russell inPrincipia 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 ofPrincipia(seePreface, 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 formerr-types.There is an r-typeito which the individual variables belong. Ifβ1,β2, …,βmare any given r-types,m≧ 0, there is an r-type (β1,β2, …,βm)/nto which there belongm-ary functional variables of leveln,n≧ 1. The r-type (α1,α2, …,αm)/kis said to bedirectly lowerthan the r-type (β1,β2, …,βm)/nifα1=β1,α2=β2, …,αm=βm,k

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

Church Alonzo. Special Cases of the Decision Problem. In: Revue Philosophique de Louvain. Troisième série, tome 49, n°22, 1951. pp. 203-221.

The postulate A1 can be weakened with respect to the set Al, A., A3, , A, if there exists a postulate, A', weaker than Al, such that the logical product A'A2 A8. A. implies Al. Under this definition we say that a postulate can be weakened with respect to a set of postulates, of which it is one, only when it can be replaced in the set by a weaker postulate in such a way that none of the implications of the set as a whole is lost. A set of postulates is irredundant if the postulates are independent and no one of them can be weakened with respect to the set.

ly the Kollektiv may be represented by an infinite sequence of points of an appropriate space, the Merkmalraum. Or if the number of possible outcomes of a trial is finite (and it may well be argued that this is always the case for any actual physical observation), it is sufficient to employ an infinite sequence of natural numbers which are less than a fixed natural number. This infinite sequence—of points or of natural numbers—satisfies certain conditions which correspond to those appearing in the description of a Kollektiv as just given, and which we shall express by saying that it is a random sequence (regel

A method is presented for reducing a curvilinear response to a set of numbers which describe the curve. An analysis of such numbers including reconstruction of the curves is presented. A numerical example is used to illustrate the entire procedure.

In this paper a theorem about numerical relations will be established and shown to have certain consequences concerning decidability in quantification theory, as well as concerning the foundation of number theory. The theorem is that relations of natural numbers are reducible in elementary fashion to symmetric ones; i.e.:Theorem I. For every dyadic relation R of natural numbers there is a symmetric dyadic relation H of natural numbers such that R is definable in terms of H plus just truth-functions and quantification over natural numbers.To state the matter more fully, there is a (well-formed) formula ϕ of pure quantification theory, or first-order functional calculus, which meets these conditions:(a) ϕ has ‘x’ and ‘y’ as sole free individual variables;(b) ϕ contains just one predicate letter, and it is dyadic;(c) for every dyadic relation R of natural numbers there is a symmetric dyadic relation H of natural numbers such that, when the predicate letter in ϕ is interpreted as expressing H, ϕ comes to agree in truth-value with ‘x bears R to y’ for all values of ‘x’ and ‘y’.