数理逻辑-逻辑公理系统

数理逻辑-逻辑公理系统主要内容逻辑公理系统命题逻辑公理系统谓词逻辑公理系统定理证明公理系统性质理论与模型判定问题形式系统一个形式系统应当包括以下几部分。(1)各种初始符号。初始符号是一个形式系统的“字母”，经解释后其中一部分是初始概念。(2)形成规则。规定初始符号组成各种合适符号序列的规则。经解释后合式符号序列是一子句，称为系统里的合式公式或命题。(3)公理。把某些所要肯定的公式选出，作为推导其它所要肯定的公式的出发点，这些作为出发点的公式称为公理。(4)变形规则。变形规则规定如何从公理和已经推导出的一个或几个公式经过符号变换而推导出另一公式。经过解释，变形规则就是推理规则。应用变形规则进行推导可以得到一系列公式，这些公式经过解释是系统的定理。形式系统完全由一套表意符号建立，它能克服日常语言的歧义性，使概念、判断、推理精确化。逻辑公理系统公理系统从一些公理出发，根据演绎法，推导出一系列定理，形成的演绎体系叫作公理系统。公理系统的组成：符号集；公式集公式是用于表达命题的符号串；公理集公理是用于表达推理由之出发的初始肯定命题；推理规则集推理规则是由公理及已证定理得出新定理的规则；定理集表达了肯定的所有命题。主要内容逻辑公理系统命题逻辑公理系统谓词逻辑公理系统定理证明公理系统性质理论与模型判定问题总结命题逻辑公理系统定义：命题逻辑的公理系统定义:(1).符号集合：1).命题变元Q1,Q2,…Qn2).联结词符号：，;3).括号：(,)(2).形成规则(公式定义)：1).若Q是命题变元，则Q是公式；2).若Q是公式，则(Q)是公式；3).若Q,R是公式，则(QR)是公式。命题逻辑公理系统(续)(3).公理：公理模式中P,Q,R为任意公式1).公理模式A1：R(QR)2).公理模式A2：(P(QR))((PQ)(PR))3).公理模式A3：(QR)(RQ)(4).变形规则：推理规则(分离规则MP规则)若Q和QR成立，则R成立。其中，Q和QR称为前提，R称为结论。缩写定义谓词公理系统中仅使用了和联结词符号，而其他联结词符号,,,可以认为是缩写公式，用≡表示缩写定义。(1).QR≡(QR)(2).QR≡(QR)(3).QR≡(QR)(RQ)(4).QR≡(QR)推理序列已知Q成立，

证明R→Q成立A1=Q(RQ)A1A2=Q

QΓA3=RQ推理序列Γ=Q，公式集——前提A1、A2、A3——推理序列A3——结论演绎与推理序列定义3.2设Γ是合式公式集,Q是合式公式，有推理步骤A1,A2,…An，公式序列α1,α2,…αn，其中A1=α1A2=α2….An=αn

(αn

=Q)每个αk满足以下条件之一，(1)α是公理；(2)αkΓ；(3)有i,j<kαk=αiαj由αi,αj用MP规则推出。则称它为Q的从Γ的一个推演(演绎),记为Γ├Q。Γ称为推演的前提集，称α为结论推理序列如果推理步骤序列是A1,A2,…An，则推理序列长度n。推论：如果Q是公理或QΓ，则Γ├Q证明与定理如果存在从Γ推演出Q，则记为Γ├Q。{Q1,Q2,…Qn}├Q简记为Q1,Q2,…Qn├Q

如果Γ为空集，则记为├Q。如果Γ├Q，并且有推理步骤A1,A2,…An，则A1,A2,…An称为的一个证明。如果├Q，则Q称为定理。P,Q(PR)├QRA1=PA1ΓA2=P(QP)A1A3=QPA2=A1A3

A4=Q(PR)A4

Γ

A5=(Q(PR))((QP)(QR))A2A6=(QP)(QR)A5=A4A6

A7=(QR)A6=A3A7

例：├(QR)(QQ)A1=Q(RQ)A1A2=(Q(RQ))((QR)(QQ))A2A3=(QR)(QQ)A2=A1A3├Q(QR)(涵义)A1=Q(RQ)

