大一各科课件-离散数理逻辑slide5-axiomsystem

数理逻辑-(3)逻辑公理系马帅 3.1逻辑公理系3.2命题逻辑公理系3.3谓词逻辑公理系3.4定理证3.5公理系统性3.6理论与模3.7判定问计算机学 欧几里德（325BC-265BC），古希腊数学家《几何原本》是把点、线、面、角等分为原始定义概念（23）和可义概念命题分为公理（5）、公设由公理公设出发加以证明的定理从简单到复杂，证明相当严格。从而建立了欧几得几何学的第一公1．等于同量的2．等最3，等量减等量，其差仍相等4．彼此能重合的物体是全等的5．整体大于部

公1.由任意一点到另外任意2.一条有限3.以任意点为心及任意的4.凡直角都彼计算机学 x(N(x)0≤x)x(N(x)y(N(y)x≤y))xy(N(x)N(y)x+yy+x)xy(N(x)N(y)x+y≤y)对象运算关系计算机学 基本概念数数n的后继n'1．0

3．没有自然数n，使得n'等于04．对任意的自然数m和n，如果m’=n’，那么m=n，那么N包含每个自然计算机学 自然数公xy自然数公理是实质公具体概念：后继s()，0，+，自然数公理是所有的自然数命题真值的依从自然数公理能计算机学 x(N(x)0≤x)x(N(x)y(N(y)x≤y))xy(N(x)N(y)x+y=y+x)是真xy(N(x)N(y)x+y≤y)x(I(x)0≤x)xy(I(x)y(I(y)x≤y)xy(y(I(x)I(yx+y=y+x)xy(I(x)I(y)x+y≤y))计算机学 x(Q(x)R(c,x))x(Q(x)y(Q(y)R(x,y))xy(Q(x)Q(y)抽象：不同论 计算机学 (1)各种初始符号。初始符号是一个形式系统的“字母”，经解释其中一部分是初始概念(2)形成规则。规定初始符号组成各种合适符号序列的规则。经解释(3)公理。把某些所要肯定的公式选出，作为推导其它所要肯定的公(4)变形规则应用变形规则进行推导可以得到一系列公式，这些公式经过解释是统的定理计算机学 公理从一些公理出发，根据演绎法，推导出一系列定理系叫作公理系统符号公式–公式是用于表达命题的符号串公理–公理是用于表达推理由之出发的初始肯定推理规则–推理规则是由公理及已证定理得出新定理定理–表达了肯定的所有命题计算机学 3.1逻辑公理系3.2命题逻辑公理系3.3谓词逻辑公理系3.4定理证3.5公理系统性3.6理论与模3.7判定问计算机学 定义：命题逻辑的公理系统定义(1)1)命题变元Q,Q2…,2)联结词3)括号：(2)形成规则(公式定义1若Q是命题变元，则Q2)若Q是公式，则(Q)3)若Q,R是公式，则(QR)计算机学 命题逻辑公理系(3)公理：公理模式中P,Q,R为任意公1公理模式：R2公理模式A：(P(QR((PQ3公理模式：(QR(4)变形规则：推理规则(分离规则MP规则若Q和QR成立，则R成立。其中，Q和QR，R称为结论计算机学 结词符号,,,可以认为是缩写公式，用≡表示缩(1)QR≡(2)QR≡(3)QR≡(QR)(4)QR≡计算机学 (P(QR))((PQ)(P(QR))(QR)(P(QR))((PQ)(QR)(R

QQ计算机学 已知Q成立，证明R→Q成A1=QA2=A3=

A1推理序33计算机学 定义3.2设Γ是公式集Q

