The Origins of Type Theory
December 30, 2024Type theory began as an effort to resolve Russell’s Paradox, an issue discovered by Bertrand Russell. The precise events that mark the origin of type theory can be a matter of debate. Cantor, who developed set theory, independently discovered a similar paradox around the same time. In correspondence with Russell, Frege replied that in his conceptual notation, predicates do not take other predicates as arguments. Considering Russell’s approach that employs the hierarchical elements in the conceptual notation to resolve the paradox, one might argue that Frege’s predicate logic can be seen as an origin of type theory.
I’m interested in the origin of type theory and created slides to explain it. My interest in the origins of type theory stems from its interdisciplinary connections beyond computer science. While Cantor was a mathematician, the work of Frege and Russell is also significant in the philosophy of language. I am curious about how knowledge from related fields—such as mathematics, philosophy of language, and semiotics—can benefit programming and how this knowledge might be made appealing to software engineers.
To encourage engagement with these areas, I created slides focusing on the intersection of computer science with other disciplines, rather than on the exact historical details. The slide presentation, accessible above, is divided into three sections: the discovery of non-Euclidean geometry, naive set theory, and mathematical logic.
The core ideas are:- The discovery of non-Euclidean geometry led to a reevaluation of the foundational principles of mathematics, eventually leading to the definition of mathematical objects through the set theory developed by Cantor and Dedekind.
- Frege attempted to base mathematics on logic using his conceptual notation and set theory. However, his system could potentially derive Russell’s Paradox, indicating a need for reevaluation.
- Russell explored resolving the paradox by developing hierarchical relationships among objects, predicates, and predicates of predicates, documenting this in “Principia Mathematica.” Today, this hierarchical approach is recognized as the beginning of type theory.