nLab propositions as types

Redirected from "Curry-Howard correspondence".
Contents

Context

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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

semantics

Constructivism, Realizability, Computability

(0,1)(0,1)-Category theory

Contents

Idea

General idea

In type theory, the paradigm of propositions as types says that propositions and types are essentially the same. A proposition is identified with the type (collection) of all its proofs, and a type is identified with the proposition that it has a term (so that each of its terms is in turn a proof of the corresponding proposition).

… to show that a proposition is true in type theory corresponds to exhibiting an element [[ term ]] of the type corresponding to that proposition. We regard the elements of this type as evidence or witnesses that the proposition is true. (They are sometimes even called proofs… (from Homotopy Type Theory – Univalent Foundations of Mathematics, section 1.11)

Not all type theories follow this paradigm; among those that do, Martin-Löf type theories are the most famous. In its variant as homotopy type theory the paradigm is also central, but receives some refinements, see at propositions as some types.

Even when the paradigm is not adopted, however, there is still a close relationship between logical and type-theoretic operations, called the Curry–Howard isomorphism or (if it is not clear in which category this isomorphism is supposed to exist) the Curry–Howard correspondence. Or maybe better (Harper) the Brouwer-Heyting-Kolmogorov interpretation. This correspondence is most precise and well-developed for intuitionistic logic, but could also be developed for classical logic.

Accordingly, logical operations on propositions have immediate analogs on types. For instance logical and corresponds to forming the product type A×BA \times B (a proof of AA and a proof of BB), the universal quantifier corresponds to dependent product, the existential quantifier to dependent sum. In classical mathematics, the law of double negation corresponds to a global choice operator.

Furthermore, most structures traditionally involving predicates or relations are defined as type-valued type families. For instance, setoids or Bishop sets are usually defined to have a pseudo-equivalence relation in the propositions as types paradigm, rather than a equivalence relation as typical in the propositions as some types paradigm. However, in classical mathematics, the global choice operator representing the law of double negation in propositions as types implies that the boolean domain is the type of all propositions, so predicates or relations can simply be defined as functions into the boolean domain.

Propositions as some types

A related paradigm may be called propositions as some types, in which propositions are identified with particular types, but not all types are regarded as propositions. Generally, the propositions are the “types with at most one term”. This is the paradigm usually used in the internal logic of categories such as toposes, as well as in homotopy type theory. In this case, the type-theoretic operations on types either restrict to the propositions to give logical operations (for conjunction, implication, and the universal quantifier), or have to be “reflected” therein (for disjunction and the existential quantifier). The reflector operation is called a bracket type.

In homotopy type theory

We consider aspects of the interpretation of propositions as types in homotopy type theory, see (HoTT book, section 1.11).

In homotopy type theory where types may be thought of as homotopy types (∞-groupoids) (or rather geometric homotopy types (∞-stacks,(∞,1)-sheaves), more generally), we may think for AA any type of

  • the objects of AA are proofs of some proposition;

  • the morphisms of AA are equivalences between these proofs;

  • the 2-morphisms of AA are equivalences between these equivalences, and so on.

So in terms of the notion of n-connected and n-truncated objects in an (∞,1)-category we have

  • if AA is (-1)-connected then the corresponding proposition is true;

  • if AA is (-2)-truncated (a (-2)-groupoid) then the corresponding proposition is true by a unique proof which is uniquely equivalent to itself, etc.;

  • if AA is (-1)-truncated (a (-1)-groupoid) then the corresponding proposition may be true or false, but if it is true it is to by a unique proof as above;

  • if AA is 0-truncated then there may be more than one proof, but none equivalent to itself in an interesting way;

  • if AA is 1-truncated then there may be proofs of the corresponding proposition that are equivalent to themselves in interesting ways.

We would not say homotopy type theory has propositions as types in the same way that Martin–Löf type theory has; only the (1)(-1)-truncated types are propositions as such. That is, in HoTT we have propositions as some types. In this case the bracket types can be identified with a particular higher inductive type called isInhabisInhab.

Propositions as sets in set theory

There is an analogue of the “propositions as types” in set theory, called propositions as sets. Instead of working in the external logic, one interprets certain set-theoretic operations as representing the predicate logic:

Compare with propositions as subsingletons, which is the usual interpretation of the internal logic of a set theory via set-theoretic operations on sets.

References

General

Early account for intuitionistic type theory:

With a notion of propositional truncation:

Textbook accounts:

Exposition:

See also:

Discussion in view of homotopy type theory:

History

An influential original article was

  • William Howard, The formulae-as-types notion of construction. In J. Roger Seldin, Jonathan P.; Hindley, (ed.s), To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, 1980. original paper manuscript from 1969. (Cited

    on pages 53, 54, 100, and 430.) (pdf)

The origins of this manuscript and its publication are recounted in a 2014 email from Howard to Philip Wadler:

This influential note brought Dana Scott to write “Constructive Validity” (a precursor of type theory) and also strongly influenced Per Martin-Löf. Independently and at about the same time, the idea was also found by N.G. de Bruijn for the Automath system.

Dana Scott, William Howard, Per Martin-Löf, and William Tait were all involved in the late 60s and early 70s, mainly in Chicago.

  • William Tait, The completeness of intuitionistic first-order logic. Unpublished manuscript.

Also William Lawvere was there, lecturing on hyperdoctrines. Lawvere told Steve Awodey that the basic example of a morphism of hyperdoctrines from the proof-relevant one to the proof-irrelevant one was influenced by Kreisel, not Howard, who attended Lawvere’s Chicago lectures in the 60s. See pages 2 and 3 of

  • William Lawvere interviewed by Felice Cardone, The role of Cartesian closed categories in foundations, March 2000 (link)

But the story started earlier with what has been called the BHK interpretation of intuitionistic logic, highlighted for instance in (Troelstra 91), which identifies a proposition with the collection of its proofs. This view goes back to an observation of Kolmogorov that the formalisation of Brouwer’s ideas by Heyting in 1930 can be semantically interpreted as a calculus of ‘Aufgaben’ - problems (and solutions), reported in

A historical account is in the section on types in

  • Hindley J. Roger; Cardone Felice, History of Lambda-calculus and Combinatory Logic. Handbook of the History of Logic. Volume 5. Logic from Russell to Church (edited by D. Gabbay and J. Woods), Elsevier, 2009, pp. 723-817 (pdf, errata)

and in section 5 of

Last revised on February 23, 2024 at 22:42:36. See the history of this page for a list of all contributions to it.