A1A2=(RQ)(Q→R)A3A3=Q(QR)A1，A2├A3演绎定理Γ{Q}├R

当且仅当Γ├QR归纳基础：用关于Γ{Q}到R的推演长度n作归纳证明。当n=1时，R或为公理，或属于Γ，或R是Q。若R是公理，则A1=RA2=R(QR)A3=(QR)所以├QR，从而Γ├QR若RΓ，则A1=RA2=R(QR)A3=(QR)有Γ├QR若R=Q，则├

QQ所以Γ

├QQ演绎定理(2)归纳假设：假设Γ{Q}到R的推演长度小于n定理成立。归纳证明：当Γ{Q}到R的推演长度等于n时，有Γ{Q}├RA1=Q1A2=Q2……Ai=PR……Aj=P……An=R从Γ的推演A1=D1……Am=QP……Ak=Q(PR)

Ak+1=Q(PR)((QP)(QR))Ak+2=

(QP)(QR)Ak+3=(QR)因为i,j<n,有所以Γ{Q}├PΓ├QPΓ{Q}├PRΓ├Q(PR)演绎定理(3)Γ

到QR的推演由Γ├QR可知，有推理序列A1,A2,……,Am，使得Am=QR

。证明有Γ{Q}├R。因为有推理序列A1,A2,……,Am，其中Am=QRAm+1=QAm+2=RP,Q├PQP,Q,(PQ)├Q，P,Q,

(PQ)├Q

A1=P

A1ΓA2=Q

A2ΓA3=(PQ)A3ΓA4=

(PQ)(PQ)├QQA5=PQA4=A3

A5

A6=QA5=A1

A6

所以有P,Q├(PQ)，即P,Q├PQ├(PQ)(PR)(PQR)演绎定理：(PQ)(PR)，P├QRA1=(

PQ)(PR)A1ΓA2=PA2ΓA3=(

PQ)(PR)(

PQ)├QRQA4=PQA3=A1

A4

A5=QA4=A2

A5

A6=(

PQ)(PR)(

PR)

├QRRA7=PRA6=A1

A7

A9=RA7=A2

A8

A10=QRQ,R├QR反证律如果Γ,Q├R,Γ,Q├

R,则Γ├

QA1=Q

R

Γ{Q}├R

Γ├QRA2=Q

R

Γ{Q}├R

Γ├QRA3=(QR)(RQ)

A

3

A4=RQ

A3=A2

A4

A5=QQ

A1,A4├A5A6=(QQ)Q├(QQ)Q

A7=

Q

A6=A5

A7

归谬律如果Γ,Q├R,Γ,Q├

R，则Γ├QA1=Q

R

Γ{Q}├R

Γ├QRA2=Q

R

Γ{Q}├R

Γ├QRA3=(QR)(

RQ)├(QR)(

RQ)A4=

RQA3=A1

A4

A5=QQA2,A4├A5A6=QQ├QQA7=QQA6,A5├A7A8=(QQ)Q├(QQ)Q

A9=QA8=A7

A9

定理：若Γ├R，则Γ├QR。A1=C1……Ak-1=Ck-1Ak=RΓ├RAk+1=R(QR)A1Ak+2=QRAk+1=AkAk+2Γ├Q→R定理：若Γ

├PQ

，Γ

├P(QR)

，则Γ

├PR。A1=D1……Am-1=Dm-1Am=PQ

Γ├PQ

Am+1=Dm+1……Am+n-1=Dm+n-1Am+n=P(QR)

Γ├P(QR)

Am+n+1=(P→(Q→R))→((P→Q)→(P→R))A2Am+n+2=(P→Q)→(P→R)Am+n+1=Am+nAm+n+2Am+n+3=P→RAm+n+2=AmAm+n+3主要内容逻辑公理系统命题逻辑公理系统谓词逻辑公理系统定理证明公理系统性质理论与模型判定问题总结谓词逻辑公理系统谓词逻辑的公理系统定义：(1).符号集合：1).个体变元：x1,x2,…2).个体常元：c1,c2,…3).函词符号：f11,f21,......；f12,f22,......；4).谓词符号：Q11,Q21,......；Q12,Q22,....;5).运算符号：,,；6).逗

号：,;7).括

