數(shù)理邏輯-邏輯公理系統(tǒng)主要內(nèi)容邏輯公理系統(tǒng)命題邏輯公理系統(tǒng)謂詞邏輯公理系統(tǒng)定理證明公理系統(tǒng)性質(zhì)理論與模型判定問(wèn)題形式系統(tǒng)一個(gè)形式系統(tǒng)應(yīng)當(dāng)包括以下幾部分。(1)各種初始符號(hào)。初始符號(hào)是一個(gè)形式系統(tǒng)的“字母”，經(jīng)解釋后其中一部分是初始概念。(2)形成規(guī)則。規(guī)定初始符號(hào)組成各種合適符號(hào)序列的規(guī)則。經(jīng)解釋后合式符號(hào)序列是一子句，稱為系統(tǒng)里的合式公式或命題。(3)公理。把某些所要肯定的公式選出，作為推導(dǎo)其它所要肯定的公式的出發(fā)點(diǎn)，這些作為出發(fā)點(diǎn)的公式稱為公理。(4)變形規(guī)則。變形規(guī)則規(guī)定如何從公理和已經(jīng)推導(dǎo)出的一個(gè)或幾個(gè)公式經(jīng)過(guò)符號(hào)變換而推導(dǎo)出另一公式。經(jīng)過(guò)解釋，變形規(guī)則就是推理規(guī)則。應(yīng)用變形規(guī)則進(jìn)行推導(dǎo)可以得到一系列公式，這些公式經(jīng)過(guò)解釋是系統(tǒng)的定理。形式系統(tǒng)完全由一套表意符號(hào)建立，它能克服日常語(yǔ)言的歧義性，使概念、判斷、推理精確化。邏輯公理系統(tǒng)公理系統(tǒng)從一些公理出發(fā)，根據(jù)演繹法，推導(dǎo)出一系列定理，形成的演繹體系叫作公理系統(tǒng)。公理系統(tǒng)的組成：符號(hào)集；公式集公式是用于表達(dá)命題的符號(hào)串；公理集公理是用于表達(dá)推理由之出發(fā)的初始肯定命題；推理規(guī)則集推理規(guī)則是由公理及已證定理得出新定理的規(guī)則；定理集表達(dá)了肯定的所有命題。主要內(nèi)容邏輯公理系統(tǒng)命題邏輯公理系統(tǒng)謂詞邏輯公理系統(tǒng)定理證明公理系統(tǒng)性質(zhì)理論與模型判定問(wèn)題總結(jié)命題邏輯公理系統(tǒng)定義：命題邏輯的公理系統(tǒng)定義:(1).符號(hào)集合：1).命題變?cè)猀1,Q2,…Qn2).聯(lián)結(jié)詞符號(hào)：，;3).括號(hào)：(,)(2).形成規(guī)則(公式定義)：1).若Q是命題變?cè)瑒tQ是公式；2).若Q是公式，則(Q)是公式；3).若Q,R是公式，則(QR)是公式。命題邏輯公理系統(tǒng)(續(xù))(3).公理：公理模式中P,Q,R為任意公式1).公理模式A1：R(QR)2).公理模式A2：(P(QR))((PQ)(PR))3).公理模式A3：(QR)(RQ)(4).變形規(guī)則：推理規(guī)則(分離規(guī)則MP規(guī)則)若Q和QR成立，則R成立。其中，Q和QR稱為前提，R稱為結(jié)論?？s寫(xiě)定義謂詞公理系統(tǒng)中僅使用了和聯(lián)結(jié)詞符號(hào)，而其他聯(lián)結(jié)詞符號(hào),,,可以認(rèn)為是縮寫(xiě)公式，用≡表示縮寫(xiě)定義。(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——結(jié)論演繹與推理序列定義3.2設(shè)Γ是合式公式集,Q是合式公式，有推理步驟A1,A2,…An，公式序列α1,α2,…αn，其中A1=α1A2=α2….An=αn

(αn

=Q)每個(gè)αk滿足以下條件之一，(1)α是公理；(2)αkΓ；(3)有i,j<kαk=αiαj由αi,αj用MP規(guī)則推出。則稱它為Q的從Γ的一個(gè)推演(演繹),記為Γ├Q。Γ稱為推演的前提集，稱α為結(jié)論推理序列如果推理步驟序列是A1,A2,…An，則推理序列長(zhǎng)度n。推論：如果Q是公理或QΓ，則Γ├Q證明與定理如果存在從Γ推演出Q，則記為Γ├Q。{Q1,Q2,…Qn}├Q簡(jiǎn)記為Q1,Q2,…Qn├Q

如果Γ為空集，則記為├Q。如果Γ├Q，并且有推理步驟A1,A2,…An，則A1,A2,…An稱為的一個(gè)證明。如果├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

當(dāng)且僅當(dāng)Γ├QR歸納基礎(chǔ)：用關(guān)于Γ{Q}到R的推演長(zhǎng)度n作歸納證明。當(dāng)n=1時(shí)，R或?yàn)楣恚驅(qū)儆讦?，或R是Q。若R是公理，則A1=RA2=R(QR)A3=(QR)所以├QR，從而Γ├QR若RΓ，則A1=RA2=R(QR)A3=(QR)有Γ├QR若R=Q，則├

