Math 2.0

Mathematical logic and foundations Constructive mathematics Concept

Type theory

Builds on Russell's paradoxSet

Summary

A type theory is a formal system in which every term has a type. Its rules say which terms can be formed in which types. Russell introduced a theory of types to avoid Russell's paradox, by forbidding a collection to contain objects of its own level. Church's simple type theory of 1940 and Martin-Löf's intuitionistic type theory are the main later systems. Type theories serve as foundations of mathematics alternative to set theory, and as the basis of programming languages and proof assistants.

Reading path

To understand this page from the ground up, read these 19 pages in order. The foundations come first.

Show the path as a graph
Element, definition, no evidence levelElementdefinitionProposition, concept, no evidence levelPropositionconceptSet, concept, no evidence levelSetconceptSet, definition, no evidence levelSetdefinitionConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionTruth table, concept, no evidence levelTruth tableconceptModus ponens, concept, no evidence levelModus ponensconceptPropositional logic, concept, no evidence levelPropositional logicconceptMathematical proof, concept, no evidence levelMathematical proofconceptTautology, definition, no evidence levelTautologydefinitionLogical equivalence, definition, no evidence levelLogical equivalencedefinitionDouble negation law, statement, no evidence levelDouble negation lawstatementProof by contradiction, concept, no evidence levelProof by contradictionconceptRussell's paradox, statement, no evidence levelRussell's paradoxstatementType theory, concept, no evidence levelType theoryconcept
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Element definition
  2. Proposition concept
  3. Set concept
  4. Set definition
  5. Conjunction definition
  6. Disjunction definition
  7. Implication definition
  8. Negation definition
  9. Biconditional definition
  10. Truth table concept
  11. Modus ponens concept
  12. Propositional logic concept
  13. Mathematical proof concept
  14. Tautology definition
  15. Logical equivalence definition
  16. Double negation law statement
  17. Proof by contradiction concept
  18. Russell's paradox statement
  19. Type theory concept

Where this leads

4 pages build on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Type_theory
About this page
TagQ48KGV33AH
URIm2://Q48KGV33AH
Kindconcept
WritingW0 stub
MSC03B38, 03B16
UsesRussell's paradox, Set
Same as
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Definitions

Used by

Special cases