命题逻辑的形式系统

命题逻辑的形式系统第一页，共三十九页，2022年，8月28日第一节公理演算—P系统的出法点（1）（一）

语法部分，关于对象语言的理论。1．初始符号：（1）p，q，r，s…（2）¬，∨（3）（，）2．形成规则（π，A，B，C等为元变项）：（１）初始符号（1）中的任意符号π是一合式公式；（２）如果符号序列A是合式公式，则（¬A）是合式公式；（３）如果符号序列A和B是合式公式，则（A∨B）是合式公式；（４）只有符合以上三条的符号序列是合式公式。第二页，共三十九页，2022年，8月28日

第一节公理演算—P系统的出法点（2）

3．定义（用D表示）：D1（A→B）=Df（¬A∨B）；（蕴涵）D2（A∧B）=Df¬（¬A∨¬B）；（合取）D3（A↔B）=Df（¬A∨B）∧（¬B∨A）；（等值）4．公理（用A表示公理，用元符号表示其跟随的公式是本系统要肯定的）：A1

├

（（p∨p）→p）；（重言律，或去析公理）A2├

（p→（p∨q））；（析取引入律，或加析公理）A3├

（（p∨q）→（q∨p））；（析取交换律，或交析公理）A4├

（（q→r）→（（p∨q）→（p∨r）））。（附加律，或蕴析公理）第三页，共三十九页，2022年，8月28日第一节公理演算—P系统的出法点（3）

5．推理规则（或变形规则，用R表示）：R1（代入规则）：在一个合式公式A中，用一合式公式B代替A中某变项π的每一次出现（或将A中的π全部代以B），从而得到合式公式A（π/B）。即从A可得A（π/B）。R2（分离规则）：从A和A→B（或（¬A∨B））可得B。R3（定义置换规则）：定义两边的定义项可以互相替换。设B=DfC，A（B）为包含公式B的A公式，A（B/C）为在A中用公式C置换B的公式。即从├

A（B），可得├

A（B/C）。１．符号结合力规则：（1）公式最外面的一对括号可省略，若有不能省略的括号，其结合力最优先；（2）真值联结词的结合力依下列次序递减：

