Olga Antonova. Philosophy of Kant and Type theory

Posted by admin | On 18 August,2014 | In Publications

The purpose of this article is to trace the genesis of the principal categories of modern mathematics such as set, class and type. These categories are very important for the development of mathematics not only because they lie at the basis of the principal mathematical theories (Cantor’s set theory, axiomatic set theory, type theory), but also because they help to consider the principal features of the process of construction of mathematical objects.

In this article we address the following principal periods in mathematics:

Cantor and his theory of sets.
Hilbert’s criticism of the idea of set and his axiomatic method
The concept of set in Axiomatic set theory of Zermelo and Fraenkel.
The distinction between set and class in the Axiomatic set theory of von Neumann-Bernays-Gödel
The idea of type.

Before considering these principal periods in mathematics, it is necessary to pay attention to some historical and philosophical roots of the genesis of the modern mathematical categories.

Kant’s philosophical ideas concerning the construction of mathematical objects determined for the most part further development of mathematics and, especially, the researches in the foundations of mathematics. Supposing that mathematical knowledge is formed by construction of its objects, Kant distinguished the following kinds of mathematical reasoning, that is, definitions, axioms and demonstrations.

Kant writes “…mathematical knowledge is the knowledge gained by reason from the construction of concepts. To construct a concept means to exhibit a priori the intuition which corresponds to the concept. …. Thus I construct a triangle by representing the object which corresponds to this concept either by imagination alone, in pure intuition, or in accordance therewith also on paper, in empirical intuition — in both cases completely a priori, without having borrowed the pattern from any experience” [4, p. 577].

For Kant, the construction of mathematical objects is defined by the following features:

To construct a mathematical concept means to show an object that is appropriate to this concept.
The construction of a mathematical concept lies outside of experience and, consequently, is a priori.

Thereby, according to Kant, the construction of a concept is identified with the definition of a mathematical object, and from here, the existence of mathematical objects is established by the definitions and, consequently, by construction.

Having in mind that Kant suggested this idea of construction of mathematical objects, I try to show that

The philosophical ideas of Kant concerning the construction of mathematical objects encouraged the forming and the development of the mathematical ideas of set (Theory of Cantor) and type (Type Theory).
Considering the set as entity, theory of Cantor is close to the idea of construction of a mathematical object in accordance with the concept of the object. The notion of set in modern set theory is more formal than Cantor’s notion, consequently, may be seen as opposite to Kant’s ideas.
The modern notion of type depends on the principles of construction of the elements of this type. The analysis of the differences between the modern notion of type and Church’s notion of type shows that the modern notion of type is closer to Kant’s idea about the constructive character of the formation of mathematical objects.

1. Cantor and his Theory of Sets

The concept of set became a basic category of mathematics due to the set theory of Cantor. Cantor supposes that the concept of set lies at the basis of mathematics. Cantor tried to give such definition of set that would not lead to the contradictions. Although the first contradictory notion in set theory was discovered around 1900 by Russell and Zermelo, that is «the set of all sets that are not members of themselves», already in 1899 Cantor had thought about a possibility to obtain a paradox in his set theory.

Probably to avoid this possibility of contradiction, when Cantor defines the concept of set he distinguishes two kinds of set: consistent and inconsistent multiplicities. But Cantor was not the first who considered this idea. In 1890 Schröder already introduced the distinction between consistent and inconsistent multiplicities. Schröder defines a consistent multiplicity as a multiplicity whose elements are compatible with each other, and inconsistent when the elements are not compatible. The following fact is very interesting: Schröder introduced this distinction independently of the paradoxes.

Cantor makes a distinction between the notion of multiplicity and the notion of set. For Cantor not every multiplicity can be considered as a set. A set is a multiplicity that can be considered as a unity.

Cantor writes about multiplicities that lead to contradiction. “For a multiplicity can be such that the assumption that all its elements “are together” leads to a contradiction, so that it is impossible to conceive the multiplicity as a unity, as “one finished thing” [3, p. 114].