号：(,)谓词逻辑公理系统（续）(2).项定义：1).个体常元是项；2).个体变元是项；3).若是t1,…,tn项，则是fkn

(t1,…,tn)项。(3).公式集合：1).若是t1,…,tn项，则Qkn

(t1,…,tn)是公式。2).若Q是公式，则(Q)是公式；3).若Q和R是公式，则(QR)是公式；4).若Q是公式，则(xQ)是公式。谓词逻辑公理系统（续）(4).公理集合：1).公理模式A

1：Q(RQ)2).公理模式A

2：(P(QR))((PQ)(PR))3).公理模式A3：(QR)(RQ)4).公理模式A4：xQ(x)Q(x)[x/t]

其中，项t对于Q中的x是可代入的。

5).公理模式A5：x(QR(x))(QxR(x))

其中x不是Q中自由变元。(5).推理规则1).分离规则（简称MP规则）：从Q和QR推出R。2).概括规则（简称UG规则）：从Q(x)推出(xQ)。缩写定义谓词公理系统中仅使用了和联结词符号，而其他联结词符号,,,可以认为是缩写公式，用≡表示缩写定义。(1).QR≡(QR)(2).QR≡(QR)(3).QR≡(QR)(RQ)(4).QR≡(QR)谓词公理系统中仅使用了量词，而量词可以认为是缩写公式，用≡表示缩写定义。xQ(x)≡Q(x)公理系统弗雷格公理系统Q(RQ)(P(QR))((PQ)(PR))(P(QR))(Q(PR))(QR)(RQ)QQQQa=b(F(a)F(b))a=axF(x)f(a)卢卡西维茨公理系统Q(RQ)(P(QR))((PQ)(PR))(QR)(RQ)罗素公理系统AAAAABABBA(AB)(ACBC)演绎与证明定义

设Γ是合式公式集,Q是合式公式，有推理步骤A1,A2,…An，公式序列α1,α2,…αn，其中A1=α1A2=α2….An=αn

(αn

=Q)每个αk满足以下条件之一，(1)α是公理；(2)αkΓ；(3)有i,j<kαk=αiαj由αi,αj用MP规则推出。(4)有i<j使Aj=xAi由用UG规则推出则称它为Q的从Γ的一个推演(演绎),记为Γ├Q。Γ称为推演的前提集，称α为结论序列A1,A2,…An，称为从Γ演绎出αn的一个证明。Γ├αn也称由Γ可证明αn。推理序列如果推理步骤序列是A1,A2,…An，则推理序列长度n。推论：如果Q是公理或QΓ，则Γ├Q定理从系统的公理出发，根据系统允许的变形规则推得的合式公式称为可证公式，或称系统里的定理。定义：如果├Q，则Q称为定理。设Γ是前提，Γ={Q1,...,Qn}，Q是结论，并且Γ├Q。一般讲，Γ是事实知识或归纳知识。由于证明是逻辑的，公理是逻辑真，推导规则是逻辑真，但是，前提Γ不是逻辑真。如果实践检验Q不为真，则Γ一定有不为真语句。├x(P(x)P(x))A1=P(x)P(x)QQA2=P(x)P(x)QR≡(QR)A3=x(P(x)P(x))UG├xP(x)xP(x)A1=

xP(x)P(y)A4A2=(xP(x)P(y))(P(y)

xP(x))(QR)(RQ)A3=P(y)

xP(x)A1,A2├A3A4=P(y)P(y)QQA5=P(y)xP(x)A4,A3├A5A6=xP(x)P(y)

A4A7=

xP(x)xP(x)A6,A5├A7A8=

xP(x)xP(x)

xQ(x)≡Q(x)演绎定理Γ{A}├B

当且仅当Γ├A→B因为A(x)xA(x)不是有效公式，A

可证，

xA可证？？变元约束变元自由变元出现约束出现自由出现演绎定理Γ{A}├B，且A为闭公式，当且仅当Γ├AB归纳基础：用关于Γ{A}到B的推演长度n作归纳证明。当n=1时，B或为公理，或属于Γ，或B是A。若B是公理，则A1=BA2=B(AB)A3=(AB)所以├AB，从而Γ├AB若BΓ，则若B=A，则├