QQ所以Γ

├QQ演繹定理(2)歸納假設(shè)：假設(shè)Γ{Q}到R的推演長(zhǎng)度小于n定理成立。歸納證明：當(dāng)Γ{Q}到R的推演長(zhǎng)度等于n時(shí)，有Γ{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)因?yàn)閕,j<n,有所以Γ{Q}├PΓ├QPΓ{Q}├PRΓ├Q(PR)演繹定理(3)Γ

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

。證明有Γ{Q}├R。因?yàn)橛型评硇蛄蠥1,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主要內(nèi)容邏輯公理系統(tǒng)命題邏輯公理系統(tǒng)謂詞邏輯公理系統(tǒng)定理證明公理系統(tǒng)性質(zhì)理論與模型判定問(wèn)題總結(jié)謂詞邏輯公理系統(tǒng)謂詞邏輯的公理系統(tǒng)定義：(1).符號(hào)集合：1).個(gè)體變?cè)簒1,x2,…2).個(gè)體常元：c1,c2,…3).函詞符號(hào)：f11,f21,......；f12,f22,......；4).謂詞符號(hào)：Q11,Q21,......；Q12,Q22,....;5).運(yùn)算符號(hào)：,,；6).逗

號(hào)：,;7).括

號(hào)：(,)謂詞邏輯公理系統(tǒng)（續(xù)）(2).項(xiàng)定義：1).個(gè)體常元是項(xiàng)；2).個(gè)體變?cè)琼?xiàng)；3).若是t1,…,tn項(xiàng)，則是fkn

(t1,…,tn)項(xiàng)。(3).公式集合：1).若是t1,…,tn項(xiàng)，則Qkn

(t1,…,tn)是公式。2).若Q是公式，則(Q)是公式；3).若Q和R是公式，則(QR)是公式；4).若Q是公式，則(xQ)是公式。謂詞邏輯公理系統(tǒng)（續(xù)）(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]

其中，項(xiàng)t對(duì)于Q中的x是可代入的。

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

其中x不是Q中自由變?cè)?5).推理規(guī)則1).分離規(guī)則（簡(jiǎn)稱MP規(guī)則）：從Q和QR推出R。2).概括規(guī)則（簡(jiǎn)稱UG規(guī)則）：從Q(x)推出(xQ)。縮寫(xiě)定義謂詞公理系統(tǒng)中僅使用了和聯(lián)結(jié)詞符號(hào)，而其他聯(lián)結(jié)詞符號(hào),,,可以認(rèn)為是縮寫(xiě)公式，用≡表示縮寫(xiě)定義。(1).QR≡(QR)(2).QR≡(QR)(3).QR≡(QR)(RQ)(4).QR≡(QR)謂詞公理系統(tǒng)中僅使用了量詞，而量詞可以認(rèn)為是縮寫(xiě)公式，用≡表示縮寫(xiě)定義。xQ(x)≡Q(x)公理系統(tǒng)弗雷格公理系統(tǒng)Q(RQ)(P(QR))((PQ)(PR))(P(QR))(Q(PR))(QR)(RQ)QQQQa=b(F(a)F(b))a=axF(x)f(a)盧卡西維茨公理系統(tǒng)Q(RQ)(P(QR))((PQ)(PR))(QR)(RQ)羅素公理系統(tǒng)AAAAABABBA(AB)(ACBC)演繹與證明定義

設(shè)Γ是合式公式集,Q是合式公式，有推理步驟A1,A2,…An，公式序列α1,α2,…αn，其中A1=α1A2=α2….An=αn