In difference from this notion of multiplicity, Cantor defines set as “…the totality of the elements of a multiplicity can be thought of without contradiction as “being together”, so that they can be gathered together into “one thing”, I call it a consistent multiplicity or a “set” [3, p. 114].

Thereby for Cantor every mathematical object that unites the distinct objects (elements) into certain totality is a set. One may point out the following features of Cantor’s set theory:

Mathematical objects (entities) that possess a definite property constitute a set. A set is determined and defined by the property. Mathematical objects are its elements.
Since a set is a mathematical entity, it may be considered as an element of another set.
If two sets contain the same elements, they are identical, consequently, a set is determined by its elements.

Cantor’s idea of set as a totality of distinct elements leads to the existence of many different sets. In difference of Cantor, Frege considered a universal domain of all objects. Frege’s notion of concept as a thought object is close to Dedekind’s notion of a system.

Dedekind defines the notion of a number sequence as a system of individuals, where individuals (elements) are thought objects.

He writes: “The number sequence N is a system of individuals, or elements, called numbers” [3, p. 100].

Thereby, Frege’s notion of concept which is logical may be compared with the idea of system in Dedekind’s number theory, whereas Cantor’s notion of set that is distinct from Frege’s concept and Dedekind’s system leads us to the notion of type in Type Theory.

2. Hilbert’s Criticism of the Idea of Set and his Axiomatic Method

In the famous work “Foundations of logic and arithmetic” Hilbert (1904) considered different theories concerning the notions of number and set. He criticized the conceptions of Frege, Dedekind and Cantor. For him, their conceptions do not give a sufficiently exact notion of set to avoid the paradoxes and contradictions arising in the foundations of mathematics. Obviously, the criterion of distinction between multiplicity and unity (set) is very fuzzy and not sufficient.

Hilbert pointed out that the Frege’s concept does not impose the definite restrictions to the notion of “every object” and thus it may lead to the set-theoretic paradoxes that can be derived from the idea of the set of all sets.

Hilbert asserts that Cantor’s notion of set is insufficient. He says that Cantor’s criterion for the distinction is imprecise, because it can consider a multiplicity as a set without contradiction, as one object. For Cantor a multiplicity is a set whenever it is an element of another multiplicity.

Hilbert writes: “…he does not provide a precise criterion for this distinction, I must characterize his conception on this point as one that still leaves latitude for subjective judgment and therefore affords no objective certainty” [3, p. 131].

Hilbert tried to find objective basis for this distinction. To this purpose Hilbert suggests to consider all mathematical objects as thought-objects and to distribute primitive objects or their combinations into two classes, that is, the class of entities and the class of non-entities. The axioms play the role of prescriptions to distinguish the entities and non-entities.

Thus Hilbert proposes to consider the set as “A set is generally defined as a thought-object m, and the combinations mx are called the elements of the set m, so that — contrary to the usual conception — the notion of element of a set appears only as a subsequent product of the notion of set itself” [3, p. 135—136].

In distinction of the notion of Frege’s concept and Cantor’s set, Hilbert wants to substantiate this notion objectively, that is, on the one hand to restrict the notion of set and element of a set (element — subsequent object of set), and on the other hand, to consider the axioms as non-subjective but rather objective base for the notions of set and element.

The another attempt to formalize the notion of set by axioms was undertaken in axiomatic set theory of Zermelo and Fraenkel.

3. The Concept of set in Axiomatic Set Theory of Zermelo and Fraenkel

The result of the work of Zermelo in 1908 and Fraenkel in 1922 was axiomatic set theory. Zermelo’s system was free from known paradoxes (Burali-Forti, Russell paradoxes). For example the set of all sets that do not contain themselves as elements does not exist in the system.

Zermelo-Fraenkel Axiomatic Set Theory is based on the principles

