Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels





The interesting conception of the propositions-as-types principle is what I call Brouwer’s Dictum, which states that all of mathematics, including the concept of a proof, is to be derived from the concept of a construction, a computation classified by a type. In intuitionistic mathematics proofs are themselves “first-class” mathematical objects that inhabit types that may as well be identified with the proposition that they prove. Proving a proposition is no different than constructing a program of a type. In this sense logic is a branch of mathematics, the branch concerned with those constructions that are proofs. And mathematics is itself a branch of computer science, since according to Brouwer’s Dictum all of mathematics is to be based on the concept of computation. But notice as well that there are many more constructions than those that correspond to proofs. Numbers, for example, are perhaps the most basic ones, as would be any inductive or coinductive types, or even more exotic objects such as Brouwer’s own choice sequences. From this point of view the judgement tAt\in A stating that tt is a construction of type AA is of fundamental importance, since it encompasses not only the formation of “ordinary” mathematical constructions, but also those that are distinctively intuitionistic, namely mathematical proofs.

An often misunderstood point that must be clarified before we continue is that the concept of proof in intuitionism is not to be identified with the concept of a formal proof in a fixed formal system. What constitutes a proof of a proposition is a judgement, and there is no reason to suppose a priori that this judgement ought to be decidable. It should be possible to recognize a proof when we see one, but it is not required that we be able to rule out what is a proof in all cases. In contrast formal proofs are inductively defined and hence fully circumscribed, and we expect it to be decidable whether or not a purported formal proof is in fact a formal proof, that is whether it is well-formed according to the given inductively defined rules. But the upshot of Gödel’s theorem is that as soon as we fix the concept of formal proof, it is immediate that it is not an adequate conception of proof simpliciter, because there are propositions that are true, which is to say have a proof, but have no formal proof according to the given rules. The concept of truth, even in the intuitionistic setting, eludes formalization, and it will ever be thus. Putting all this another way, according to the intuitionistic viewpoint (and the mathematical practices that it codifies), there is no truth other than that given by proof. Yet the rules of proof cannot be given in decidable form without missing the point. (Harper)


In type theory

In type theory, a proposition is identitfied with the type of all its proofs (the propositions as types-aspect of computational trinitarianism). Here a proof consists of exhibiting a term of the corresponding type (showing that it is inhabited), hence a proof is a typing judgement for a term of the type representing the proposition.

See also proofs as programs.

Formal proofs

A formal proof is whatever is called a ‘proof’ in a formal system; a formal system for mathematics then gives methods for producing a proof in the above sense. Typically, a formal system is inductively defined, and hence its proofs are fully circumscribed; this is the case for deductive systems such as natural deduction, sequent calculus, and Hilbert systems?. Gödel's theorem suggests, however, that no such system can encapsulate all of mathematics.


A brief exposition of the notion of proof and formal proof in constructive mathematics/type theory is in

  • Robert Harper, Extensionality, Intensionality, and Brouwer’s Dictum, August 2012 (web)

  • Robert Harper, Constructive Mathematics is not Meta-Mathematics, July 2013 (web)

Further discussion of formal proofs includes the following

  • Thomas Hales, Formal proof (pdf)

  • John Harrison, Formal proof – theory and practice (pdf)

  • Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff, A formally verified proof of the prime number theorem (arXiv:cs/0509025)

  • Jeremy Avigad, John Harrison, Formally Verified Mathematics, Communications of the ACM, Vol. 57 No. 4, Pages 66-75 (web)

  • Jeremy Avigad, Formal verication, interactive theorem proving, and automated reasoning (2014) (pdf)

A discussion of the relation of mathematical proof to phenomenology of theories of physics is in

Texts on genuine proof theory include

Projects aiming to formalize parts of mathematics include

Revised on March 10, 2015 11:58:09 by Urs Schreiber (