AAA1=B所以Γ├AAA2=B(AB)A3=(AB)有Γ├AB演绎定理(2)归纳假设：假设Γ{A}到B的推演长度小于n定理成立。归纳证明：当Γ{A}到B的推演长度等于n时，并且B由分离规则推出有Γ{A}├BA1=B1A2=B2……An=BAi=RAj=RB从Γ的推演A1=D1……Am=ARAk=A(RB)

Ak+1=(A(RB))

((AR)

(AB))Ak+2=(AR)

(AB)Ak+3=AB因为i,j<n,所以Γ{A}├RΓ├ARΓ{A}├RBΓ├A(RB)演绎定理(3)归纳证明：当Γ{A}到B的推演长度等于n时，并且B由综合规则推出，所以从Γ的推演A1=B1......Am=ARAm+1=x(AR)Am+2=AxRA为闭公式Γ{A}├BA1=B1A2=B2……An-1=RAn=xRAn=B因为Γ{A}├R推演长度等于n-1，所以Γ├AR演绎定理(4)Γ

到AB的推演由Γ├AB可知，有推理序列A1,A2,……,Am，使得Am=AB

。证明有Γ{A}├B

。因为有推理序列A1,A2,……,Am，其中Am=ABAm+1=AAm+2=B├x(P(x)Q(x))(xP(x)xQ(x))x(P(x)Q(x))├

xP(x)xQ(x)A1=x(P(x)Q(x))A2=x(P(x)Q(x))P(x)Q(x)A3=P(x)Q(x)A4=P(x)Q(x)P(x)A5=P(x)A6=xP(x)A7=P(x)Q(x)Q(x)A8=Q(x)A9=xQ(x)A10=xP(x)xQ(x)

自由出现变元问题├

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是在Γ语句集中不出现的不同常元，y1,…,ym是在公式Q(c1,…,cm)中不出现的不同变元，用y1,…,ym分别同时代替Q(c1,…,cm)中的c1,…,cm得到Q(y1,…,ym)。若Γ├Q(c1,…,cm)，则Γ├Q(y1,…,ym)。证明步骤A1~An：(1)使用公理模式对应;(2)使用AkΓ对应;(3)使用MP规则对应；(4)使用UG规则对应。证明：Γ├Q(c1,…,cm)A1=Q1(c1,…,cm)…An=Qn(c1,…,cm)An=Q

(c1,…,cm)z1,…,zn是在Γ中不出现的不同变元，并且{z1,…,zn}{y1,…,yn}=。A1=Q1(z1,…,zm)…An=Qn(z1,…,zm)An=Q

(z1,…,zm)An+1=z1…

znQ

(z1,…,zm)An+2=z1…

znQ

(z1,…,zm)

Q

(y1,…,ym)An+3=Q

(y1,…,ym)├

x(P(x,y)→Q(x,y))→(xP(x,y)→xQ(x,y))├

x(P(x,c)→Q(x,c))→(xP(x,c)→xQ(x,c))x(P(x,c)→Q(x,c)),xP(x,c)├xQ(x,c)A1=x(P(x,c)→Q(x,c))A2=P(x,c)→Q(x,c)A3=xP(x,c)A4=P(x,c)A5=Q(x,c)A6=xQ(x,c)若Γ├A(x)B(x)，则Γ├xA(x)