the primitive notion of set
the suggestion that all mathematical objects are sets
the function of axioms is to delimit how sets are formed.

Zermelo-Fraenkel Axiomatic Set Theory cannot be axiomatized by a finite set of axioms. A set is defined in this system as “…we finally decide to use the term “set” from now on not just for a member of the counterdomain of $\in$ , but rather for a member of its field, i.e., for any object belonging to the universe of discourse” [2, p. 121].

Zermelo-Fraenkel Axiomatic Set Theory refused to use the concept of Cantor’s set. Instead it uses the axiomatic method by which the concept of set is postulated but this concept itself is left unexplained. These sets are for the most part arbitrary and do not have any specific properties for the definition of their elements. Therefore the sets are defined as objects satisfying the axioms. One may find out about sets no more than that is established in the axioms. The axioms formulate the concept of set in such a way that all theorems of Cantor’s set theory may be derived from them without antinomies. Avoiding the concept of Cantor’s set Zermelo-Fraenkel Axiomatic Set Theory wants to specify the role of axioms in the definition of set. The notion of set in Cantor’s Set Theory has “substantial” character. Thus Cantor’s notion of set is distinguished from the notion of set of modern Set Theory, which has only “formal” character.

4. The Distinction between Set and Class in the Axiomatic Set Theory of von Neumann-Bernays-Gödel

The distinction between consistent and inconsistent multiplicities of Cantor prefigures the distinction between sets and classes, introduced by von Neumann in 1925. Prior to von Neumann, König in 1905 distinguished two kinds of collections (set and class) in order to avoid the paradoxes. König’s notion of set as a totality is close to Cantor’s notion.

Concerning set, König writes: “Through the stipulation that a1, a2….are to be replaced by definite positive integers, it becomes a “definite” sequence, an element of the continuum, which cannot become an object of our thought without being conceptually distinct from any other element” [3, p. 148].

In the distinction of the continuum, the second number class Z ( $\aleph$ 0) is considered by König as a class or “as a set in the process of becoming”. For König the notion of a class is more of a collective notion. The properties that determinate the elements of a class are abstractions “at best a means of distinguishing between objects belonging and objects not belonging to the class” [3, p. 148]. Also König notes that they are not rules “according to which every element of Z( $\aleph$ 0) can be formed” [3, p. 148].

The distinction between set and class plays important role for set theory since it leads to the resolution of the paradoxes, such as “the set of all sets”. Von Neumann introduced his axiomatic set theory in 1925. This axiomatic set theory was modified by Paul Bernays in 1937, and finally, Kurt Gödel simplified it in 1940. The basic principle and fundamental innovation of this system is the introduction of two kinds of collections: sets and classes.

Fraenkel A. A., Bar-Hillel Y. write “..we have seen that the axiom systems of von Neumann, Bernays, and Gödel are superior to the system Z in many respects, an important feature being that the concept of set (class) is explicitly conceived as comprehensive as possible in view of the antinomies” [2, p. 121—122].

A set is a class, but there are classes (ultimate classes) that are not sets: an ultimate class is not an element of any other class. The notion of class allows us to use the notion of the class of all sets, because it can be very large. However, there are some formal limitations in using the notion of the class of all classes or the set of all sets. The membership relation a є s is only defined if a is a set and s is a set or a class. There is a certain parallelism of the concepts of set and class in the theory of von Neumann-Bernays-Gödel and the distinction between consistent and inconsistent multiplicities in Cantor’s set theory. On the basis of the principle of abstraction, classes may be constructed from any statement of this theory with the membership relation. Sets and classes are characterized by axioms. But other notions such as subclasses, equivalence, are introduced by definitions.

The axiomatic set theory of von Neumann-Bernays-Gödel and the set theory of Zermelo-Fraenkel are equivalent set theories, since any theorem about sets which can be proved in one theory can be proved in the other.