¬，∧、∨，→，↔第四页，共三十九页，2022年，8月28日(二）语义部分，关于符号和公式解释的理论2．关于形成规则例：判定¬（¬q∨r）∨¬（p∨q）∨（p∨r）是否为公式。根据规则（1），p，q，r是公式，因为它们都是字母表中的字母，都属于π，进而属于A。根据规则（2），¬q是公式，因为¬q为¬A。根据规则（3），¬q∨r，p∨q，p∨r是公式，因为它们均为A∨B。再根据规则（2），¬（¬q∨r），¬（p∨q）是公式，它们可看作是¬A。再两次根据规则（3），最后判定¬（¬q∨r）∨¬（p∨q）∨（p∨r）是公式，因为它们可看作是A∨B。第五页，共三十九页，2022年，8月28日对公理的解释每一条公理都是本系统最基本的重言式，其真值，可用真值表方法判定。第六页，共三十九页，2022年，8月28日

关于推理规则（1）

（1）关于代入规则（R1）该规则要求只有命题变项π才能被代入，而其他多于一个符号的公式，例如¬p都不能被代入。但是，对于代入的公式B是没有限制的。另外，如果在A中的π出现不止一次，那么在代入时必须到处都用同一公式B代替，不能用不同的公式代替，也不能有的不代替。第七页，共三十九页，2022年，8月28日举例：设公式├A为：├p∨q→q∨pA中被代入的变项π为：q代入的公式B为：¬q合法代入（├A（π/B））：├p∨¬q→¬q∨p不合法代入：p∨¬q→q∨p（未对π在A中的所以出现即每一个q进行代替）第八页，共三十九页，2022年，8月28日关于定义置换规则（R3）这里的置换和前面的代入是不同的。置换要求置换公式和被置换公式是等值（或可互相定义）的，而且是在被置换公式出现的某些位置上进行替换。代入则不要求代入公式和被代入公式等值，但必须在被代入公式出现的所有位置上进行替换。第九页，共三十九页，2022年，8月28日举例：设公式├A为：├p→p∨¬qA中被置换的公式B为：P∨¬q置换的公式C为：q→p（要求：B=dfC即p∨¬q↔q→p）置换后所得公式（├A（B/C））：├p→（q→p）第十页，共三十九页，2022年，8月28日关于符号省略规则根据形成规则所构造的公式，其符号过多也过于复杂。我们可以作些简化。本规则是在保证不影响原公式固有层次的前提下，对公式的简化。例如根据本规则，P公理可简化为：A1．├p∨p→pA2．├p→p∨qA3．├p∨q→q∨pA4．├（q→r）→（p∨q→p∨r）第十一页，共三十九页，2022年，8月28日

3．2P系统定理的证明

所谓P定理的证明，乃是一有穷的公式序列A1，…，An，其中每一公式Ai（1≤i≤n）都适合以下条件之一：（1）Ai是一公理；（2）Ai是一已证定理；（3）Ai由本序列在先的一个公式经代入或置换所得到；（4）Ai由本序列在先的两个公式Aj和Ak（其形式分别为B和B→Ai，ji，ki）经分离所得到；（5）最后一个公式An是要证明的定理。

第十二页，共三十九页，2022年，8月28日定理的证明T1├（q→r）→（（p→q）→（p→r））证：1.├（q→r）→（p∨q→p∨r）公理42.├（q→r）→（¬p∨q→¬p∨r）1代入p/¬p3.├（q→r）→（（p→q）→（p→r））

2定义1置换第十三页，共三十九页，2022年，8月28日T2

├p→p

证：1．├p→p∨q公理22．├p→p∨p1代入q/p3．├p∨p→p公理14、├（q→r）→（（p→q）→（p→r））定理15、├（p∨p→p）→（（p→p∨p）→（p→p））

4代入q/p∨p，r/p6．├（p→p∨p）→（p→p）5，3分离7．├p→p6，2分离第十四页，共三十九页，2022年，8月28日T3

├¬p∨p（略）T4├p∨¬p

证：1．├p∨q→q∨p公理32．├¬p∨p→p∨¬p1代入p/¬p，q/p3．├¬p∨p定理34．├p∨¬p3，2分离第十五页，共三十九页，2022年，8月28日T5├p→¬¬p（略）T6

├¬¬p→p

证：1．├p→¬¬p定理52．├¬p→¬¬¬p1代入p/¬p3．├（q→r）→（p∨q→p∨r）公理44．├（¬p→¬¬¬p）→（p∨¬p→p∨¬¬¬p）3代入q/¬p，r/¬¬¬p5．├p∨¬p→p∨¬¬¬p4，2分离6．├p∨¬p定理47．├p∨¬¬¬p5，6分离8．├p∨q→q∨p公理39．├（p∨¬¬¬p）→（¬¬¬p∨p）8代入q/¬¬¬p10．├¬¬¬p∨p9，7分离11．├¬¬p→p10定义1置换第十六页，共三十九页，2022年，8月28日T7

├（p→q）→（¬q→¬p）证：1．├p→¬¬p定理52．├q→¬¬q1代入p/q3．├（q→r）→（p∨q→p∨r）公理44．├（q→¬¬q）→（¬p∨q→¬p∨¬¬q）3代入r/¬¬q，p/¬p5．├¬p∨q→¬p∨¬¬q4，2分离6．├p∨q→q∨p公理37．├（¬p∨¬¬q）→（¬¬q∨¬p）6代入p/¬p，q/¬¬q8．├（q→r）→（（p→q）→（p→r））定理19·

├（¬p∨¬¬q→¬¬q∨¬p）→（（¬p∨q→¬p∨¬¬q）→（¬p∨q→¬¬q∨¬p）8代入q/¬p∨¬¬q，r/¬¬q∨¬p，

p/¬p∨q10．├（¬p∨q→¬p∨¬¬q）→（¬p∨q→¬¬q∨¬p）9，7分离11．├¬p∨q→¬¬q∨¬p10，5分离12．├（p→q）→（¬q→¬p）11定义1置换第十七页，共三十九页，2022年，8月28日T8

├¬（p∧q）→¬p∨¬q（略）

T9

├¬p∨¬q→¬（p∧q）

证：1．├p→¬¬p定理52．├

¬p∨¬q→¬¬（¬p∨¬q）

1代入p/¬p∨¬q3．├¬p∨¬q→¬（p∧q）

2定义2置换第十八页，共三十九页，2022年，8月28日定理的简化证明使证明简化的一个主要方法是把本系统中的公理和已证定理当作推理规则使用。这些规则称作导出规则。列举如下：1.析取交换规则：从├A∨B可得├B∨A公理32.附加规则：从├B→C可得├A∨B→A∨C。公理43.三段论规则：从├B→C和├A→B可得├A→C。定理14.假言易位规则：从├A→B可得├¬B→¬A。定理75.等值构成规则：从├A→B和├B→A可得├A↔B。定义36.等值置换规则：如果A和B等值，即├A↔B，则从├φA可得├ΦB。Φ表示任意合式公式，其中A（或B）是Φ的子公式。A，B可相互置换。这是定义置换规则的扩充。第十九页，共三十九页，2022年，8月28日导出规则27．结合括号省略规则：（1）从├（A∨B）∨C可得├A∨B∨C；（2）从├（A∧B）∧C可得├A∧B∧C。8.条件互易规则：从├A→（B→C）可得├B→（A→C）。9．合取构成规则：从├A→（B→C）可得├A∧B→C。10．条件融合规则：从├A→（A→B）可得├A→B。以上8，9，10三条规则都是相应定理的概括。

11．求否定规则：设A为一公式，A中没有→和↔出现（或已定义为¬，∨或∧），其否定式（记为A-）用以下方法可得：将∨，∧互换，同时π将和¬π互换（π为任一命题变项）。例如，p∧¬（q∨r）∧¬r，其否定式为¬p∨¬（¬q∧¬r）∨r。12．对偶规则：设A，B为两个公式，在其中→和↔不出现。A~和B~是在A和B中把∨和∧互换的结果。我们可有：（1）从├

A→B可得├

B~→A~；（2）从├

A↔B可得├

A~↔B~。第二十页，共三十九页，2022年，8月28日一些已证或待证定理的简化证明T2

├p→p证：1．├p→p∨q公理22．├p→p∨p1代入q/p3．├p∨p→p公理14．├p→p2，3三段论T4

├p∨¬p证：1．├¬p∨p公理32．├p∨¬p1析取交换第二十一页，共三十九页，2022年，8月28日简化证明（2）T6

├¬¬p→p证：1．├p→¬¬p定理52．├¬p→¬¬¬p1代入p/¬p3．├p∨¬p→p∨¬¬¬p2附加4．├p∨¬p定理45．├p∨¬¬¬p3，4分离6．├¬¬¬p∨p5析取交换7．├¬¬p→p6定义1置换T10

├p↔¬¬p证：1．├p→¬¬p定理52．├¬¬p→p定理63．├p↔¬¬p1，2等值构成第二十二页，共三十九页，2022年，8月28日简化证明（3）T7

├（p→q）→（¬q→¬p）证：1．├p∨q→q∨p公理32．├¬p∨q→q∨¬p1代入p/¬p3．├¬p∨q→¬¬q∨¬p2等值置换4．├（p→q）→（¬q→¬p）3定义置换1T11

├¬（p∧q）↔¬p∨¬q证：1．├¬（p∧q）→¬p∨¬q定理82．├¬p∨¬q→¬（p∧q）定理93．├¬（p∧q）↔¬p∨¬q1，2等值构成T12

├¬（p∨q）↔¬p∧¬q证：1．├¬（p∧q）↔¬p∨¬q定理112．├¬（p∨q）↔¬p∧¬q1对偶第二十三页，共三十九页，2022年，8月28日简化证明（4）T13

├p→q∨pT14

├p∧q→q∧pT15

├p∧q→pT16

├p∧q→qT17

├p∨（q∨r）→q∨（p∨r）T18

├p∨（q∨r）→（p∨q）∨rT19

├（p∨q）∨r→p∨（q∨r）T20

├p∧（q∧r）→（p∧q）∧rT21

├q∧（p∧r）→p∧（q∧r）T22

├p→（q→p∧q）T23

├（p→（q→r））→（q→（p→r））第二十四页，共三十九页，2022年，8月28日简化证明（5）T24

├（p→（q→r））↔（p∧q→r）T25

├（p→（p→q））↔（p→q）T26

├p∨（q∧r）↔（p∨q）∧（p∨r）T27

├p∧（q∨r）↔（p∧q）∨（p∧r）T28

├（p→q）∧（p→r）↔（p→q∧r）T29

├p↔p∨（q∧¬q∧r）T30

├p↔p∧（q∨¬q∨r）T31

├（p↔q）↔（¬p↔¬q）T32

├（p↔q）↔（¬p∨q）∧（¬q∨p）T33

├（p↔q）↔（p∧q）∨（¬p∧¬q）T34

├¬（p↔q）↔（p∧¬q）∨（¬p∧q）以上只是P系统的部分定理，请读者自证。

第二十五页，共三十九页，2022年，8月28日3．3P系统定理的演绎

令是P中的一组公式，它们可以是P中的公理或定理，也可以不是。P中以为前提的演绎是一有穷的公式序列A1，…，An，其中每一公式Ai（1≤i≤n）都适合下列条件之一：（1）Ai是一公理或定理；（2）Ai是Γ中的一个公式（记为Hyp）；（3）Ai由本序列在先的一个或两个公式根据推理规则（系统内的基本变形规则和导出规则，但对假设前提公式不得使用代入规则）而得到。如果这样一个演绎存在，我们就称该序列最后的一个公式An以为前提是可演绎的，或称An为P中的后承，记为├An。当假设前提集为空集时，P中关于空前提的演绎就是P中的一个证明。A是P中的定理，记作├A，简记成├A。第二十六页，共三十九页，2022年，8月28日演绎定理令A、B为P中任意公式，为P中任何公式集，如果{，A}├

B，那么├

A→B。意即如P中一前提集和另一前提A能推出B，那么，由本身可推出A→B。当为空集时，如果由一前提A能推出B，那么，A→B可无前提推出，即为P的定理（├

A→B）。第二十七页，共三十九页，2022年，8月28日反证定理令A为P中任意公式，为P中任何公式集，如果{，¬A}├∧¬，那么├

A。意即如果从P的一前提公式集和一命题公式A的否定推出了矛盾，则从该前提集可推出A。当为空集时，如果由一前提¬A能推出∧¬

，那么，A可无前提推出，即A为P的定理（├

A）。第二十八页，共三十九页，2022年，8月28日对P系统部分定理的演绎证明（1）T13

├p→q∨p证：1．pHyp2．p→p∨q公理23．p∨q2，1分离4．p∨q→q∨p公理35．q∨p4，3分离6．├p→q∨p1，5演绎定理（又一附加的导出规则：从p可得q∨p）第二十九页，共三十九页，2022年，8月28日演绎证明（2）T14

├p∧q→q∧p证：1．p∧qHyp2．¬（¬p∨¬q）1定义2置换3．p∨q→q∨p公理34．¬（q∨p）→¬（p∨q）3假言易位5．¬（¬p∨¬q）→¬（¬q∨¬p）4代入p/¬q，q/¬p6．¬（¬q∨¬p）5，2分离7．q∧p6定义2置换8．├

p∧q→q∧p1，7演绎定理（合取交换的导出规则：从p∧q可得q∧p）第三十页，共三十九页，2022年，8月28日演绎证明（3）T15

├p∧q→p证：1．p∧qHyp2．¬（¬p∨¬q）1定义2置换3．p→p∨q公理24．¬p→¬p∨¬q3代入p/¬p，q/¬q5．¬（¬p∨¬q）→¬¬p4假言易位（R导4）6．¬¬p5，2分离7．p6等值置换（R导6）8．├p∧q→p1，7演绎定理（导出规则：从p∧q可得p。与此相同的方法，可证定理T16├p∧q→q，得导出规则：从p∧q可得q。它们是合取分解规则）第三十一页，共三十九页，2022年，8月28日演绎证明（4）T22

├p→（q→p∧q）证：1．pHyp2．p→p定理23．p∧q→p∧q2代入p/p∧q4．¬（p∧q）∨（p∧q）3定义1置换5．（¬p∨¬q）∨（p∧q）4等值置换6．¬p∨（¬q∨（p∧q））5析取结合（R导7）7．¬q∨（p∧q）6，1分离8．q→p∧q7定义置换9．├p→（q→p∧q）1，8演绎定理（合取组合的导出规则：从p和q可得p∧q）第三十二页，共三十九页，2022年，8月28日演绎证明（5）T23

├（p→（q→r））→（q→（p→r））证：1．p→（q→r）Hyp2．qHyp3．pHyp4．q→r1，3分离5．r4，2分离6．p→r3，5演绎定理7．q→（p→r）2，6演绎定理8．├（p→（q→r））→（q→（p→r））1，7演绎定理（由于演绎定理的引入，所有已证定理都可看作是一导出规则，而且象上节导出规则中前提与结论前的断定符都可去掉。如“换头”可表示为：从p→（q→r）可得q→（p→r）。）第三十三页，共三十九页，2022年，8月28日演绎证明（6）T24

├（p→（q→r））↔（p∧q→r）该定理的证明分两步，先证前件蕴涵后件，再证后件蕴涵前件。即：证：├（p→（q→r））→（p∧q→r）1．p→（q→r）Hyp2．p∧qHyp3．p2合取分解4．q2合取分解5．q→r1，3分离6．r5，4分离7．p∧q→r2，6演绎定理8．├（p→（q→r））→（p∧q→r）1，7演绎定理（合取构成的导出规则：从p→（q→r）可得p∧q→r）第三十四页，共三十九页，2022年，8月28日演绎证明（7）再证：├（p∧q→r）→（p→（q→r））1