Logical Methods in Computer Science
Vol.4(2:1)2008,pp.1–29
www.lmcs-online
Abstract.IZF is a well investigated impredicative constructive version of Zermelo-Fraen-kel t theory.Using t terms,we axiomatize IZF with Replacement,which we call
IZF R,along with its intensional counterpart IZF−
R .We define a typed lambda calculusλZ
corresponding to proofs in IZF−
R according to the Curry-Howard isomorphism principle.
Using realizability for IZF−
R ,we show weak normalization ofλZ.We u normalization
to prove the disjunction,numerical existence and term existence properties.An inner
extensional model is ud to show the properties,along with the t existence property,
for full,extensional IZF R.
1.Introduction
Four salient properties of constructive t theories are:
•Numerical Existence Property(NEP):From a proof of a statement“there exists a natural number x ”a witness n∈N can be extracted.
•Disjunction Property(DP):Ifφ∨ψis provable,then eitherφorψis provable.•Term Existence Property(TEP):If∃x.φ(x)is provable,thenφ(t)is provable for some term t.
•Set Existence Property(SEP):If∃x.φ(x)is provable,then there is a formulaψ(x)such that∃!x.φ(x)∧ψ(x)is provable,where bothφandψare term-free.
How to prove the properties for a given theory?There is a variety of methods appli-cable to constructive theories.Cut-elimination,proof normalization,realizability,Normalization proofs,bad on the Curry-Howard isomorphism principle,have the advantage of providing an explicit
method of witness and program extraction from proofs.They also provide information about the behaviour of the proof system.
We are interested in intuitionistic t theory IZF.It is esntially what remains of ZF t theory after excluded middle is carefully taken away.An important decision to make on the way is whether to u Replacement or Collection axiom schema.We will call the version with Collection IZF C and the version with Replacement IZF R.In the literature,IZF usually denotes IZF C.Both theories extended with excluded middle are equivalent to ZF[Fri73].
They are not equivalent[FS85].While the proof-theoretic power of IZF C is equivalent to that of ZF,the exact power of IZF R is unknown.Arguably IZF C is less constructive,as Collection,similarly to Choice,asrts the existence of a t without defining it.
Both versions have been investigated thoroughly.Results up to1985are prented in [Bee85,ˆS85].Later rearch was concentrated on weaker subsystems[AR01,Lub02].A predicative constructive t theory CZF has attracted particular interest.[AR01]describes the t-theoretic apparatus available in CZF and provides further references.
We axiomatize IZF R,along with its intensional version IZF−R,using t terms.We define a typed lam
bda calculusλZ corresponding to proofs in IZF−R.We also define realizability for IZF−R,in the spirit of[McC84],and u it to show thatλZ weakly normalizes.Strong normalization ofλZ does not hold;moreover,we show that in non-well-founded IZF even weak normalization fails.
With normalization in hand,the properties NEP,DP and TEP easily follow.To show the properties for full,extensional IZF R,we define an inner model T of IZF R,consisting of what we call transitively L-stable ts.We show that a formula is true in IZF R iffits relativization to T is true in IZF−R.Therefore IZF R is interpretable in IZF−R.This allows us to u the properties proven for IZF−R.In IZF R,SEP easily follows from TEP.
The importance of the properties in the context of computer science stems from the fact that they make it possible to extract programs from constructive proofs.For example, suppo IZF R⊢∀n∈N∃m∈N.φ(n,m).From this proof a program can be extracted —take a natural number n,construct a proof IZF R⊢
n,m)and apply NEP to get a number m such that IZF R⊢φ(m).A detailed account of program extraction from IZF R proofs can be found in[CM06].
There are many provers with the program extraction capability.However,they are usually bad on v
ariants of type theory,which is a foundational basis very different from t theory.This makes the process of formalizing program specification more difficult,as an unfamiliar new language and logic have to be learned from scratch.[LP99]strongly argues against using type theory for the specification purpos,instead promoting standard t theory.
IZF R provides therefore the best of both worlds.It is a t theory,with familiar language and axioms.At the same time,programs can be extracted from proofs.OurλZ calculus and the normalization theorem make the task of constructing the prover bad on IZF R not very difficult.
This paper is mostly lf-contained.We assume some familiarity with t theory,proof theory and programming languages terminology,found for example in[Kun80,SU06,Pie02]. The paper is organized as follows.We start by prenting in details intuitionisticfirst-order logic in ction2.In ction3we define IZF R along with its intensional version IZF−R.In ction4we define a lambda calculusλZ corresponding to IZF−R proofs.Realizability for IZF−R is defined in ction5.We u it to prove normalization ofλZ in ction6,where we also show that non-well-founded IZF does not normalize.We prove the properties in ction7,and show how to derive them for full,extensional IZF R in ction8.Comparison with other results can be found in ction9.
2.Intuitionistic first-order logic
小学三年级美术画
Due to the syntactic character of our results,we prent the intuitionisticfirst-order logic(IFOL)in details.We u a natural deduction style of proof rules.The terms will
be denoted by letters t,s,u.The variables will be denoted by letters a,b,c,d,e,f.The notation a stands for afinite quence,treated as a t when convenient.The i-th element of a quence is denoted by a i.We considerα-equivalent formulas equal.The capture-avoiding substitution is defined as usual;the result of substituting s for a in a term t is denoted by t[a:=s].We write t[a1,...,a n:=s1,...,s n]to denote the result of substituting simultaneously s1,...,s n for a1,...,a n.Contexts,denoted byΓ,are ts of formulas.The t of free variables of a formulaφ,denoted by F V(φ),are defined as usual.The free variables of a contextΓ,denoted by F V(Γ),are the free variables of all formulas inΓ.The notationφ( a)means that all free variables ofφare among a.The proof rules are as follows:
Γ⊢φΓ⊢φ→ψΓ⊢φ
Γ⊢φ→ψ
Γ⊢φΓ⊢ψ
Γ⊢φ
Γ⊢φ∧ψ
Γ⊢φ∨ψ
Γ⊢ψ
Γ⊢ϑ
Γ⊢φ
Γ⊢φ[a:=t]
Γ⊢φ[a:=t]
Γ⊢ψ
a/∈F V(Γ)∪{ψ} Negation in IFOL is an abbreviation:¬φ≡φ→⊥.So is the symbol↔:φ↔ψ≡(φ→ψ∧ψ→φ).Note that IFOL does not contain equality.The excluded middle rule added to IFOL makes it equivalent to the classicalfirst-order logic without equality.We adopt the“dot”-convention—a formula∀a.φshould be pard as∀a.(φ).In other words1, the dot reprents a left pare
nthesis who scope extends as far to the right as possible. Lemma2.1.For any formulaφ,φ[a:=t][b:=u[a:=t]]=φ[b:=u][a:=t],for b/∈F V(t). Proof.Straightforward structural induction onφ.
3.IZF R
Intuitionistic t theory IZF R is afirst-order theory,equivalent to ZF when extended with excluded middle.It is a definitional extension of term-free versions prented in [Myh73,Bee85,FS85].The signature consists of one binary relational symbol∈and func-tion symbols ud in the axioms below.The t of all IZF R terms will be denoted by T ms. The notation t=u is an abbreviation for∀z.z∈t↔z∈u.Function symbols0and S(t) are abbreviations for∅and {t,{t,t}}.Bounded quantifiers and the quantifier∃!a(there exists exactly one a)are also abbreviations defined in the standard way.The axioms are as follows:
•(EMPTY)∀c.c∈∅↔⊥奥利奥慕斯蛋糕
青年强则国强
•(PAIR)∀a,b∀c.c∈{a,b}↔c=a∨c=b
•(INF)∀c.c∈ω↔c=0∨∃b∈ω.c=S(b)
20的序数词•(SEP
φ(a, f))∀ f,a∀c.c∈S
φ(a, f)
(a, f)↔c∈a∧φ(c, f)
•(UNION)∀a∀c.c∈ a↔∃b∈a.c∈b •(POWER)∀a∀c.c∈P(a)↔∀b.b∈c→b∈a
•(REPL φ(a,b, f ))∀ f,a ∀c.c ∈R φ(a,b, f )(a, f )↔(∀x ∈a ∃!y.φ(x,y, f ))∧(∃x ∈a.φ(x,c, f ))
•(IND φ(a, f )
)∀ f.
(∀a.(∀b ∈a.φ(b, f ))→φ(a, f ))→∀a.φ(a, f )•(L φ(a, f ))∀ f,a,b.a =b →φ(a, f )→φ(b, f )
Axioms SEP φ,REPL φ,IND φand L φare axiom schemas,and so are the corresponding function symbols —there is one function symbol for each formula φ.Formally,we define formulas and terms by mutual induction:
φ::=t ∈t |φ∧φ|...t ::=a |{t,t }|S φ(a, f )(t, t )|R φ(a,b, f )(t, t )|...Our prentation is not minimal;for examp
le,the empty t axiom can be derived as usual using Separation and Infinity.However,we aim for a natural axiomatization of IZF R ,not necessarily the most optimal one.
The Leibniz axiom schema L φis usually not prent among the axioms of t theories,as it is assumed that logic contains equality and the axiom is a proof rule.We include L φamong the axioms of IZF R ,becau there is no obvious way to add it to intuitionistic logic in the Curry-Howard isomorphism context,as its computational content is unclear.Our axiom of Replacement is equivalent to the usual formulations,e [Moc06b]for details.IZF −
R will denote IZF R without the Leibniz axiom schema L φ.IZF −R is an intensional version of IZF R —even though extensional equality is ud in the axioms,it does not behave as the “real”equality.The terms S φ(a, f
)and R φ(a, f )can be displayed as {x ∈a |φ(x, f )}and {z |(∀x ∈a ∃!y.φ(x,y, f
))∧∃x ∈a.φ(x,z, f )}.The axioms (EMPTY),(PAIR),(INF),(SEP φ),(UNION),(POWER)and (REPL φ)all asrt the existence of certain class and have the same form:∀ a .∀c.c ∈t A ( a )↔φA (c, a ),where t A is a function symbol and φA a corresponding formula for the axiom A.For example,for (POWER),t POWER is P and φPOWER is ∀b.b ∈c →b ∈a .We rerve the notation t A and φA to denote the ter
m and the corresponding formula for the axiom A.
Lemma 3.1.Every term T ≡t A (−−→t ( a ))of IZF R is definable.In other words,there is a
term-free formula φ(x, a )such that IZF R ⊢∀ a .φ(T, a )∧∃!x.φ(x, a ).
Proof.Straightforward induction on the size of T .We first show the claim for ω,then for the rest of the terms.For ω,the defining formula 2is:
φ(x )≡c ∈x ↔c =0∨∃y ∈x.c =S (y )
Indeed,φ(ω)holds.Suppo φ(z )for some z ,we need to show that z =ω.To do this,we prove by ∈-induction ∀c.c ∈z ↔c ∈ω.Take any c and suppo c ∈z .Then c =0or there is y ∈z such that c =S (y ).In the former ca c ∈ω,in the latter y ∈c ,so by the induction hypothesis y ∈ωand hence c ∈ω.The other direction is symmetric.Consider now arbitrary T ≡t A (−−→t ( a )).Let u denote −−→t ( a ),so T ≡t A ( u ).By the induction hypothesis there are formulas −−−−→φ(x, a )defining u .Consider the formula:φ(x, a )≡∃ x . −−−−→φ(x, a )∧∀c.c ∈x ↔φA (c, x )
We will now show that φ(x, a )defines T .Take any a and take x = u .We have −−−−→φ(u, a )
and by the axiom (A)corresponding to t A ,we get ∀c.c ∈t A ( u )↔φA (c, u ).Furthermore,
suppo φ(z, a )for some z .Then there are b such that −−−−→φ(b, a )and ∀c.c ∈z ↔φA (c, b ).Since −−−−→φ(x, a )define u , b = u and thus also ∀c.c ∈z ↔φA (c, u ).To show that z =T ,it
suffices to show that ∀a.a ∈T ↔a ∈z ,which follows easily.
It remains to consider the situation when φA contains some terms,which can happen if A is the Separation or Replacement axiom.However,by the induction hypothesis all the terms are definable as well,so there is also a term-free formula φ′equivalent to φ.
Corollary 3.2.For any clod term t there is a term-free formula φ(x )such that IZF R ⊢(∃!x.φ(x ))∧φ(t ).
4.The λZ calculus
We now prent a lambda calculus λZ for IZF −
R ,bad on the Curry-Howard isomor-
phism principle.The first-order part of λZ is esntially λP 1from [SU06].The lambda terms in the calculus correspond to proofs in IZF −
R .The correspondence is captured formally
by Lemma 4.10.
大悲咒的作用
The lambda terms in λZ will be denoted by letters M,N,O,P .There are two kinds of lambda abstractions,one ud for proofs of implications,the other for proofs of universal quantifications.We u parate ts of variables for the abstractions and call them proof and first-order variables,respectively.We u letters x,y,z for proof variables and a,b,c for first-order variables.Letters t,s,u are rerved for IZF R terms.The types in the system are IZF R formulas.The lambda terms are generated by an abstract grammar.The first group of terms is standard and ud for IFOL proofs:
M ::=x |M N |λa.M |λx :φ.M |inl(M )|inr(M )|fst(M )|snd(M )|[t,M ]|M t
M,N |ca(M,x :φ.N,x :ψ.O )|magic(M )|let [a,x :φ]:=M in N
The rest of the terms correspond to the axioms of IZF −R :
emptyProp(t,M )|emptyRep(t,M )
pairProp(t,u 1,u 2,M )|pairRep(t,u 1,u 2,M )
unionProp(t,u,M )|unionRep(t,u,M )
p φ(a, f )Prop(t,u, u ,M )|p φ(a, f )Rep(t,u,
影子的变化规律u ,M )powerProp(t,u,M )|powerRep(t,u,M )
infProp(t,M )|infRep(t,M )
repl φ(a,b, f )Prop(t,u, u ,M )|repl φ(a,b, f )Rep(t,u,
u ,M )ind φ(a, b )
( t ,M )The ind term corresponds to the ∈-induction axiom schema (IND φ(a, f )),and Prop and Rep terms correspond to the respective axioms.The exact nature of the correspondence will become clear in the next ction.Briefly and informally,the Rep terms are reprentatives of the fact that a t is a member of a term t ( u )and the Prop terms provide the defining property of t ∈t ( u ).To avoid listing all of them every time,we adopt a convention of using axRep and axProp terms to tacitly mean all Rep and Prop terms,for ax being one of empty,pair,union,p,power,inf and repl.With this convention in mind,we can summarize the definition of the Prop and Rep terms as:
axProp(t, u ,M )|axRep(t, u ,M ),
where the number of terms in the quence u depends on the particular axiom.
梦到孕妇The free variables of a lambda term are defined as usual,taking into account that variables inλ,ca and let terms bind respective terms.The relation ofα-equivalence is defined taking this information into account.We considerα-equivalent terms equal.We denote the t of all free variables of a term M by F V(M)and the t of the freefirst-order variables of a term by F V F(M).The free(first-order)variables of a contextΓare denoted by F V(Γ)(F V F(Γ))and defined in a natural way.The notation M[x:=N]stands for a term M with N substituted for x.The t of allλZ lambda terms will be denoted byΛ.
4.1.Reduction rules.The deterministic reduction relation→aris by lazily evaluating the following ba reduction rules:
(λx:φ.M)N→M[x:=N](λa.M)t→M[a:=t]
fst( M,N )→M snd( M,N )→N
ca(inl(M),x:φ.N,x:ψ.O)→N[x:=M]ca(inr(M),x:φ.N,x:ψ.O)→O[x:=M] let[a,x:φ]:=[t,M]in N→N[a:=t][x:=M]
axProp(t, u,axRep(t, u,M))→M
ind
φ(a, b)( t,M)→λc.M c(λb.λx:b∈c.ind
φ(a, b)
( t,M)b)c,b,x new
The laziness is specified formally by the following evaluation contexts:
[◦]::=fst([◦])|snd([◦])|ca([◦],x:φ.M,x:ψ.N)|axProp(t, u,[◦])
let[a,y:φ]:=[◦]in N|[◦]M|magic([◦])
In other words,the(small-step)reduction relation aris from the ba reduction rules and the following inductive definition:
M→M′
snd(M)→snd(M′)
M→M′
axProp(t, u,M)→axProp(t, u,M′)
800字优秀作文大全M→M′
M N→M′N
M→M′