In contrast to Zermelo-Fraenkel Axiomatic Set Theory, von Neumann—Bernays—Gödel Set Theory can be axiomatized by a finite set of axioms. Von Neumann points out, that classes can be regarded as Zermelo’s “definite conditions”. The definite conditions may be replaced by classes, if set is distinguished from class. The existence of classes is characterized by axioms, consequently, there is a finite number of axioms. No axiom schema is required. Russell’s and Burali-Forti’s paradoxes cannot be reproduced in von Neumann’s system, because a universal class and a class of all ordinals are both ultimate.

The distinction between class and set plays an important role not only for avoiding paradoxes in set theory, but also for other mathematical theories, for example, category theory. So if we relate large categories to ultimate classes and small categories to sets, then we can get the concept of large category of all small categories avoiding the paradoxes.

5. The Idea of Type

The concept of type in mathematics was introduced by Russell to avoid the paradox which was discovered in Frege’s set theory. The notion of Type in the canonical Type Theory of Russell and Church has roots in the Aristotle’s principle of limitation of subject domain. Aristotle rejected the existence of the universal domain of objects and, thereby, distinguishes the existence of domain of individual objects and domain of classes of objects. This distinction is based on the Aristotle’s idea of two substances. Concerning the primary substance, Aristotle writes: «Every substance seems to signify a certain “this”. As regards the primary substances, it is indisputably true that each of them signifies a certain “this”; for the thing revealed is individual and numerically one” [6, v. 1, p. 6].

Secondary substance does not consist of individuals, but is independent domain that contains classes of individual objects. Aristotle writes: “But as regards the secondary substances, though it appears from the form of the name — when one speaks of man or animal — that a secondary substance likewise signifies a certain “this”, this is not really true; rather, is signifies a certain qualification — for the subject is not, as the primary substance is, one, but man and animal are said of many things” [6, v. 1, p. 6].

The principal idea of theory of types is to create a hierarchy of types, such that each mathematical entity will be of a certain type. Objects that belong to a given type are based on the objects of preceding types. This hierarchy of types prevents circles in the domain of objects.

Russell writes: “… we explained a doctrine of types of variables, proceeding upon the principle that any expression which refers to all of some type must, if it denotes anything, denote something of a higher type than that to all of which it refers…..Thus any expression containing an apparent variable is of higher type than that variable” [3, p. 182].

Alonzo Church developed his Theory of Types to avoid the paradox that is called the Kleene-Rosser paradox. In Church’s type theory the expressions or formulas are distributed into types, and the types of expressions restrict the ways in which they can be combined. A. Church writes: “ The class of type symbols is described by the rules that i and o are each type symbols and that if $\alpha$ and $\beta$ are type symbols then ( $\alpha\beta$ ) is a type symbol: it is the least class of symbols which contains the symbols i and o and is closed under the operation of forming the symbol ( $\alpha\beta$ ) from the symbols $\alpha$ and $\beta$ ” [1, p. 57].

The notion of type in the canonical Type Theory of Russell and Church is very close to the notion of set as unity in Cantor’s Set Theory. Thus this notion is the generalization Cantor’s notion of set. Type Theories of Russell and Church were only a reaction against the paradoxes. The question why a collection of elements may create a new entity didn’t bother them much. Their approach was to consider formal restrictions on formation of new sets to avoid paradoxes. The notion of set (Type) has more restricted character in the modern Type Theory than in Cantor’s Set Theory and Type Theory of Russell and Church.

One principal feature of Intuitionistic type theory is certain analogy between propositions and types. A proposition corresponds to the type of its proofs. Another innovation was the introduction of inductive and coinductive types with more restrictive rules of construction than for sets in set theories mentioned above. One may observe that the role of types in Intuitionistic Type Theory is similar to the role of sets in set theory but it establishes more strict rules for constructon of types and definition of their elements. Therefore functions that are definable in Type Theory are always constructive and computable.

Thereby we arrive at the following conclusions:

