As in Peano arithmetic the natural numbers are generated by 0 and the successor operation [ltr]ss[/ltr]. The elimination rule states that these are the only possible ways to generate a natural number.We write [ltr]f(c)=R(c,d,xy.e)f(c)=R(c,d,xy.e)[/ltr] for the function which is defined by primitive recursion on the natural number [ltr]cc[/ltr] with base case [ltr]dd[/ltr] and step function [ltr]xy.exy.e[/ltr] (or alternatively [ltr]λxy.eλxy.e[/ltr]) which maps the value [ltr]yy[/ltr] for the previous number [ltr]x:Nx:N[/ltr] to the value for [ltr]s(x)s(x)[/ltr]. Note that [ltr]RR[/ltr] is a new variable-binding operator: the variables [ltr]xx[/ltr] and [ltr]yy[/ltr] become bound in [ltr]ee[/ltr].[ltr]NN[/ltr]-formation.
[ltr]Γ⊢NΓ⊢N[/ltr]
[ltr]NN[/ltr]-introduction.
[ltr]Γ⊢0:NΓ⊢a:NΓ⊢s(a):NΓ⊢0:NΓ⊢a:NΓ⊢s(a):N[/ltr]
[ltr]NN[/ltr]-elimination.
[ltr]Γ,x:N⊢CΓ⊢c:NΓ⊢d:C[x:=0]Γ,y:N,z:C[x:=y]⊢e:C[x:=s(y)]Γ⊢R(c,d,yz.e):C[x:=c]Γ,x:N⊢CΓ⊢c:NΓ⊢d:C[x:=0]Γ,y:N,z:C[x:=y]⊢e:C[x:=s(y)]Γ⊢R(c,d,yz.e):C[x:=c][/ltr]
[ltr]NN[/ltr]-equality (under appropriate premises).
[ltr]R(0,d,yz.e)R(s(a),d,yz.e)=d:C[x:=0]=e[y:=a,z:=R(a,d,yz.e)]:C[x:=s(a)]R(0,d,yz.e)=d:C[x:=0]R(s(a),d,yz.e)=e[y:=a,z:=R(a,d,yz.e)]:C[x:=s(a)][/ltr]
The rule of [ltr]NN[/ltr]-elimination simultaneously expresses the type of a function defined by primitive recursion and, under the Curry-Howard interpretation, the rule of mathematical induction: we prove the property [ltr]CC[/ltr] of a natural number [ltr]xx[/ltr] by induction on [ltr]xx[/ltr].Gödel’s System [ltr]TT[/ltr] is essentially intuitionistic type theory with only the type formers [ltr]NN[/ltr] and [ltr]A→BA→B[/ltr] (the type of functions from [ltr]AA[/ltr] to [ltr]BB[/ltr], which is the special case of [ltr](Πx:A)B(Πx:A)B[/ltr] where [ltr]BB[/ltr]does not depend on [ltr]x:Ax:A[/ltr]). Since there are no dependent types in System [ltr]TT[/ltr] the rules can be simplified. 3.6 The Universe of Small Types
Martin-Löf’s first version of type theory (Martin-Löf 1971a) had an axiom stating that there is a type of all types. This was proved inconsistent by Girard who found that the Burali-Forti paradox could be encoded in this theory.To overcome this pathological impredicativity, but still retain some of its expressivity, Martin-Löf introduced in 1972 a universe [ltr]UU[/ltr] of small types closed under all type formers of the theory, except that it does not contain itself (Martin-Löf 1998 [1972]). The rules are:[ltr]UU[/ltr]-formation.
[ltr]Γ⊢UΓ⊢U[/ltr]
[ltr]UU[/ltr]-introduction.
[ltr]Γ⊢∅:UΓ⊢1:UΓ⊢∅:UΓ⊢1:U[/ltr]
[ltr]Γ⊢A:UΓ⊢B:UΓ⊢A+B:UΓ⊢A:UΓ⊢B:UΓ⊢A×B:UΓ⊢A:UΓ⊢B:UΓ⊢A+B:UΓ⊢A:UΓ⊢B:UΓ⊢A×B:U[/ltr]
[ltr]Γ⊢A:UΓ⊢B:UΓ⊢A→B:UΓ⊢A:UΓ⊢B:UΓ⊢A→B:U[/ltr]
[ltr]Γ⊢A:UΓ,x:A⊢B:UΓ⊢Σx:A.B:UΓ⊢A:UΓ,x:A⊢B:UΓ⊢Πx:A.B:UΓ⊢A:UΓ,x:A⊢B:UΓ⊢Σx:A.B:UΓ⊢A:UΓ,x:A⊢B:UΓ⊢Πx:A.B:U[/ltr]
[ltr]Γ⊢N:UΓ⊢N:U[/ltr]
[ltr]UU[/ltr]-elimination.
[ltr]Γ⊢A:UΓ⊢AΓ⊢A:UΓ⊢A[/ltr]
Since [ltr]UU[/ltr] is a type, we can use [ltr]NN[/ltr]-elimination to define small types by primitive recursion. For example, if [ltr]A:UA:U[/ltr], we can define the type of [ltr]nn[/ltr]-tuples of elements in [ltr]AA[/ltr] as follows:[ltr]A[size=13]n=R(n,1,xy.A×y):UAn=R(n,1,xy.A×y):U[/ltr][/size]
This type-theoretic universe [ltr]UU[/ltr] is analogous to a Grothendieck universe in set theory which is a set of sets closed under all the ways sets can be constructed in Zermelo-Fraenkel set theory. The existence of a Grothendieck universe cannot be proved from the usual axioms of Zermelo-Fraenkel set theory but needs a new axiom.In Martin-Löf (1975) the universe is extended to a countable hierarchy of universes[ltr]U[size=13]0:U1:U2:⋯.U0:U1:U2:⋯.[/ltr][/size]
In this way each type has a type, not only each small type. 3.7 Propositional Identity
Above, we introduced the equality judgment[ltr]Γ⊢a=a[size=13]′:A.(4)(4)Γ⊢a=a′:A.[/ltr][/size]
This is usually called a “definitional equality” because it can be decided by normalizing the terms [ltr]aa[/ltr] and [ltr]a[size=13]′a′[/ltr] and checking whether the normal forms are identical. However, this equality is a judgment and not a proposition (type) and we thus cannot prove such judgmental equalities by induction. For this reason we need to introduce propositional identity types. For example, the identity type for natural numbers [ltr]
I(N,m,n)I(N,m,n)[/ltr] can be defined by [ltr]
UU[/ltr]-valued primitive recursion. We can then express and prove the Peano axioms. Moreover, extensional equality of ufnctions can be defined by[/size]
[ltr]I(N→N,f,f[size=13]′)=Πx:N.I(N,fx,f′x).I(N→N,f,f′)=Πx:N.I(N,fx,f′x).[/ltr][/size]
3.8 The Axiom of Choice is a Theorem
The following form of the axiom of choice is an immediate consequence of the BHK-interpretation of the intuitionistic quantifiers, and is easily proved in intuitionistic type theory:[ltr](Πx:A.Σy:B.C)→Σf:(Πx:A.B).C[y:=fx](Πx:A.Σy:B.C)→Σf:(Πx:A.B).C[y:=fx][/ltr]
The reason is that [ltr]Πx:A.Σy:B.CΠx:A.Σy:B.C[/ltr] is the type of functions which map elements [ltr]x:Ax:A[/ltr] to pairs [ltr](y,z)(y,z)[/ltr] with [ltr]y:By:B[/ltr] and [ltr]z:Cz:C[/ltr]. The choice function [ltr]ff[/ltr] is obtained by returning the first component [ltr]y:By:B[/ltr]of this pair.It is perhaps surprising that intuitionistic type theory directly validates an axiom of choice, since this axiom is often considered problematic from a constructive point of view. A possible explanation for this state of affairs is that the above is an axiom of choice for types, and that types are not in general appropriate constructive approximations of sets in the classical sense. For example, we can represent a real number as a Cauchy sequence in intuitionistic type theory, but the set of real numbers is not the type of Cauchy sequences, but the type of Cauchy sequences up to equiconvergence. More generally, a set in Bishop’s constructive mathematics is represented by a type (commonly called “preset”) together with an equivalence relation.If [ltr]AA[/ltr] and [ltr]BB[/ltr] are equipped with equivalence relations, there is of course no guarantee that the choice function, [ltr]ff[/ltr] above, is extensional in the sense that it maps equivalent element to equivalent elements. This is the failure of the extensional axiom of choice, see Martin-Löf (2009) for an analysis.4. Extensions
4.1 The Logical Framework
The above completes the description of a core version of intuitionistic type theory close to that of (Martin-Löf 1998 [1972]).In 1986 Martin-Löf proposed a reformulation of intuitionistic type theory; see Nordström, Peterson and Smith (1990) for an exposition. The purpose was to give a more compact formulation, where [ltr]λλ[/ltr] and [ltr]ΠΠ[/ltr] are the only variable binding operations. It is nowadays considered the main version of the theory. It is also the basis for the Agda proof assistant. The 1986 theory has two parts:
- the theory of types (the logical framework);
- the theory of sets (small types).
Remark 4.1. Note that the word “set” in the logical framework does not coincide with the way it is used in Bishop’s constructive mathematics. To avoid this confusion, types together with equivalence relations are usually called “setoids” or “extensional sets” in intuitionistic type theory.The logical framework has only two type formers: [ltr]Πx:A.BΠx:A.B[/ltr] (usually written [ltr](x:A)B(x:A)B[/ltr] or [ltr](x:A)→B(x:A)→B[/ltr] in the logical framework formulation) and [ltr]UU[/ltr] (usually called [ltr]SetSet[/ltr]). The rules for [ltr]Πx:A.BΠx:A.B[/ltr] ([ltr](x:A)→B(x:A)→B[/ltr]) are the same as given above (including [ltr]ηη[/ltr]-conversion). The rules for [ltr]UU[/ltr] ([ltr]SetSet[/ltr]) are also the same, except that the logical framework only stipulates closure under [ltr]ΠΠ[/ltr]-type formation.The other small type formers (“set formers”) are introduced in the theory of sets. In the logical framework formulation each formation, introduction, and elimination rule can be expressed as the typing of a new constant. For example, the rules for natural numbers become[ltr]N0sR:Set,:N,:N→N,:(C:N→Set)→C0→((x:N)→Cx→C(sx))→(c:N)→Cc.N:Set,0:N,s:N→N,R:(C:N→Set)→C0→((x:N)→Cx→C(sx))→(c:N)→Cc.[/ltr]
where we have omitted the common context [ltr]ΓΓ[/ltr], since the types of these constants are closed. Note that the recursion operator [ltr]RR[/ltr] has a first argument [ltr]C:N→SetC:N→Set[/ltr] unlike in the original formulation.Moreover, the equality rules can be expressed as equations[ltr]RCde0RCde(sa)=d:C0=ea(RCdea):C(sa)RCde0=d:C0RCde(sa)=ea(RCdea):C(sa)[/ltr]
under suitable assumptions.In the sequel we will present several extensions of type theory. To keep the presentation uniform we will however not use the logical framework presentation of type theory, but will use the same notation as in section 2. 4.2 A General Identity Type Former
As we mentioned above, identity on natural numbers can be defined by primitive recursion. Identity relations on other types can also be defined in the basic version of intuitionistic type theory presented in section 2.However, Martin-Löf (1975) extended intuitionistic type theory with a uniform primitive identity type former [ltr]II[/ltr] for all types. The rules for [ltr]II[/ltr] express that the identity relation is inductively generated by the proof of reflexivity, a canonicial constant called [ltr]rr[/ltr]. (Note that [ltr]rr[/ltr] was coded by the number 0 in the introductory presentation of proof-objects in 2.3. The elimination rule for the identity type is a generalization of identity elimination in predicate logic and introduces an elimination constant [ltr]JJ[/ltr]. (We here show the formulation due to Paulin-Mohring (1993) rather than the original formulation of Martin-Löf (1975).) The inference rules are the following.[ltr]II[/ltr]-formation.[ltr]Γ⊢AΓ⊢a:AΓ⊢a[size=13]′:AΓ⊢I(A,a,a′)Γ⊢AΓ⊢a:AΓ⊢a′:AΓ⊢I(A,a,a′)[/ltr][/size]
[ltr]II[/ltr]-introduction.[ltr]Γ⊢AΓ⊢a:AΓ⊢r:I(A,a,a)Γ⊢AΓ⊢a:AΓ⊢r:I(A,a,a)[/ltr]
[ltr]II[/ltr]-elimination.[ltr]Γ,x:A,y:I(A,a,x)⊢CΓ⊢b:AΓ⊢c:I(A,a,b)Γ⊢d:C[x:=a,y:=r]Γ⊢J(c,d):C[x:=b,y:=c]Γ,x:A,y:I(A,a,x)⊢CΓ⊢b:AΓ⊢c:I(A,a,b)Γ⊢d:C[x:=a,y:=r]Γ⊢J(c,d):C[x:=b,y:=c][/ltr]
[ltr]II[/ltr]-equality (under appropriate assumptions).[ltr]J(r,d)=dJ(r,d)=d[/ltr]
By constructing a model of type theory where types are interpreted as groupoids (categories where all arrows are isomorphisms) Hofmann and Streicher (1998) showed that it cannot be proved in intuitionistic type theory that all proofs of [ltr]I(A,a,b)I(A,a,b)[/ltr] are identical. This may seem as an incompleteness of the theory and Streicher suggested a new axiom [ltr]KK[/ltr] from which it follows that all proofs of [ltr]I(A,a,b)I(A,a,b)[/ltr] are identical to [ltr]rr[/ltr].The [ltr]I[/ltr][ltr]I[/ltr]-type is often called the intensional identity type, since it does not satisfy the principle of function extensionality. Intuitionistic type theory with the intensional identity type is also often called intensional intuitionistic type theory to distinguish it from extensional intuitionistic type theory which will be presented in section 7.1. 
Natural Numbers
اليوم في 5:04 pm من طرف