Γ称为推演的前提集α1α2,αn，其AA (α每个αk(1)α是公理(2)α(3有ijkαkαiα由αα用MP规则推则称它为Q的从Γ的一个推演(演绎记为Γ├Q

称ααn为结推理序1推论如果Q是公QΓ，则Γ├计算机学 证明与定 则A1,A2,AnQ称为Γ├Q的一个证明。计算机学 {P,A1=A2=PA4=A5=A6=A7=

A2=A1A4A2A5=A4A6A6=计算机学 ├(QR)A1=Q A2=(Q(RQ))((QR)(QQ))A2A3=(QR) 计算机学 Q(QR)(涵义A1=A2=(RQ)A3=((RQ)(Q→R))(Q((RQ)A4=Q((RQ)A5=(Q((RQ)(Q→R)))((Q(RQ))(QA6=(Q(RQ))(QA7=Q

A2A3├A2A4A5├1A6├计算机学 Γ{Q}R当且仅当Γ1Γ{Q}R成立，证明Γ(1.1)归纳基础：用关于Γ{Q}到R的推演长度n当n=1时，R或为公理，或属于Γ，或R是QA2=A3=所以├QR，从而Γ├若R=Q，则Q所以Γ├

若RΓA2=A3=有Γ计算机学 (1.2)归纳假设：假设Γ{Q}到R的推演长度小于n(1.3)归纳证明：当Γ{Q}到R的推演长度等于nΓ{Q}Ai=

因为i,j<n,有所Γ{Q}├Γ├Γ{Q}├Γ├Q

Am=Ak=QAk+1=Q((QP)(Q

=(QP)(QAk+3=(Q计算机学 由ΓQR可知，有推理序列A1A2,……Am，使得Am=QR。证明有Γ{Q}R。因有推理序列A1A2,……Am，其Am=Am+1=Am+2=计算机学 证明PQ├P{P,Q,(PQ)}├Q，{P,Q,(PQ)}├123(P4(PQ)(P5P6所以有P,Q├(PQ)，即P,QP

AA2A3├QA4=A3A5=A1计算机学 证明PQ(PR(PQ演绎定理：(PQ)(PR，PQ1(PQ)23=(PQ)(PR)(456(PQ)(PR)(7=910Q

AA├QRA3=A1AA4=A2├QRA6=A1AA7=A2A计算机学 如果{ΓQ}├RΓQ}├R,则Γ├1Q2Q3(QR)(RQ456(Q7

Γ{Q}├RΓ├Γ{Q}├RΓ├A3A3=A2AA,A4├(QA6=A5计算机学 如果{ΓQ}├RΓQ}├R，则Γ1Q2Q3(QR)(45Q67Q8(9

Γ{Q}├RΓ├Γ{Q}├RΓ├├(QR)(A3=A1AA,A├A,A├(QA8=A7计算机学 定理：若Γ├R，则Γ├QRAk-1=Ck-Ak+1=RAk+2=

Ak+1=Ak定理：若ΓPQΓP(QR，则Γ├PRAm-1=Dm-Am=Am+n-1=Dm+n-Am+n=PAm+n+1=(P→(Q→R))→((P→Q)Am+n+2=(P→Q)

Γ├Γ├P3.1逻辑公理系3.2命题逻辑公理系3.3谓词逻辑公理系3.4定理证3.5公理系统性3.6理论与模3.7判定问计算机学 (1) 变元：x,x 常元：,c3)函词符号：f1,f1,......；f2,f 4)谓词符号1,Q1,......；Q2,Q 5)运算符号：,67

号：号：计算机学 (2) k3若是t…t项，则是fn(t,…t)k(3)1)若是t,,n项，则Qkn(t,…t)2)若Q是公式，则(Q)是公3)若Q和R是公式，则(QR)4)若Q是公式，则(xQ)计算机学 (4)公理集合1理模式A1：Q2理模式A2：(P(QR((PQ3A3：(QR5).公理模式A5：x(QR(x(QxR(x))，其中x不(5)推理规1)分离规则（简称MP规则）：从Q和QR推出R2)概括规则（简称UG规则）：从Q(x)推出(xQ计算机学 ,,,(2).QR≡(3).QR≡(QR)(4).QR≡xQ(x)计算机学 定义设Γ是合式公式集Q是合式式序列α1α2,αn，其中A1AA (α每个αk(1)α是公(2)α(3有i,j<kαkαiα由αiα用MP规推出(4)有i<j使Aj=xAi由用UG规则推则称它为Q的从Γ的一个推演(绎),记为Γ├Q

序列从演绎出证明。可证明α。推理序1如果Q是公理或Γ，则Γ├计算机学 定义：如果├Q，则Q计算机学 ={证明1P(x)23

Q计算机学 xQ(xyQ(y)(y不在Q证明A1=xQ(x) AA2=y(xQ(x) A3=y(xQ(x)Q(y))(xQ(x)y AA4=xQ(x)y A3=A2计算机学 Γ{A}├B当且仅当Γ├式，A可证，xA可证？？

约束变自由约束出自由出计算机学 Γ{A}├B，且A为闭公式(语句)，当且仅当Γ├归纳基础：用关于Γ{A}到B的推演长度n当n=1时，B或为公理，或属于Γ，或B是AA2A3–所以├AB，从而Γ├若BΓA2A3–有Γ├

若B=AA所以Γ├计算机学 归纳假设：假设Γ{A}到B的推演长度小于n定理成 Γ{A} A • •

因为i,j<nΓ{A}├Γ├

从ΓAAmAAAnAi=AjR

Γ{A}├Γ├A

1=((RB))R)(AAk+=AR)(AA+计算机学 Γ{A}

因为Γ{A}├R推演 从Γ的推An-2=

长度等于n-1Γ├

AAmA–Am+1=x(ARAn-1=xR=

AmAA为闭计算机学 Γ到AB的推由Γ├AB可知，有推理序列A,A2m使得AB证明有Γ{A}├B。因AAAmAmAm计算机学 定理：├x(Q(x)R(x))(xQ(x)仅需证x(Q(x)R(x))├xQ(x)xR(x)。设Γ={x(Q(x)R(x))A1A2x(Q(x)R(x))A3A4Q(x)R(x)A5A6A7Q(x)R(x)A8A9A10

AA2=A1A4=A3AA7=A3A├x(P(x,y)→Q(x,y))→(xP(x,y)→xQ(x,y)x(P(x,b)→Q(x,b))→(xP(x,b)→xQ(x,b)计算机学 定理设c1,…cm是在Γ语句集中不出现的不同常…,ym是在公式Q(c1,…,cm)中不出现的不同变元，用…ym分别同时代替Q(c1,…cm)中的c1…cm得Q(y1,…ym。若ΓQ(c1,…cm)，则ΓQ(y1,…ym)Γ├Q(c1,…,A1Q(c1,…,…AnQ(c1,…,Q 骤~：(2)使用AkΓ对应(3)使用MP(4)使用UG

z1,…,zn是在Γ元，并且{z1,…,zn}{y1,…,yn}=A1Q(z1,…,…An(z1,…,An(z1,…,An+1=z1…znQ(z1,…,An+2=z1…znQ(z1,…,Q(y1,…,An+3=Q(y1,…,x(P(x,c)→Q(x,c)),xP(x,c)├12=3456若ΓA(x)B(x)，则ΓxA(xxmm+x

问题是什么X是自由Am+5=xA(x)x3.1逻辑公理系3.2命题逻辑公理系3.3谓词逻辑公理系3.4定理证3.5公理系统性3.6理论与模3.7判定问计算机学 ：Q,QR反证律：如果ΓQRΓQ├R,则Γ归谬律：如果ΓQRΓQ├R，则Γ计算机学 ├(P(QR))├├QQ

├├├(QR├Q(Q├(QR)├(QR)(Q计算机学 ├Q((QR)├├(PQ)((QR)(P├(QR)((QR)├(QR)((QR)├(QRR)├(PQR)(P(Q├├(PQ)(PR)(PQ├(PR)((QR)((PQ)计算机学 Q,QRA1=A2=A3=

A1ΓA2ΓA1,A2计算机学 PQ,A1=(QR)(PA3=PA4=(P(QR))((PQ)A5=(PQ)

A2ΓA1=A2A3A2A4,A3A5A6ΓA5,计算机学 例 证明A1=((QR))((PQ)(P AA2((PQ)(PR))(Q((PQ)(P AA3=(Q((PQ)(PR)))((Q(PQ))(Q(P AA4(P(QR))((Q(PQ))(Q(PA5=((((QR))((Q(PQ))(Q(P

A1A2A3(((P(QR))(Q(PQ)))(((P(QR))(Q(P AA6=((((QR))(Q(PQ)))((P(QR))(Q(PR)))A5=A4A7A8(Q(PQ))((P(QR))(Q(PA9(P(QR))(Q(PA10((QR))(Q(P

AAA8A├A6A├计算机学 例 证明├(QR)((PQA1=(QR)(P(QA2=(P(QR))((PQ)(PA3=(QR)((PQ)(P

A2A1,A2├计算机学 例 证明A1=(QR)((PQ)├(QR)((PQ(PR(例A2=((QR)((PQ)P(QR (例A3=((P A2,A1├计算机学 证明P(QR),A1=A2=(P(QR))((PQ)A3=(PQ)(PRA4=Q(PA6=A7=P

A1A2A2A├A5A4A├6A3A├计算机学 A1=((PQ)(PR))(Q((P A2= A2A3=Q(P A4=(Q((PP(QR),Q├PR(例A5=((PQ)(PR))A6=(Q(PR))

A1,A4├(P(QR))├(Q(PR))(例A7=((PQ)(PR))(P A5,A6├计算机学 证明A1=(Q A2A2=Q((QQ) A3=(Q(QQ))A4=Q

1A2├3，├计算机学 证明A1=QA2=(QQ)A3=(QQ)A4=QA5=(Q((QQ)(QA6=(QQ)(QA7=(QA8=Q

A1,A2,A3├A2A5A4├├QQ(例A6A7├计算机学 证明QA1=A2=A3=

├QQ(例A1A1├计算机学 A1=(QR) A2=(RQ) 计算机学 A

QQ(例AAA├ AAAQA7=(QQ)((QR)(Q

AA├├QQ(例A8=(QR)(Q

├(PQ)((QR)(PR))(例AA6AA计算机学 证明├(QR(RA1A2(QR)(RA3(QR)(R

├(QR)(QR)(例A2A├计算机学 证明├(QR12

├(QR(RQ)(例QQ(例3(Q├(QR)((PQ)(PR))(例45(QR)

A3A├A1,A4├计算机学 证明├(QRA1(QR A2(QQ)((QR)(QR├(PQ)((QR)(PR))(例A3(QA4(QR)(QRA5(QR)

QQR(例A2AA4,A1├计算机学 证明A1A3=QA5=QQ)(QA6(QR)

A1├A2A4A3AA5├计算机学 ├(QQ)(RQ)(例(((QQ)(QQ)) A(QQ)(QQ)

AAAAA计算机学 证明QQA1=QQA2=(QQ)A3=QQ

QR├(QQ)Q(例AA计算机学 证明A2=(QQ)(QA3=(QA4=

QQ(例├QQ(例A2A1QR≡(Q计算机学 证明A1=QA2=

QQ(例QR≡Q计算机学 Q(QA1Q(RA2(RQ)(QA3Q(Q

A1,A2├计算机学 A1A2(RQ)A3QA4A5A6(Q(QR))((QR)A7

├Q(QR)(例A4,A3├├(QR)A5,A6├A8(QR)(RA9

├(P(QR(Q(PR(例QR≡Q计算机学 证明├(QR)(QA1R(QA3Q(R(QA4(R(QR))((QA5Q((QR)

A2,A1├├(QR)(RA3,A4├A6(Q((QR)R((QR)(Q (例A7(QR)(QA8(QR)(Q

A6,A5├QR≡Q计算机学 证明├Q((QR) ├QQ(例├(P(QR))(Q(PR))(例A3 A2A├计算机学 证明A1A2

QQ(例├(P(QR))(Q(PR))(例A3((QR)R)(RA4

├(QR)AAA5A6(Q(QR))

A4;├(P(QR))(QA5;├(QR)QR≡(Q计算机学 证明├(QR)((QR)1(QQ QQQ)(例A2=((RQ)(QQ))((RQ)1├(QR((PQ(PR))(例A3=((QR)((RQ)(QQ)))((QR)((RQ)2├(QR)((PQ)(P4=(QR)((RQ)A5=(QR)((RQ)

├(PQ)((QR)(PA3A├6=(RQ)((QR)7=(QR)8=(QR)((QR)9(QR)((QR)

5├(P(QR))(Q(PR)(例AA7├8├(P(QR))计算机学 证明├(QR)((QR)1(QQ)A2=(QQ)

QQQ(例├(QR)3

AA4((RQ)(QQ))((RQ)3├(QR((PQ(PR(例5((QR)((RQ)(QQ)((QR)((RQ) 4├(QR)((PQ)(P6(QR)((RQ)(QQ)7(QR)((RQ)8(RQ)9(QR)10(QR)11(QR)

├(PQ((QR(PR(例A5=A65├(P(QR(Q(PR(例├(QR)AA810├(P(QR))(Q计算机学 证明├(QRR1(Q(RR))((R2=A3=(Q(RR))4(QRR)

├(QR)├QQ(例P(QR),QPR(例QR≡(Q计算机学 证明A1=A2=

计算机学 证明QRA1=(RQ)(QA2=((RQ)(Q3

├(RQ)(Q├(RQ)(QR)QR=(QR)4QR计算机学 证明123A4=(Q(QR))((Q5(Q6QR

A1├AAQR计算机学 证明├(QA1=(QA2=(QQ)(QA3=(QA4=(Q

QQ(例QQ(例AAQR≡计算机学 证明├(PQR(P(QA1=(PQR)(R(PQA2=(R(PQ))(R(PA3=(PQ)(PA4=(R(PQ))(R(P

├(QR)(RQR≡QQ(例A3;├(QR)((PQ)(PR))(例A5=(R(PQ))(P(R(P(QR))(Q(PR))(例A6=(RQ) A7=((RQ)(QR))((P(R(QR)((PQ)(PR))(例A8=(P(RA9=(PQR)

A6├A1A,A,A,A计算机学 A1(QR(Q ├QQ(例A2=((QR)(QR))(Q((QR)A3=Q((QR)

├(P(QR))(Q(PR))(例A,AA4=((QR)A5=Q(R(QA6=

├(QR)(RA,AQR≡计算机学 证明A1=(RQ)(Q

├(RQ)(QA2=((RQ)(QR))((QR)├(QR)A3=(QR)A4=

A,AQR≡计算机学 证明A1=A2=A3=A4=(Q(QR))A5=A6=

├A,A├A,AQR≡计算机学 证明PQ(PR(PQA1=(P(QR))((Q A2=((PQ)(PR))(P(QQR≡计算机学 ├xR(x)├xR(x)├Q(c)├Q(c)├xR(x)

├xyR(x,y)├xyR(x,y)├xyR(x,y)├xyR(x,y)├xR(x,x)├x(P(x)Q(x))(xP(x)├x(P(x)Q(x))(xP(x)├x(P(x)Q(x))(xP(x)├xP(x)xQ(x))x(P(x)├x(P(x)Q(x))(xP(x)├x(P(x)Q(x))(xP(x)计算机学 ├xP(x)├xP(x)├xP(x)├xP(x)计算机学 选择规引入规P(c)计算机学 证明xQ(xyQ(y)(y不在QA1=xQ(x)A2=y(xQ(x)A3=y(xQ(x)Q(y))(xQ(x)yA4=xQ(x)y

A4A5A,A计算机学 xR(xyR(y(y不在QA ├xQ(x)yQ(y)（例A2=(yQ(y)xQ(x))(xQ(x)├(QR)(RA(xQ(x)AxR(x)

AAxQ(x)计算机学 证明├Q(cA1=xQ(x) AA2=(xQ(x)Q(c))(Q(c)├(QR)A3=Q(c)A4Q(c)A5Q(c)A

A,A2QQ(例A,AxQ(x)计算机学 AA2=(xQ(x)Q(c))(Q(c)├(QR)(RA3=Q(c)

A,A计算机学 A1xQ(x)A2Q(c)A3xQ(x)

AQ(cxQ(x)(例A,A计算机学 证明├xyA1=xyR(x,y)yA2=yA3=xyR(x,y)A4=x(xyR(x,y)

AAA,AA5=x(xyR(x,y)R(x,y))(xyR(x,y) AA6=xyR(x,y)A7=y(xyR(x,y)

AAA8=y(xyR(x,y)xR(x,y))(xyR(x,y)yxR(x,y))AA9=(xy AA计算机学 xyR(x,yAyx├xyR(x,y)yxR(x,y)(例AxyR(x,y)A;├(QR)(RAxyR(x,y)xQ(x)AxyR(x,y)xQ(x)计算机学 xyR(x,yyxAxyR(x,y)AyR(c,y)AR(c,y)AxyR(x,y)xA

AAQ(c)xQ(x)(例38)A1AA3A6=y())A5A7=xyR(x,y) A计算机学 证明A2=yR(x,y)A3=xyR(x,y)

AAA,AA6 A,A5计算机学 xR(x,xA1A2xR(x,x)A3xR(x,x)A4xyR(x,y)A5xyR(x,y)xA6xR(x,x)x

A├(QR)(RA3A4计算机学 证明├x(P(x)Q(x))(xP(x)xA1 AA2=(P(x)Q(x))((xP(x)P(x))(xP(x)├(QR)((PQ)(PR))(例A3(x(P(x)Q(x))((xP(x)P(x))(xP(x)A,A4A5(x(P(x)Q(x))(xP(x)A6=x((x(P(x)Q(x))(xP(x)A7x(P(x)Q(x))x(xP(x)

A(P(QRQPR(例AA8=x(xP(x)Q(x))(xP(x)xA9=x(P(x)Q(x))(xP(x)x

AA,计算机学 x(P(xQ(x(xP(xAx(P(x)Q(x))(P(x)A2=

A├Q(c)xQ(x)(例A3=(Q(x)xQ(x))((P(x)Q(x))(P(x)

))A(P(x)Q(x))(P(x)A(P(x)xQ(x))(xAx(P(x)Q(x))A7=x(x(P(x)Q(x))(x

A,AA,A8=x(x(P(x)Q(x))(xQ(x)P(x)))((x(P(x)Q(x))x(xA(x(P(x)Q(x))x(x AAx(xQ(x)P(x))(xQ(x)xA(xQ(x)xP(x))(xP(x)xA12=(xP(x)xQ(x))(xP(x)xA13(x(P(x)Q(x))(xP(x)x A9,A10A11,计算机学 证明xP(x)xQ(xx(P(x)1(xP(x)xQ(x))23=(xP(x)xQ(x))4(xP(x)xQ(x))5=xQ(x)6(xP(x)xQ(x))7(xP(x)xQ(x))P(x)A8=x((xP(x)xQ(x))P(x)9x((xP(x)xQ(x))P(x)

├QRQ(例AA,├QRAA,├((PQ)(PR))(PQR)(例(xP(x)xQ(x))x(P(x) A10(xP(x)xQ(x))x(P(x)

A,A9├计算机学 证明A1xP(x) AA2xQ(x) AA3=(xP(x)xQ(x))(P(x)

PQ,RT├PRA4=x((xP(x)xQ(x))(P(x) A5=x((xP(x)xQ(x))(P(x)Q(x)))xQ(x))x(P(x)A6(xP(x)xQ(x))x(P(x) A,A计算机学 证明x(P(xQ(x(xP(xA1(xP(x)xQ(x))xP(x (例A2x(P(x)Q(x))(xP(x) A3x(P(x)Q(x))(xP(x)xQ(x))A4x(P(x)Q(x))(xP(x)A5(xP(x)xQ(x))(xP(x)A6x(P(x)Q(x))(xP(x)

(例A,A计算机学 证明├x(P(x)Q(x))(xP(x)1=xP(x) A2xQ(x) A3=xP(x)xQ(x)P(x)4P(x)Q(x)(P(x)5xP(x)xQ(x)(P(x)

PQ,RT├PRA3├6=(xP(x)xQ(x))xP(x)7(xP(x)xQ(x))(P(x)8(xP(x)xQ(x))(P(x)9=x((xP(x)xQ(x))(P(x)10(xP(x)xQ(x))x(P(x)

A6├A4A11=x(P(x)Q(x))(xP(x)1=x(P(x)Q(x))(xP(x)

├(QR)(R计算机学 3.1逻辑公理系3.2命题逻辑公理系3.3谓词逻辑公理系3.4定理证3.5公理系统性3.6理论与模3.7判定问计算机学 可靠性定理：若ΓQ，则ΓQ证明：设QΓ├Qi，有Γ╞Q，1.n=1时，若Q是公理，则Q是永真式。若Q，则├Qi，有Γ╞Qi公理模式–v(Q–––公理模式–(P(QR))((PQ)–同理v((P(QR))((PQ)公理模式–(QR)–同理v((QR)计算机学 若QiΓ，则ΓQ对于v(Γ)=1，AiΓ有v(Qi)=1，所Γ╞Q2.假设i<n3.证明i=n设Qi由QjQk用MP规则推出，其中j,k<iQk为Qj→Qi由归纳假设知ΓQjΓQjQi,所以ΓQjΓQjQi由ΓQj,ΓQjQi,所以Γ╞Qi因此当i=n时成即ΓQ计算机学 定义3.3如果对于每个公式Q，ΓQ，则Γ称不协调，否计算机学 定理3.3若ΓQQ，则Γ证明：Q∧Q等价于A1=A2=(QQ)(R(QQ)A3=RA4(R(QQ))((QQ)RA5(QQ)A6A7Γ├R（R为任意公式定理3.4若Γ协调，则Γ可满足完备性定理：若ΓQΓQ证明若真值赋值v满足Γ，则它必满足Q,即不可满足所以Γ{Q}不可满因此，Γ{Q}不协调所以有Γ{Q}├Q有演绎定理有Γ├QQ由├(QQ)Q计算机学 可靠性定理：若Γ├Q，则Γ╞Q归纳证明：对于Γ├Qi，有Γ╞Qi，1n=1时，即Qi是公理，则Qi(1)公理模式–v(Q–如果v(Q)=1，则v(Q)(v(R)v(Q))=1–如果v(Q)=0，则v(A)(v(R)v(Q))=1(2)公理模式–(P(QR))((PQ)–同理v((P(QR((PQ(3)公理模式–(QR)–同理v((QR)计算机学 (4Qi4xQQtx。–任取解释I和赋值t–若I(xQ)(v)=1，则对于每个–所以I(Qtx–这表明Qi是永真式，即Γ╞Qi计算机学 可靠性定理(3)—公理(5)设A是公理5x(QR)(QxR)。其中x是公式Q的自由–若I(xQR)则I(xQR)(Q–若(xQR))(v)=1，且I(Q)(v)=0，所以I(xQR)(Q–若(x(QR))(v)=1，且则对于任意dD，I(x(QR))(v[x/d])=1因为I(Q)(v)=1，所以I(R)(v[x/d])=1。从而I(xR)(v)=1，因此有I(x(QR)计算机学 可靠性定理(4)—MP规 –Γ╞假设i<n证明i=n,其中j,<k为→–由归纳假设知，ΓQ且Γ├Qj所以ΓQjΓQj→ΓQ–因此Γ╞即Γ计算机学 (7)证明i=n–设Q由k用UG规则推出，其中k<i，–由归纳假设知，ΓQk所以ΓQ–因为Qi=xQk，对于任意所以，I(xQk–因此Γ╞即Γ╞QUG规则：If├P(x),then计算机学 如定理3.12若Γ├P(x)∧P(x)，则Γ不协若计算机学 若Γ╞Q，则Γ├证明所以Γ{Q}不协调，即Γ├Q又因为├(QQ)所以Γ├

推论若╞Q计算机学 若Γ╞Q，则Γ├证设R是QΓ{R}├R。由演绎定理知，ΓRR，因为├(RR)R，故Γ├R，因此，Γ├Q。计算机学 (t12)…t11=t21…可靠性定若ΓQΓ完备性定若Γ╞Q，则Γ├计算机学 3.1逻辑公理系3.2命题逻辑公理系3.3谓词逻辑公理系3.4定理证3.5公理系统性3.6理论与模3.7判定问计算机学 (1).x(Q(x)(2).x(Q(x)y(Q(y)(3).xy(Q(x)Q(y)(4).xy(Q(x)Q(y)计算机学 定义：对于任意ε>0，存在N>0，对于任何n，当n>N，都有|nb|<ε，则称序列xn的极限是b，记limxn序列极限的形式表ε(ε>0N(N>0n(n>N|xn-|<limf(x)ε(ε>0δ(δ>0x(|x-x0|<δ|f(x)-计算机学 定理1若序列的极限存在，则极限值唯ε(ε>0N1(N1>0n(n>N1|xn-计算机学 证明S1=ε(ε>0N1(N1>0n(n>N1|xn-S2=a)/2S3=(ε0>0N1(N1>0n(n>N1|xn-S4=N1(N1>0n(n>N1|xn-))S5=N'1>0n(n>N'1|xn-S6n(n>N'1|xn-S7n>N'1|xn-S8=ε(ε>0N2(N2>0n(n>N2|xn-S9n>N'2|xn-S10=NmaN''S11n>Nn>S12n>Nn>S13n>N|xn-S14n>N|xn-εS15n>S16|nS17|nS18n<a+ε(取xb>S19xnS20S21=+)<S22(xnb2若序列{}有极限，则{nε(ε>0N(N>0n(n>N|xn-S1=ε(ε>0