As already mentioned, the principle that

اقتباس :

a proposition is the type of its proofs.

is fundamental to intuitionistic type theory. This principle is also known as the Curry-Howard correspondence or even Curry-Howard isomorphism. Curry discovered a correspondence between the implicational fragment of intuitionistic logic and the simply typed lambda-calculus. Howard extended this correspondence to first-order predicate logic. In intuitionistic type theory this correspondence becomes an identification of proposition and types, which has been extended to include quantification over higher types and more.

2.3 Sets of Proof-Objects

So what are these proof-objects like? They should not be thought of as logical derivations, but rather as some (structured) symbolic evidence that something is true. Another term for such evidence is “truth-maker”.
It is instructive, as a somewhat crude first approximation, to replace types by ordinary sets in this correspondence. Define a set [ltr]E[size=13]m,nEm,n[/ltr], depending on [ltr]m,n∈Nm,n∈N[/ltr], by:[/size]
Then [ltr]E[size=13]m,nEm,n[/ltr] is nonempty exactly when [ltr]m=nm=n[/ltr]. The set [ltr]Em,nEm,n[/ltr] corresponds to the proposition [ltr]m=nm=n[/ltr], and the number [ltr]00[/ltr] is a proof-object (truth-maker) inhabiting the sets [ltr]Em,mEm,m[/ltr].[/size]
Consider the proposition that [ltr]mm[/ltr] is an even number expressed as the formula [ltr]∃n∈N.m=2n∃n∈N.m=2n[/ltr]. We can build a set of proof-objects corresponding to this formula by using the general set-theoretic sum operation. Suppose that [ltr]A[size=13]nAn[/ltr] ([ltr]n∈Nn∈N[/ltr]) is a family of sets. Then its disjoint sum is given by the set of pairs[/size]
If we apply this construction to the family [ltr]A[size=13]n=Em,2nAn=Em,2n[/ltr] we see that [ltr](Σn∈N)Em,2n(Σn∈N)Em,2n[/ltr] is nonempty exactly when there is an [ltr]n∈Nn∈N[/ltr] with [ltr]m=2nm=2n[/ltr]. Using the general set-theoretic product operation [ltr](Πn∈N)An(Πn∈N)An[/ltr] we can similarly obtain a set corresponding to a universally quantified proposition.[/size]

2.4 Dependent Types

In intuitionistic type theory there are primitive type formers [ltr]ΣΣ[/ltr] and [ltr]ΠΠ[/ltr] for general sums and products, and [ltr]II[/ltr] for identity types, analogous to the set-theoretic constructions described above. The identity type [ltr]I(N,m,n)I(N,m,n)[/ltr] corresponding to the set [ltr]E[size=13]m,nEm,n[/ltr] is an example of a dependent typesince it depends on [ltr]mm[/ltr] and [ltr]nn[/ltr]. It is also called an indexed family of types since it is a family of types indexed by [ltr]mm[/ltr] and [ltr]nn[/ltr]. Similarly, we can form the general disjoint sum [ltr]Σx:A.BΣx:A.B[/ltr] and the general cartesian product [ltr]Πx:A.BΠx:A.B[/ltr] of such a family of types [ltr]BB[/ltr] indexed by [ltr]x:Ax:A[/ltr], corresponding to the set theoretic sum and product operations above.[/size]
Dependent types can also be defined by primitive recursion. An example is the type of [ltr]nn[/ltr]-tuples [ltr]A[size=13]nAn[/ltr] of elements of type [ltr]AA[/ltr] and indexed by [ltr]n:Nn:N[/ltr] defined by the equations[/size]
where [ltr]11[/ltr] is a one element type and [ltr]××[/ltr] denotes the cartesian product of two types. We note that dependent types introduce computation in types: the defining rules above are computation rules. For example, the result of computing [ltr]A[size=13]3A3[/ltr] is [ltr]A×(A×(A×1))A×(A×(A×1))[/ltr].[/size]

2.4 Propositions as Types in Intuitionistic Type Theory