(αn

=Q)每個(gè)αk滿足以下條件之一，(1)α是公理；(2)αkΓ；(3)有i,j<kαk=αiαj由αi,αj用MP規(guī)則推出。(4)有i<j使Aj=xAi由用UG規(guī)則推出則稱它為Q的從Γ的一個(gè)推演(演繹),記為Γ├Q。Γ稱為推演的前提集，稱α為結(jié)論序列A1,A2,…An，稱為從Γ演繹出αn的一個(gè)證明。Γ├αn也稱由Γ可證明αn。推理序列如果推理步驟序列是A1,A2,…An，則推理序列長(zhǎng)度n。推論：如果Q是公理或QΓ，則Γ├Q定理從系統(tǒng)的公理出發(fā)，根據(jù)系統(tǒng)允許的變形規(guī)則推得的合式公式稱為可證公式，或稱系統(tǒng)里的定理。定義：如果├Q，則Q稱為定理。設(shè)Γ是前提，Γ={Q1,...,Qn}，Q是結(jié)論，并且Γ├Q。一般講，Γ是事實(shí)知識(shí)或歸納知識(shí)。由于證明是邏輯的，公理是邏輯真，推導(dǎo)規(guī)則是邏輯真，但是，前提Γ不是邏輯真。如果實(shí)踐檢驗(yàn)Q不為真，則Γ一定有不為真語(yǔ)句。├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

當(dāng)且僅當(dāng)Γ├A→B因?yàn)锳(x)xA(x)不是有效公式，A

可證，

xA可證？？變?cè)s束變?cè)杂勺冊(cè)霈F(xiàn)約束出現(xiàn)自由出現(xiàn)演繹定理Γ{A}├B，且A為閉公式，當(dāng)且僅當(dāng)Γ├AB歸納基礎(chǔ)：用關(guān)于Γ{A}到B的推演長(zhǎng)度n作歸納證明。當(dāng)n=1時(shí)，B或?yàn)楣恚驅(qū)儆讦?，或B是A。若B是公理，則A1=BA2=B(AB)A3=(AB)所以├AB，從而Γ├AB若BΓ，則若B=A，則├

AAA1=B所以Γ├AAA2=B(AB)A3=(AB)有Γ├AB演繹定理(2)歸納假設(shè)：假設(shè)Γ{A}到B的推演長(zhǎng)度小于n定理成立。歸納證明：當(dāng)Γ{A}到B的推演長(zhǎng)度等于n時(shí)，并且B由分離規(guī)則推出有Γ{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因?yàn)閕,j<n,所以Γ{A}├RΓ├ARΓ{A}├RBΓ├A(RB)演繹定理(3)歸納證明：當(dāng)Γ{A}到B的推演長(zhǎng)度等于n時(shí)，并且B由綜合規(guī)則推出，所以從Γ的推演A1=B1......Am=ARAm+1=x(AR)Am+2=AxRA為閉公式Γ{A}├BA1=B1A2=B2……An-1=RAn=xRAn=B因?yàn)棣A}├R推演長(zhǎng)度等于n-1，所以Γ├AR演繹定理(4)Γ

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

。證明有Γ{A}├B

。因?yàn)橛型评硇蛄蠥1,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)

自由出現(xiàn)變?cè)獑?wèn)題├

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))定理

設(shè)c1,…,cm是在Γ語(yǔ)句集中不出現(xiàn)的不同常元，y1,…,ym是在公式Q(c1,…,cm)中不出現(xiàn)的不同變?cè)?，用y1,…,ym分別同時(shí)代替Q(c1,…,cm)中的c1,…,cm得到Q(y1,…,ym)。若Γ├Q(c1,…,cm)，則Γ├Q(y1,…,ym)。證明步驟A1~An：(1)使用公理模式對(duì)應(yīng);(2)使用AkΓ對(duì)應(yīng);(3)使用MP規(guī)則對(duì)應(yīng)；(4)使用UG規(guī)則對(duì)應(yīng)。證明：Γ├Q(c1,…,cm)A1=Q1(c1,…,cm)…An=Qn(c1,…,cm)An=Q

(c1,…,cm)z1,…,zn是在Γ中不出現(xiàn)的不同變?cè)⑶襸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)問(wèn)題是什么?X是自由出現(xiàn)主要內(nèi)容邏輯公理系統(tǒng)命題邏輯公理系統(tǒng)謂詞邏輯公理系統(tǒng)定理證明公理系統(tǒng)性質(zhì)理論與模型判定問(wèn)題總結(jié)重要定律三段論：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