高级数理逻辑第七章

1、存在性命题的两种解释&证明,一个典型的存在性命题：存在无理数a和b，使得ab是有理数。证：若是有理数，则a=b=若是无理数，则a=b=对于存在性命题的构造性解释：能找到无理数a和b，使得ab是有理数。对应于构造性解释的证明为构造性证明。构造性证明：必须证是无理数。,构造性逻辑中自然推理系统,构造性逻辑不支持经典逻辑中的反证律，进而不支持排中律。在构造性逻辑规则中，用以下两个规则替代反证律：(+)若，AB，AB，则A()若A，A，则B,构造性逻辑中公理推理系统,在公理推理系统中，用以下两个公理：(AB)(AB)A)A(AB)替代公理(AB)(AB)A),cA,A是在构造性逻辑中由C形式可推演（C

2、形式可证明）的，记为cA，当且仅当cA能有限次使用构造性逻辑中形式推演规则生成。一个有限序列1cA1，2cA2，ncAn被称为ncAn的C形式证明。其中，kcAk（1kn）由使用某一推演规则而生成。,证明xA(x)cxA(x)。,证：(1)xA(x)xA(x)(Ref)(2)xA(x)A(u)u不在A(x)中出现(-)(1)(3)A(u)，xA(x)A(u)(+)(2)(4)A(u)，xA(x)A(u)()(5)A(u)xA(x)(+)(3)(4)(6)x(A(x)xA(x)(-)(5)(7)xA(x)，xA(x)xA(x)(+)(5)(8)xA(x)，xA(x)xA(x)()(9)xA(x)

3、xA(x)(+)(7)(8)(10)A(u)A(u)(Ref)(11)A(u)xA(x)(+)(10)(12)xA(x)，A(u)xA(x)(+)(11)(13)xA(x)，A(u)xA(x)()(14)xA(x)A(u)(+)(12)(13)(15)xA(x)xA(x)(+)(14)(16)xA(x)xA(x)(Tr)(9)(15),zcA,定义：zcA当且仅当存在序列A1，A2，An，使得A=An，且对于任何Ak，k=1，2，n，满足以下条件之一：Ak是公理Ak存在i，jk，使得Ai=AjAk存在ik和B(u)，使得u不在中出现，Ai=B(u)，且Ak=xB(x)A是在构造性逻辑中C形式可

4、证明的iffzcA,自然推理系统与公理推理系统的关系,设Form(L)，AForm(L)，则zcA当且仅当cA,构造性逻辑与经典逻辑的关系,设Form(L)，AForm(L)。若cA，则A逆命题不成立。,Glivenko定理,设Form(Lp)，AForm(Lp)。cA当且仅当A证明：必要性。由cA，则A。进一步，可得A。充分性。对A的结构进行归纳证明。以证(-)为例。,证明：若，AcB，AcB则cA证：(1)，AcB(已知)(2)A，AcA()(3)A，AcA()(4)AcA(+)(2)(3)(5)，AcA(+)(4)(6)，Ac()(7)，AcB(Tr)(1)(5)(6)(8)，AcB(与

5、(7)同理)(9)cA(+)(7)(8),Gdel翻译,AForm(L)的Gdel翻译A。，递归定义如下：若AAtom(L)，则A。=A；(A)。=A。；(AB)。=A。B。；(AB)。=(A。B。)；(AB)。=A。B。；(AB)。=A。B。；(xA(x)。=x(A(x)。；(xA(x)。=x(A(x)。设Form(L)。=A。|A,引理,若AForm(L)，则A。AA。cA。,定理,设Form(L)，AForm(L)。A当且仅当。cA。,C协调性,Form(L)是C协调的，当且仅当不存在AForm(L)，使得cA且cA。,C极大协调性,Form(L)是C极大协调的，当且仅当是C协调的。对于

6、任何A，A是C不协调的。,Kripke语义,对于公式A，其在赋值v下的值1，0，可能由一组具有时间顺序的赋值决定。对于公式A，其在赋值v下的值为1，表示A在v及其时间顺序之后的所有赋值下的值都为1。对于公式A，其在赋值v下的值为0，表示A在v的时间顺序之前的所有赋值下的值都为0。,语义（一）,定义：设K是一个集，R是K上的一个自反和传递的二元关系。称每个vK为对Lp的构造性赋值当且仅当v：Lp中所有命题符号1，0，且对于任何的命题符号p和vK，若pv=1并且R，则pv=1。定义：给定K和R，构造性赋值vK给公式A指派的值，记为Av。其定义为：(i)pv1,0。(ii)若Av=Bv=1，则(AB

7、)v=1；否则，(AB)v=0。(iii)若Av=Bv=0，则(AB)v=0；否则，(AB)v=1。(iv)若对于任何使得R的vK，Av=1蕴含Bv=1，则(AB)v=1；否则，(AB)v=0。(v)若对于任何使得R的vK，Av=Bv，则(AB)v=1；否则，(AB)v=0。(vi)若对于任何使得R的vK，Av=0，则(A)v=1；否则，(A)v=0。,语义（二）,定义：给定K和R，每个vK为对L的构造性赋值，当且仅当v包括一个论域D(v)和以所有的个体符号、关系符号、函数符号、自由变元符号构成的集合为定义域的一个函数（记为v），且将v(a)，v(F)，v()，v(f)，v(u)记为av，Fv

8、，v，fv，uv，其中a为个体符号，F为n元关系符号，f为m元函数符号，u为自由变元符号，v满足以下条件：i）若v，vK且R，则D(v)D(v)。ii）av，uvD(v)。若v，vK且R，则av=av，uv=uv。iii）FvD(v)n。若v，vK且R，则FvFv。iv）v=|xD(v)。若v，vK且R，则vv。v）fv：D(v)mD(v)。若v，vK且R，则fv=fv|D(v)。,语义（三）,给定K和R，项t在构造性赋值vK下的值，记为tv。其定义为：i）av，uvD(v)ii）(f(t1，t2，tn)v=fv(t1v，t2v，tnv)，其中t1，t2，tnTerm(L)定理：给定K和R。若

9、vK，tTerm(L)，则tvD(v)。若v，vK，tTerm(L)且R，则tv=tv。,语义（四）,给定K和R，公式A在构造性赋值vK下的值，记为Av。其定义为：(i)若Fv，(F(t1，t2，tn)v=1；否则，(F(t1，t2，tn)v=0。(ii)若Av=0，则(A)v=1；否则，(A)v=0。(iii)若Av=Bv=1，则(AB)v=1；否则，(AB)v=0。(iv)若Av=Bv=0，则(AB)v=0；否则，(AB)v=1。(v)若Av=1并且Bv=0，则(AB)v=0；否则，(AB)v=1。(vi)若Av=Bv，则(AB)v=1；否则，(AB)v=0。(vii)u代入x，由A(x)

10、得到A(u)，且u不在A(x)中出现。若对于任何使得R成立的vK和任何D(v)，A(u)v(u/)=1，则(xA(x)v=1；否则，(xA(x)v=0。(viii)u代入x，由A(x)得到A(u)，且u不在A(x)中出现。若存在D(v)，使得A(u)v(u/)=1，则(xA(x)v=1，否则，(xA(x)v=0。定理：给定K和R。若vK，AForm(Lp)Form(L)，则Av1,0。若v，vK，AForm(Lp)Form(L)且R，则Av=1蕴含Av=1。,公式的语义分类,是C可满足的，当且仅当存在K，R和vK，使得v=1。特别的，若A是C可满足的，则称A为C可满足式。A是C有效的，当且仅当对于任何的K，R和vK，Av=1。,逻辑推论,设Form(L)，AForm(L)。A是的C逻辑推论，记作cA，当且仅当对于任何的K，R和vK，v=1蕴涵Av=1（Av=0蕴涵v=0）。cA表示A为C有效公式。c不是L中符号。cA不是公式。AcB表示“AcB并且BcA”，并称A和B是C逻辑等值的。,可靠性定理,设Form(L)，AForm(L)。i)若cA，则cA