With propositions as types, predicates become dependent types. For example, the predicate [ltr]Prime(x)Prime(x)[/ltr] becomes the type of proofs that [ltr]xx[/ltr] is prime. This type depends on [ltr]xx[/ltr]. Similarly, [ltr]xxxx[/ltr] is less than [ltr]yy[/ltr].
According to the Curry-Howard interpretation of propositions as types
where [ltr]Σx:A.BΣx:A.B[/ltr] is the disjoint sum of the [ltr]AA[/ltr]-indexed family of types [ltr]BB[/ltr] and [ltr]Πx:A.BΠx:A.B[/ltr] is its cartesian product. The canonical elements of [ltr]Σx:A.BΣx:A.B[/ltr] are pairs [ltr](a,b)(a,b)[/ltr] such that [ltr]a:Aa:A[/ltr] and [ltr]b:B[x:=a]b:B[x:=a][/ltr] (the type obtained by substituting all free occurrences of [ltr]xx[/ltr] in [ltr]BB[/ltr] by [ltr]aa[/ltr]). The elements of [ltr]Πx:A.BΠx:A.B[/ltr] are (computable) functions [ltr]ff[/ltr] such that [ltr]fa:B[x:=a]fa:B[x:=a][/ltr], whenever [ltr]a:Aa:A[/ltr].
For example, consider the proposition
expressing that there are arbitrarily large primes. Under the Curry-Howard interpretation this becomes the type [ltr]Πm:N.Σn:N.mΠm:N.Σn:N.mmm[/ltr] to a triple [ltr](n,(p,q))(n,(p,q))[/ltr], where [ltr]nn[/ltr] is a number, [ltr]pp[/ltr] is a proof that [ltr]mmqq[/ltr] is a proof that [ltr]nn[/ltr] is prime. This is the proofs as programs principle: a constructive proof that there are arbitrarily large primes becomes a program which given any number produces a larger prime together with proofs that it indeed is larger and indeed is prime.
Note that the proof which derives a contradiction from the assumption that there is a largest prime is not constructive, since it does not explicitly give a way to compute an even larger prime. To turn this proof into a constructive one we have to show explicitly how to construct the larger prime. (Since proposition ([ltr]11[/ltr]) above is a [ltr]Π[size=13]02Π20[/ltr]-formula we can for example use Friedman’s A-translation to turn such a proof in classical arithmetic into a proof in intuitionistic arithmetic and thus into a proof in intuitionistic type theory.)[/size]

3. Basic Intuitionistic Type Theory

We now present a core version of intuitionistic type theory, closely related to the first version of the theory presented by Martin-Löf in 1972 (Martin-Löf 1998 [1972]). In addition to the type formers needed for the Curry-Howard interpretation of typed intuitionistic predicate logic listed above, we have two types: the type [ltr]NN[/ltr] of natural numbers and the type [ltr]UU[/ltr] of small types.
The resulting theory can be shown to contain intuitionistic number theory [ltr]HAHA[/ltr] (Heyting arithmetic), Gödel’s System [ltr]TT[/ltr] of primitive recursive functions of higher type, and the theory [ltr]HA[size=13]ωHAω[/ltr] of Heyting arithmetic of higher type.[/size]
This core intuitionistic type theory is not only the original one, but perhaps the minimal version which exhibits the essential features of the theory. Later extensions with primitive identity types, well-founded tree types, universe hierarchies, and general notions of inductive and inductive-recursive definitions have increased the proof-theoretic strength of the theory and also made it more convenient for programming and formalization of mathematics. For example, with the addition of well-founded trees we can interpret the Constructive Zermelo-Fraenkel Set Theory [ltr]CZFCZF[/ltr] of Aczel (1978 [1977]). However, we will wait until the next section to describe those extensions.

3.1 Judgments

In Martin-Löf (1996) a general philosophy of logic is presented where the traditional notion of judgment is expanded and given a central position. A judgment is no longer just an affirmation or denial of a proposition, but a general act of knowledge. When reasoning mathematically we make judgments about mathematical objects. One form of judgment is to state that some mathematical statement is true. Another form of judgment is to state that something is a mathematical object, for example a set. The logical rules give methods for producing correct judgments from earlier judgments. The judgments obtained by such rules can be presented in tree form
or in sequential form

• (1)[ltr]J1 axiomJ1 axiom[/ltr]
  
  
• (2)[ltr]J2 axiomJ2 axiom[/ltr]
  
  
• (3)[ltr]J3 by rule r1 from (1) and (2)J3 by rule r1 from (1) and (2)[/ltr]
  
  
• (4)[ltr]J4 axiomJ4 axiom[/ltr]
  
  
• (5)[ltr]J5 by rule r2 from (4)J5 by rule r2 from (4)[/ltr]
  
  
• (6)[ltr]J6 axiomJ6 axiom[/ltr]
  
  
• (7)[ltr]J7 by rule r3 from(5) and (6)J7 by rule r3 from(5) and (6)[/ltr]
  
  
• (8)[ltr]J8 by rule r4 from (3) and (7)J8 by rule r4 from (3) and (7)[/ltr]
  
  

The latter form is common in mathematical arguments. Such a sequence or tree formed by logical rules from axioms is a derivation or demonstration of a judgment.
First-order reasoning may be presented using a single kind of judgment:

اقتباس :

the proposition [ltr][size=18]BB[/ltr] is true under the hypothesis that the propositions [ltr]A[size=13]1,…,AnA1,…,An[/ltr][/size] are all true.[/size]

We write this hypothetical judgment as a so-called Gentzen sequent
Note that this is a single judgment that should not be confused with the derivation of the judgment[ltr]⊢B⊢B[/ltr] from the judgments [ltr]⊢A[size=13]1,…,⊢An⊢A1,…,⊢An[/ltr]. When [ltr]n=0n=0[/ltr], then the categorical judgment [ltr]⊢B⊢B[/ltr] states that [ltr]BB[/ltr] is true without any assumptions. With sequent notation the familiar rule for conjunctive introduction becomes[/size]