Types, Theory of

Types, Theory of


an important chemical theory of the mid-19th century. In the years 1839 and 1840, J. B. Dumas proposed that chemical compounds be regarded as products of the substitution of single elements or radicals for others in a few “typical” compounds (older type theory). In 1853, C. Gerhardt developed his own type theory, which he used for classifying organic compounds. Gerhardt believed that complicated organic compounds could be derived from the following four basic types of substances:

The substitution of other atoms or radicals, called residues by Gerhardt, for the H atoms in these formulas yielded the formulas for the organic compounds of all the classes known in the mid-19th century. For example, the hydrogen type included hydrocarbons, organometallic compounds, aldehydes, and ketones; the water type, alcohols, acids, and ethers; the hydrogen chloride type, monohalogen derivatives of hydrocarbons; and the ammonia type, amines, amides, imides, arsines, and phosphines. In 1857, hydrocarbons were grouped under the methane type, as proposed by F. A. Kekulé.

The theory of types furthered the development of organic chemistry, in particular, the classification of organic compounds. However, the underlying concept—the placement of carbon compounds in formulas for the simplest inorganic compounds— was erroneous. Before long, it became necessary to introduce multiple types (double, triple) and conjugated types (comprising two or more simple types), and the possibility arose of classifying compounds of the same class as different types, for example, classifying aldehydes as both hydrogen and water types. In addition, formulas derived from the theory of types represented not the actual structure of compounds but only the similarity between certain of the compounds’ reactions and the reactions of simpler, better-known substances. Therefore, in the 1860’s, the theory of types gradually gave way to the classical theory of chemical structure, developed by A. M. Butlerov.


Bykov, G. V. Istoriia klassicheskoi teorii khimicheskogo stroeniia. Moscow, 1960. Pages 17–23.


Types, Theory of


in logic, a system of the extended predicate calculus or axiomatic set theory that includes variables of different “types” (sorts, levels, orders).

In the system of Russell and Whitehead, the formal objects of the theory are divided into types. The lowest type consists of all individuals, the next type is composed of all predicates, the succeeding type is composed of all predicates of predicates, and so on. Thus, objects of type n are predicates of objects of type n – 1 and, possibly, of lower types. In the alternative formulation of the theory of types as axiomatic set theory, objects of type n are sets of objects of type n – 1 and, possibly, of lower types.

Accordingly, the axiom of comprehension, or axiom of abstraction, whose unrestricted use in the extended predicate calculus and in set theory leads to paradoxes, is now stated differently: “For every predicate formula with free variable x that does not contain objects of type higher than n – 1, there exists a predicate of type n that is true for those, and only those, values of x for which the original formula is true.” The axiom may also be stated as follows: “For any property whose statement employs sets of type not higher than n – 1, there exists a set of type n consisting of those, and only those, objects that possess this property.” The italicized portions of these two formulations are the additions to the usual form of the axiom of comprehension that distinguish the type-theoretic form of the axiom from the usual form and prevent the occurrence in type theory of the paradoxes that appear in naive set theory. An example is Russell’s paradox of the set of all sets that do not contain themselves as elements.

As careful analysis has shown, the mathematics constructed on the basis of the theory of types is substantially weaker than ordinary classical mathematics. For this reason, Russell introduced into his system the axiom of reducibility, which, roughly speaking, postulates for every set (predicate) of type n the existence of an equivalent set of type 1. As Russell himself showed, however, even this axiom did not make possible the construction of mathematics on a purely logical foundation. Consequently, logicism’s attempt to derive all of mathematics from pure logic proved to be unrealizable.


Hilbert, D., and W. Ackermann. Osnovy teoreticheskoi logiki. Moscow, 1947. Chapter 4 and Appendix 1. (Translated from German.)
Wang, H., and R. McNaughton. Aksiomaticheskie sistemy teorii mnozhestv. Moscow, 1963. Chapters 1–2, 5–6. (Translated from French.)
Fraenkel, A., and Y. Bar-Hillel. Osnovaniia teorii mnozhestv. Moscow, 1966. Chapters 1, 3. (Contains bibliography.) (Translated from English.)
Andrews, P. B. A Transfinite Type Theory With Type Variables. Amsterdam, 1965.