Cantor’s consideration of a set of elements as entity that is formed by the set-forming operation, corresponds to Kant’s idea of construction of a mathematical object in accordance with the concept of the object. In contradistinction to Cantor’s notion of set, the notion of set in modern set theory is not substantive but more formal and meaningless notion. Consequently, modern notion of set may be seen as opposite to Kant’s idea of the existence of mathematical object and Cantor’s notion of set as entity, whereas the notion of type (especially, modern notion of type) that is close to Cantor’s notion of set moves us nearer to Kant’s idea about the constructive character of the formation of mathematical objects.
Cantor’s distinction between the consistent and inconsistent multiplicities became the causes of the distinction between sets and classes in the Axiomatic set theory of von Neumann-Bernays-Gödel, sets and types in Intuitionistic Type Theory.
Frege’s concept may be compared with the idea of system in Dedekind’s number theory, whereas Cantor’s notion of set, which is distinct from Frege’s concept and Dedekind’s system, leads us to the notion of type (set) in Type Theory.
In distinction from Cantor’s notion of set and Frege’s concept, Hilbert wanted to formalize this notion objectively, that is, on the one hand to restrict the notion of set and element of a set (element —subsequent element of set), and on the other hand, to consider the axioms as a non-subjective but rather objective base for the notions of set and element.
The Hilbert’s conception of set and axiomatic set theory of Zermelo —Fraenkel formalise the notion of set by axioms. Therefore the notion of set «as such» becomes formal and is defined as an object from axioms. The axioms formulate the concept of set in such a way that all theorems of Cantor’s set theory may be derived from them without antinomies. Avoiding Cantor’s concept of set, the Zermelo-Fraenkel Axiomatic Set Theory wants to specify the role of axioms in the definition of set.
König distinguished two kinds of collections (set and class) in order to avoid the paradoxes. König’s notion of set as a totality (Inbegriff) corresponds to Cantor’s notion of set. For König the notion of class is close to the collective notion that may be compared with Cantor’s notion of inconsistent multiplicity.
The distinction between class and set introduced in von Neumann-Bernays —Gödel axiomatic theory is in some way a reaction against the formal notion of set and return to Cantor’s notion of set. The concept of set corresponds to the concept of set in Cantor’s set theory. On the basis of the principle of abstraction, classes may be constructed from any statement of this theory with the membership relation. Sets and classes are characterized by axioms.
The notion of Type in Type Theory of Russell and Church determines the formation of entities built of objects in the domain. So the types play the role of definitions and classifications of objects, that is, they set and restrict different objects in the domain. In distinction from the axiomatic set theory, Type Theory continues to consider type (set) as an object that is determined by some principle of form. Cf. “propositions as types”, inductive and coinductive types in Intuitionistic Type Theory.

Bibliography

1. Church A. A Formulation of the Simple Theory of Types // Journal of Symbolic Logic. 1940. № 5. P. 56—68.

2. Fraenkel A. A., Bar-Hillel Y. Foundations of Set Theory. Amsterdam, 1958.

3. Heijenoort J. From Frege to Gödel: a source book in Mathematical logic, 1879—1931. Amsterdam, 1967.

4. Kant’s Critique of Pure Reason. Translated by N. K. Smith. New York, 1968.

5. Martin-Löf P. Analytic and synthetic judgments in Type Theory. Florence, 1992.

6. The complete works of Aristotle. V.1. Princeton, 1984.

This article was firstly published in collected articles «Klassische Vernunft und Herausforderungen der modernen Zivilisation» (2010): Antonova, Olga. Philosophy of Kant and Type theory// 10. Internationale Kant Konferenz. Klassische Vernunft und die Herausforderungen der modernen Zivilisation: Materialien der internationalen Konferenz: in 2 Bd. Hrsg. W.N. Brjuschinkin. – Kaliningrad: Verlag der Immanuel Kant Universität Kaliningrad, 2010. Band. 1, S.. 269 – 279.

Related Posts