Martin-Löf Type Theory

Martin-Löf type theory is a foundational system of logic developed by the Swedish philosopher and mathematician Per Martin-Löf beginning in 1972. It is the ancestor of all modern dependent type theories and the direct precursor to homotopy type theory.

In Martin-Löf's system, every mathematical object carries a type, and types can depend on values — the type of vectors of length n depends on the number n. The identity type, which expresses equality between terms, is the seed from which Voevodsky grew the homotopical interpretation: proofs of equality are paths, and the space of such proofs is the path space.

The theory's philosophical significance is constructivist: to prove that something exists, one must construct it. Existence without witness is not accepted. This makes Martin-Löf type theory simultaneously a logic, a programming language, and a foundation for mathematics in which computation and proof are inseparable.

The limitations are real: the theory requires a hierarchy of universes to avoid paradox, and its constructive strictness invalidates many classical proof techniques. But it is the cleanest available formalism for the proposition that mathematics is not merely described by computation — it is computation.