# Theory of types

DOI
10.4324/9780415249126-Y030-1
DOI: 10.4324/9780415249126-Y030-1
Version: v1,  Published online: 1998
Retrieved December 05, 2020, from https://www.rep.routledge.com/articles/thematic/theory-of-types/v-1

## 2. The axiom of reducibility

It was Russell’s view that all of traditional mathematics about numbers as abstract objects could be represented in terms of the predicative propositional functions of his theory of ramified types. He could not justify such a view, however, without assuming an ‘axiom (schema) of reducibility’, which stipulates that every propositional function of whatever r-type is coextensive with a predicative propositional function (having arguments of the same r-type). In symbols:

$\begin{array}{r}\left(\mathrm{\forall }\varphi \right)\left(\mathrm{\exists }\psi \right)\left({x}_{1}\right)\dots \left({x}_{m}\right)\left[\varphi \left({x}_{1},\dots ,{x}_{m}\right) \\ \equiv \psi !\left({x}_{1},\dots ,{x}_{m}\right)\right],\end{array}$

where ‘φ’ and ‘ψ’ are variables for propositional functions of r-types (β1,…,βm)/n and (β1,…,βm)/1, respectively, and $\prime {x}_{1}\text{′},\dots ,\prime {x}_{m}\text{′}$ are variables of r-type β1,…,βm, respectively. (Russell used ‘ψ!’ to indicate that the propositional function represented by ‘ψ’ is predicative.) This axiom was criticized by a number of logicians (including L. Chwistek 1922; F. Ramsey 1931; W.V. Quine 1936) who argued that, on the assumption that type theory is an extensional system in which propositional functions of the same r-type are identical if they are coextensive (that is, true of all the same objects), the effect of the axiom of reducibility was to nullify the distinction between the different levels of propositional functions – in which case ramified type theory amounted to nothing more than a notationally complex version of simple type theory.

The extensionality assumption is dubious, however, if propositional functions are interpreted intensionally as properties and relations (as Russell originally intended). The point of the axiom of reducibility was not to identify properties and relations with their extensions, but to represent their extensions within the wider intensional framework, which is why Russell also called it ‘the axiom of classes’ (1910–13: vol. 1, 167). The effect of the axiom is that so-called ‘impredicative’ specifications of propositional functions – that is, specifications of functions in terms of a totality to which they belong – are ‘annulled in extensional but not in intensional matters’ (Church 1976: 758).

Ramsey emphasized a distinction between so-called logical and semantic antinomies, both of which the theory of ramified types was designed to avoid. Russell’s paradox, for example, is one of the logical antinomies, as is Georg Cantor’s paradox that there are classes (such as the universal class) larger than all other classes, even though, by a theorem of Cantor’s, there is a class larger than any given class. These are paradoxes that, without some restrictions such as those imposed in a theory of types, simple or ramified, might occur in any system rich enough to represent properties as objects having properties, or classes as members of classes. The semantic antinomies, on the other hand, assume special semantic notions, such as truth (as in the liar paradox of a sentence that says of itself that it is false, which if true is false, and if false is true), or definability (as in G.G. Berry’s paradox of ‘the least integer not nameable in fewer than nineteen syllables’, which is itself a name with just eighteen syllables), and other related notions of semantics. Ramsey (1931) thought of the semantic paradoxes as ‘epistemological’ in nature. (See Paradoxes of set and property.)