Discussing "An Intuitionistic Theory of Types: Predicative Part"

(Link), although I downloaded a free copy here.

Author: Per Martin-Löf (University of Stockholm)

Reference: Per Martin-Löf, An Intuitionistic Theory of Types: Predicative Part, Editor(s): H.E. Rose, J.C. Shepherdson, Studies in Logic and the Foundations of Mathematics, Elsevier, Volume 80, 1975, Pages 73-118, https://doi.org/10.1016/S0049-237X(08)71945-1.

Why this paper? Cited by Encoding Dependently-Typed Constructions into Simple Type Theory and Normalization and coherence for ∞-type theories

After covering a few advanced and recent papers on type theory recently, this week we look at the first ever fully realised paper on type theory for formalised mathematics (previous work was either incomplete or suffered from errors). It is stated from the very first sentence that the work of this paper is “intended to be a full scale system for formalizing intuitionistic mathematics”. Charmingly, the paper ends with the self-effacing remark “What is doubtful at present is not whether computerization is possible, because we already know that, but rather whether these proof-theoretical computation procedures are at all useful in practice. So far, they do not seem to have found a single significant application”. Almost 50 years on, the vision of this paper has been thoroughly vindicated by the development of sophisticated proof assistants such as Coq and Lean capable of formalising complex mathematics such as proofs of the Four-Colour Theorem and the Odd Order Theorem.

The basic idea is to exploit the Curry-Howard isomorphism, only recently worked out in detail by William Howard (see Howard’s comments on his influence on Martin-Löf here), which identifies propositions with types and (intuitionistic) proofs with programs, to develop a (at this stage, paper-only) programming language for which which proof checking is type checking. Each logical symbol, familiar from any introductory logic course, becomes associated with a type former, as well as program formers which allow programs with that type to be introduced and eliminated (used). Less familiar to logicians, a universe (type of types) is essential to formalise many mathematical arguments, but care must be taken to avoid paradoxes that would crop up if the universe is taken to be a member of itself (very similar paradoxes must be avoided in set theory); this is the predicativity of the title. Crucially (and again, perhaps not so familiar from an introductory logical course) the decidability and other good properties of algorithms related to the type theory – reduction and type checking – is proved, paving the way for type theory to jump off the page and into real implementation.

This paper is quite a readable introduction to this brand new area, as Martin-Löf does not assume familiarity with the underlying idea of performing mathematics inside type theory, as a more recent paper might, but rather must justify his approach. The paper is full of pithy quotes (some original, some adapted from other sources) to motivate the work, such as “A proposition is defined by prescribing how we are allowed to prove it” and, justifying the importance of type checking being decidable, “we recognize a proof when we see one”.