Theory of types

DOI: 10.4324/9780415249126-Y030-1
Version: v1,  Published online: 1998
Retrieved March 02, 2021, from

3. The simple v. the ramified theory of types

The simple theory of types suffices to avoid the logical paradoxes, but not the semantic ones, unless a distinction is made (as first proposed by A. Tarski) between the object language of simple type theory and a metalanguage in which the different semantic notions for the expressions of simple type theory can be defined or developed axiomatically (see Tarski’s definition of truth). The ramified theory of types avoids the semantic paradoxes by incorporating an additional hierarchy of levels that (combined with the hierarchy of orders) implicitly contains a hierarchy of languages, and that in effect amounts to a special form of the metalanguage/object language distinction by which the semantic (and related intensional) paradoxes can be avoided (as noted by Church 1976: §4). Adding the axiom of reducibility does not nullify the way ramified type theory resolves or avoids the semantic (and related intensional) paradoxes. (See Church (1976: §5) and Myhill (1979) for justification of this claim.)

Different versions of the simple theory of types have been formulated by L. Chwistek (1922), F. Ramsey (1931), R. Carnap (1929), K. Gödel (1931), and A. Church (1940). The simple theory is not committed to an extensional logic, although it is often formulated as such. R.M. Montague (1974), for example, extended Church’s simple theory of types by incorporating into it operators for representing the intensions and extensions of expressions, and then used the resulting system as an intensional logic by which to provide an interpretation of a variety of intensional contexts of natural language (along lines originally described by Frege). Church (1974) has also formulated an intensional version of the simple theory by adding to it a formula operator for the Russellian notion of propositional identity. But in 1984, Church also showed that, given Russell’s notion of a proposition, and hence of propositional identity, Russell’s antinomy of propositions (Russell 1903: §500) can be reconstructed in simple type theory, but not in ramified type theory. According to this antinomy, there cannot be more classes of propositions than there are propositions – because every non-empty class of propositions can be associated with its ‘logical product’, which, by Russell’s notion of propositional identity, is unique for that class; and yet, by Cantor’s theorem, there must be more classes of propositions than there are propositions (see Cantor’s theorem).

Citing this article:
Cocchiarella, Nino B.. The simple v. the ramified theory of types. Theory of types, 1998, doi:10.4324/9780415249126-Y030-1. Routledge Encyclopedia of Philosophy, Taylor and Francis,
Copyright © 1998-2021 Routledge.

Related Searches


Related Articles