History of type theory facts for kids
Type theory is a way of organizing ideas and symbols in mathematical logic and computer science. It was first created to avoid confusing problems, called paradoxes, that appeared in early systems of logic. Later, type theory became a whole group of formal systems. Some of these systems can even be used as a strong foundation for all of mathematics, instead of simpler ideas like naive set theory.
Type theory has been connected to formal mathematics for a long time, from the famous book Principia Mathematica to modern-day proof assistants, which are computer programs that help check mathematical proofs.
Early Ideas (1900–1927)
How Russell's Type Theory Started
In 1902, a mathematician named Bertrand Russell wrote a letter to Gottlob Frege, another important logician. Russell told Frege about a problem he found in Frege's work, which is now known as Russell's paradox. This paradox showed a flaw in how sets were defined.
Frege quickly replied, agreeing there was a problem. He suggested thinking about things in different "levels." He said that a "predicate" (which describes a property) usually needs an object to describe. It can't describe itself. For example, "is red" describes a ball, but "is red" can't be red itself.
Because of Russell's paradox, both Frege and Russell had to quickly change their books that were about to be printed. In his book The Principles of Mathematics (1903), Russell added a new section where he first introduced his "tentative" (meaning not yet final) theory of types. This problem bothered Russell for about five years.
Willard Quine, another philosopher, explained how Russell's theory of types came about. After thinking about giving up on the idea in 1905, Russell then suggested three different theories:
- the zigzag theory
- the theory of limitation of size
- the no-class theory (from 1905–1906)
After these, he went back to developing the theory of types starting in 1908.
Quine noted that Russell's idea of "apparent variable" (a symbol that stands for any value in a certain group) helped show the difference between "all" and "any." "All" refers to everything within a specific type, while "any" refers to an unspecified thing without worrying about its type.
The "Ramified" Theory of Types (1908)
Quine explained the ramified (meaning "branched" or "divided") theory of types. In this theory, the "type" of a function depends on two things: the types of its inputs and the types of any "apparent variables" it uses.
Stephen Kleene, in his 1952 book, described the ramified theory this way:
- Basic objects (like numbers or individual things) are "type 0."
- Properties of these objects (like "is even" for a number) are "type 1."
- Properties of properties (like "is a common property") are "type 2," and so on.
- This system doesn't allow properties that don't fit into these types.
To avoid problems where a definition refers to itself in a circular way (called impredicativity), types above type 0 were further divided into "orders." For example, properties defined without referring to a whole group of things were "order 0." Properties defined using a whole group of things of a certain order belonged to the next higher order.
However, this separation made it hard to define many common mathematical ideas. To fix this, Russell added his axiom of reducibility. This axiom said that any property of a higher order could be matched by a simpler property of the lowest order that applied to the exact same objects.
The Axiom of Reducibility and "Matrix"
The rules of the ramified theory were quite difficult to use. So, Russell also suggested his axiom of reducibility in his 1908 paper.
By 1910, Alfred North Whitehead and Russell, in their book Principia Mathematica, added to this axiom the idea of a matrix. A matrix is a complete description of a function. From a matrix, a function could be created by a process called "generalization." This process could also be reversed. This method helped avoid the problem of impredicativity.
Truth Tables
In 1921, Emil Post developed the idea of "truth functions" and their truth tables. These tables showed how the truth of a statement depends on the truth of its parts. This idea replaced Russell's complex "apparent versus real variables." Post's work focused on simple statements and how they combine.
Around the same time, Ludwig Wittgenstein developed similar ideas in his 1922 book Tractatus Logico-Philosophicus. He also proposed using truth tables. Wittgenstein believed that a statement cannot talk about itself. He thought this was the core idea of the theory of types. He also stated that a function cannot be its own input.
The idea of a matrix being like a truth table appeared in the work of Alfred Tarski as late as the 1940s and 1950s.
Russell's Doubts
In his 1920 book Introduction to Mathematical Philosophy, Russell dedicated a whole chapter to his concerns about the theory of types. He admitted that much of the theory was still unclear. However, he was sure that some form of type theory was necessary, even if the exact details were still being worked out.
Russell gives up the axiom of reducibility: In the second edition of Principia Mathematica (1927), Russell agreed with Wittgenstein's arguments. He stated that there was no need for the distinction between "real" and "apparent" variables. He now fully accepted the idea of a "matrix." He said that "a function can only appear in a matrix through its values." He also introduced a new, simpler idea of a "logical matrix," which contains no specific values.
Russell had mostly abandoned the axiom of reducibility. However, he noted that without it, he couldn't derive some important mathematical concepts. He hoped a new axiom would be discovered to replace it.
Theory of Simple Types
In the 1920s, Leon Chwistek and Frank P. Ramsey noticed something important. If you were willing to give up the strict "vicious circle principle" (which prevents definitions from referring to themselves), you could simplify the many levels of types in the "ramified theory of types."
This simpler logic is called the theory of simple types. Detailed versions of simple type theory were published in the late 1920s and early 1930s by R. Carnap, F. Ramsey, W.V.O. Quine, and A. Tarski. In 1940, Alonzo Church created a new version of it called simply typed lambda calculus. Kurt Gödel also studied it in 1944.
Modern Type Theory (1940s–Present)
Gödel's View (1944)
In his 1944 paper Russell's mathematical logic, Kurt Gödel defined the "theory of simple types." He said it's the idea that objects of thought (or symbols) are divided into types:
- Individuals (basic things)
- Properties of individuals
- Relationships between individuals
- Properties of such relationships, and so on.
Sentences like "a has the property φ" only make sense if a and φ are of types that fit together. This theory avoids paradoxes. Gödel concluded that the theory of simple types and axiomatic set theory could be used to build modern mathematics and avoid all known paradoxes.
Curry–Howard Correspondence (1934–1969)
The Curry–Howard correspondence is a fascinating idea that connects computer programs with mathematical proofs. It suggests that a mathematical proof can be seen as a computer program, and a mathematical formula can be seen as a type of data.
This idea started in 1934 with Haskell Curry and was fully developed in 1969 by William Alvin Howard. It showed how the "computational part" of many type theories was linked to how proofs are built in logic. Howard showed that a specific type of lambda calculus (a way of writing functions) matched a type of logic called natural deduction. This connection between types and logic led to a lot of new research.
de Bruijn's AUTOMATH (1967–2003)
Nicolaas Govert de Bruijn created a type theory called Automath. This was the mathematical basis for the Automath computer system. The main goal of Automath was to check if mathematical proofs were correct. The system grew and added new features as type theory itself developed.
Martin-Löf's Intuitionistic Type Theory (1971–1984)
Per Martin-Löf discovered a type theory that matched predicate logic. He did this by introducing dependent types, which are types that can depend on values. This theory became known as intuitionistic type theory or Martin-Löf type theory.
Martin-Löf's theory uses "inductive types" to represent data structures that can grow without limits, like natural numbers (0, 1, 2, 3...). Martin-Löf's way of presenting his theory, using rules of inference and judgments, became the standard for how future type theories were described.
Calculus of Constructions (1986)
Thierry Coquand and Gérard Huet created the Calculus of Constructions. This was another dependent type theory, specifically for functions. When combined with inductive types, it became known as "the Calculus of Inductive Constructions." This system is now the foundation for important proof assistants like Coq and Lean.
Barendregt's Lambda Cube (1991)
The lambda cube isn't a new type theory itself. Instead, it's a way to organize and categorize existing type theories. It's like a map that shows how different type theories are related. The "eight corners" of the cube represent various theories, from the simplest (simply typed lambda calculus) to the most complex (calculus of constructions).
Identity Proofs Are Not Unique (1994)
Before 1994, many type theorists thought that all ways of proving two things were the same (called "identity proofs") were basically identical. They thought that the only way to show something was equal to itself was through "reflexivity" (meaning it's equal to itself).
However, Martin Hofmann and Thomas Streicher showed that this wasn't necessarily true. In their paper, they showed that equality proofs could be thought of like elements in a mathematical group. In this model, "reflexivity" was like the zero element, "transitivity" (if A=B and B=C, then A=C) was like addition, and "symmetry" (if A=B, then B=A) was like negation.
This discovery opened up a whole new area of research called homotopy type theory. This field applies ideas from category theory (a branch of mathematics that studies abstract structures) to the concept of identity in type theory.