xB(x)A1=C1……Am=A(x)B(x)Am+1=xA(x)A(x)Am+2=xA(x)B(x)Am+3=x(xA(x)B(x))Am+4=x(xA(x)B(x))(xA(x)xB(x))Am+5=xA(x)xB(x)问题是什么?X是自由出现主要内容逻辑公理系统命题逻辑公理系统谓词逻辑公理系统定理证明公理系统性质理论与模型判定问题总结重要定律三段论：Q,QR├R传递律：PQ,QR├PR反证律：如果Γ,Q├R,Γ,Q├R,则Γ├Q归谬律：如果Γ,Q├R,Γ,Q├R，则Γ├Q重要定理├(P(QR))(Q(PR))├(QR)((PQ)(PR))├(PQ)((QR)(PR))├((PQ)(PR))(P(QR)├QQ├QQ├QQ├QQQ├(QQ)├(QQ)├(QR)(QR)├(QR)(QR)├(QR)(RQ)├(QR)(RQ)├(QR)(RQ)├Q(QR)├(QQ)(RQ)├(QQ)Q├(QR)(RQ)├(QR)(QR)重要定理├Q((QR)R)├Q(QR)R├(PQ)((QR)(PR))├(QR)((QR)Q)├(QR)((QR)Q)├(QRR)Q├(PQR)(P(QR))├Q(R(QR))├(PQ)(PR)(PQR)├(PR)((QR)((PQ)R))

三段论Q,QR├RA1=QRA1

ΓA2=QA2

ΓA3=RA1=A2

A3

传递律PQ,QR├PRA1=(QR)(P(QR))A1A2=QRA2

ΓA3=P(QR)A1=A2

A3

A4=(P(QR))((PQ)(PR))A2A5=(PQ)(PR)A4=A3

A5A6=(PQ)A6

ΓA7=(PR)A5=A6→A7├(P(QR))(Q(PR))A1=(P(QR))((PQ)(PR))A

2A2=((PQ)(PR))(Q((PQ)(PR)))A

1A3=(Q((PQ)(PR)))((Q(PQ))(Q(PR)))A

2A4=((P(QR))

((Q(PQ))(Q(PR))))A1,A2,A3├A4A5=((P(QR))

((Q(PQ))(Q(PR))))((P(QR))(Q(PQ))(P(QR))(Q(PR)))A

2A6=((P(QR))(Q(PQ))(P(QR))(Q(PR))A5=A4

A6A7=Q(PQ)A

1A8=(Q(PQ))((P(QR))(Q(PQ)))A

1A9=(P(QR))(Q(PQ))A8=A7

A9A10=(P(QR))(Q(PR))A6=A9

A10├(QR)((PQ)(PR))A1=(QR)(P(QR))A1A2=(P(QR))((PQ)(PR))A2A3=(QR)((PQ)(PR))

A1,

A2├

A3├(PQ)((QR)(PR))A1=(QR)((PQ)(PR))├(QR)((PQ)(PR))A2=((QR)((PQ)(PR)))((PQ)((QR)(PR)))

├(P(QR))(Q(PR))A3=((PQ)((QR)(PR)))A2=A1

A3P(QR),Q├PRA1=P(QR)A1

ΓA2=(P(QR))((PQ)(PR))A2A3=(PQ)(PR)A2=A1

A3A4=Q(PQ)A1A5=QA5

ΓA6=PQA4=A5

A6A7=PRA3=A6

A7├((PQ)(PR))(P(QR)A1=((PQ)(PR))(Q((PQ)(PR)))A1A2=(Q((PQ)(PR)))((Q(PQ))(Q(PR)))A2A3=Q(PQ)A1A4=(Q((PQ)(PR)))(Q(PR))

P(QR),Q├PRA5=

((PQ)(PR))(Q(PR))A1,

A4├

A5A6=(Q(PR))(P(QR))(P(QR))├(Q(PR))

A7=((PQ)(PR))(P(QR))A5,

A6├

A7├QQA1=(Q((QQ)Q))((Q(QQ)(QQ)

A2A2=Q((QQ)Q))A1A3=(Q(QQ))(QQ)A1=A2A3A4=Q(QQ)A1A5=QQ

A3=A4A5├QQA1=Q(QQ)A1A2=

(QQ)(QQ)A3A3=(QQ)(QQ)A3A4=Q(QQ)A1,

A2,A3├A4A5=(Q(QQ))

((QQ)(QQ))A2A6=(QQ)(QQ)A5=A4

A6

A7=(QQ)├QQA8=QQA6=A7

A8

├QQA1=(QQ)(QQ)A3A2=(QQ)

├QQA3=(QQ)(QQ)A3A4=QQA3=A2

A4

├(QR)(QR)A1=(QR)(RQ)A3

A2=(RQ)(QR)A3├(QR)(QR)A1=RR├QQA2=(RR)(Q(RR))A

1A3=Q(RR)A2=A1

A3A4=(Q(RR))((QR)(QR))A

2A5=(QR)(QR)A4=A3

A5A6=QQ├QQA7=(Q

Q)((QR)(QR))

├(P

Q)((QR)(PR))A8=(QR)(Q

R)A7=A6

A8A9=(QR)(QR)A8,A5├A9├(QR)(RQ)A1=

(QR)(QR)├(QR)(QR)A2=

(QR)(RQ)

A3A3=(QR)(RQ)A2=A1

A3

├(

QR

)(RQ)A1=(QR)(RQ)├(QR)(RQ)A2=QQ

├QQA3=(QQ)((RQ)(RQ))

├(QR)((PQ)(PR))A4=(RQ)(RQ)A3=A2

A4A5=(QR)(RQ)A1,

A4├

A5├(QR

)(RQ)A1=(QR)(RQ)

A3A2=

(QQ)((QR)(QR))├(PQ)((QR)(PR))A3=

(QQ)├(QQ)A4=(QR)(QR)A2=A3

A4A5=(QR)(RQ)A4,

A1├

A5├(QQ)(RQ)A1=Q(RQ)A1A2=(RQ)(QR)A3A3=Q(QR)A1,A2├A3A4=(Q(QR))((QQ)(QR))A2A5=(QQ)(QR)A4=A3

A5A6=(QR)(RQ)A3A7=(QQ)(RQ)A5,A6├A7├(QQ)QA1=(QQ)((QQ)Q)├(QQ)(RQ)A2=((QQ)((QQ)Q))

(((QQ)(QQ))((QQ)Q)))A2A3=((QQ)(QQ))((QQ)Q)A2=A1

A3A4=(QQ)

(QQ)A1A5=(QQ)QA3=A4

A5├QQQA1=QQ(QQ)QQ≡(QR)A2=(QQ)Q├(QQ)QA3=QQQA1,A2├A3├(QQ)A1=QQ├

QQA2=(QQ)(QQ)├

QQA3=(QQ)A2=A1

A3A4=(QQ)QR≡(QR)├(QQ)A1=QQ├

QQA2=(QQ)

QR≡QR

├Q(QR)A1=Q(R

Q)A1A2=(R

Q)(QR)A3A3=Q(QR)A1,

A2├

A3├(QR)(RQ)A1=

Q(RQ)A1A2=(RQ)(QR)A3A3=

Q(QR)

├Q(QR)

A4=(Q(QR))(R(Q(QR)))A1A5=

R(Q(QR))A4=A3

A5A6=(Q(QR))((QR)Q)

├(QR)(RQ)A7=R((QR)Q)A5,

A6├

A7A8=(QR)(RQ)

├(P(QR))(Q(PR))A9=(QR)(RQ)

QR≡QR├(QR)(QR)A1=R(QR)A1A2=(R(QR))(Q(R(QR)))A1A3=Q(R(QR))A2=A1

A3A4=(R(QR))((QR)R)

├(QR)(RQ)A5=Q((QR)R)A3,

A4├

A5A6=(Q((QR)R))((QR)(QR))

├(QR)(RQ)A7=(QR)(QR)A6=A5

A7A8=(QR)(QR)

QR≡QR├Q((QR)R)A1=(QR)(QR)├QQA2=((QR)(QR))(Q((QR)R))

├(P(QR))(Q(PR))A3=Q((QR)R)A2=A1

A3├Q(QR)RA1=

(QR)(QR)

├QQA2=Q((QR)R)

├(P(QR))(Q(PR))A3=((QR)R)(R

(QR))

├(QR)(RQ)A4=Q(R(QR))A2,A3├A4A5=

R(Q(QR))

A4;├(P(QR))(Q(PR))

A6=

(Q(QR))RA5;├(QR)(RQ)A7=Q(QR)RQR≡(QR)├(QR)((QR)Q)A1=(QQ)Q

├(QQ)Q

A2=((RQ)(QQ))((RQ)Q)

A1;├(QR)((PQ)(PR))A3=((QR)((RQ)(QQ)))((QR)((RQ)Q))A2;├(QR)((PQ)(PR))A4=(QR)((RQ)(QQ))├(PQ)((QR)(PR))A5=(QR)((RQ)Q)A3=A4

A5A6

=(RQ)((QR)Q)A5;├(P(QR))(Q(PR))A7

=(QR)(RQ)A3A8=(QR)((QR)Q)A7,A6├A8A9=(QR)((QR)Q)A8;├(P(QR))(Q(PR))├(QR)((QR)Q)A