命题逻辑的形式系统.ppt

《命题逻辑的形式系统.ppt》由会员分享，可在线阅读，更多相关《命题逻辑的形式系统.ppt（39页珍藏版）》请在三一办公上搜索。

1、第五章 命题逻辑的形式系统,第一节 公理演算P系统的出发点第二节 P系统定理的证明第三节 P系统定理的演绎第四节 自然演算NP系统第五节 命题逻辑的系统特征,第一节 公理演算P系统的出法点（1）,（一）语法部分，关于对象语言的理论。1初始符号：（1）p，q，r，s（2），（3）（，）2形成规则（，A，B，C等为元变项）：（）初始符号（1）中的任意符号是一合式公式；（）如果符号序列A是合式公式，则（A）是合式公式；（）如果符号序列A和B是合式公式，则（AB）是合式公式；（）只有符合以上三条的符号序列是合式公式。,第一节 公理演算P系统的出法点（2）,3定义（用D表示）：D1（AB）=Df（AB）

2、；（蕴涵）D2（AB）=Df（AB）；（合取）D3（AB）=Df（AB）（BA）；（等值）4公理（用A表示公理，用元符号表示其跟随的公式是本系统要肯定的）：A1（pp）p）；（重言律，或去析公理）A2（p（pq）；（析取引入律，或加析公理）A3（pq）（qp）；（析取交换律，或交析公理）A4（qr）（pq）（pr）。（附加律，或蕴析公理）,第一节 公理演算P系统的出法点（3）,5推理规则（或变形规则，用R表示）：R1（代入规则）：在一个合式公式A中，用一合式公式B代替A中某变项的每一次出现（或将A中的全部代以B），从而得到合式公式A（/B）。即从A可得A（/B）。R2（分离规则）：从A和AB（

3、或（AB）可得B。R3（定义置换规则）：定义两边的定义项可以互相替换。设B=DfC，A（B）为包含公式B的A公式，A（B/C）为在A中用公式C置换B的公式。即从 A（B），可得 A（B/C）。符号结合力规则：（1）公式最外面的一对括号可省略，若有不能省略的括号，其结合力最优先；（2）真值联结词的结合力依下列次序递减：，、，,(二）语义部分，关于符号和公式解释的理论,2关于形成规则例：判定（qr）（pq）（pr）是否为公式。根据规则（1），p，q，r是公式，因为它们都是字母表中的字母，都属于，进而属于A。根据规则（2），q是公式，因为q为A。根据规则（3），qr，pq，pr是公式，因为它们均为A

4、B。再根据规则（2），（qr），（pq）是公式，它们可看作是A。再两次根据规则（3），最后判定（qr）（pq）（pr）是公式，因为它们可看作是AB。,对公理的解释,每一条公理都是本系统最基本的重言式，其真值，可用真值表方法判定。,关于推理规则（1）,（1）关于代入规则（R1）该规则要求只有命题变项才能被代入，而其他多于一个符号的公式，例如p都不能被代入。但是，对于代入的公式B是没有限制的。另外，如果在A中的出现不止一次，那么在代入时必须到处都用同一公式B代替，不能用不同的公式代替，也不能有的不代替。,举例：,设公式A为：pqqpA中被代入的变项为：q代入的公式B为：q合法代入（A（/B）：pq

5、qp不合法代入：pqqp（未对在A中的所以出现即每一个q进行代替）,关于定义置换规则（R3）,这里的置换和前面的代入是不同的。置换要求置换公式和被置换公式是等值（或可互相定义）的，而且是在被置换公式出现的某些位置上进行替换。代入则不要求代入公式和被代入公式等值，但必须在被代入公式出现的所有位置上进行替换。,举例：,设公式A为：ppqA中被置换的公式B为：Pq置换的公式C为：qp（要求：B=dfC即pqqp）置换后所得公式（A（B/C）：p（qp）,关于符号省略规则,根据形成规则所构造的公式，其符号过多也过于复杂。我们可以作些简化。本规则是在保证不影响原公式固有层次的前提下，对公式的简化。例如根

6、据本规则，P公理可简化为：A1pppA2ppqA3pqqpA4（qr）（pqpr）,32 P系统定理的证明,所谓P定理的证明，乃是一有穷的公式序列A1，An，其中每一公式Ai（1in）都适合以下条件之一：（1）Ai是一公理；（2）Ai是一已证定理；（3）Ai由本序列在先的一个公式经代入或置换所得到；（4）Ai由本序列在先的两个公式Aj和Ak（其形式分别为B和BAi，ji，ki）经分离所得到；（5）最后一个公式An是要证明的定理。,定理的证明,T1（qr）（pq）（pr）证：1.（qr）（pqpr）公理42.（qr）（pqpr）1代入p/p3.（qr）（pq）（pr）2定义1置换,T2 pp,证

7、：1ppq 公理22ppp 1代入q/p3ppp 公理14、（qr）（pq）（pr）定理15、（ppp）（ppp）（pp）4代入q/pp，r/p6（ppp）（pp）5，3分离7pp 6，2分离,T3 pp（略）T4 pp,证：1pqqp 公理32pppp 1代入p/p，q/p3pp 定理34pp 3，2分离,T5 pp（略）T6 pp,证：1pp 定理52pp 1代入p/p3（qr）（pqpr）公理44（pp）（pppp）3代入q/p，r/p5pppp 4，2分离6pp 定理47pp 5，6分离8pqqp 公理39（pp）（pp）8代入q/p10pp 9，7分离11pp 10定义1置换,T7（

8、pq）（qp）,证：1pp 定理52qq 1代入p/q3（qr）（pqpr）公理44（qq）（pqpq）3代入r/q，p/p5pqpq 4，2分离6pqqp 公理37（pq）（qp）6代入p/p，q/q8（qr）（pq）（pr）定理19（pqqp）（pqpq）（pqqp）8代入q/pq，r/qp，p/pq10（pqpq）（pqqp）9，7分离11pqqp 10，5分离12（pq）（qp）11定义1置换,T8（pq）pq（略）T9 pq（pq）,证：1pp 定理52 pq（pq）1代入p/pq3pq（pq）2定义2置换,定理的简化证明,使证明简化的一个主要方法是把本系统中的公理和已证定理当作推理

9、规则使用。这些规则称作导出规则。列举如下：1.析取交换规则：从AB可得BA公理32.附加规则：从BC可得ABAC。公理43.三段论规则：从BC和AB可得AC。定理14.假言易位规则：从AB可得BA。定理75.等值构成规则：从AB和BA可得AB。定义36.等值置换规则：如果A和B等值，即AB，则从A可得B。表示任意合式公式，其中A（或B）是的子公式。A，B可相互置换。这是定义置换规则的扩充。,导出规则2,7结合括号省略规则：（1）从（AB）C可得ABC；（2）从（AB）C可得ABC。8.条件互易规则：从A（BC）可得B（AC）。9合取构成规则：从A（BC）可得ABC。10条件融合规则：从A（AB

10、）可得AB。以上8，9，10三条规则都是相应定理的概括。11求否定规则：设A为一公式，A中没有和出现（或已定义为，或），其否定式（记为A-）用以下方法可得：将，互换，同时将和互换（为任一命题变项）。例如，p（qr）r，其否定式为p（qr）r。12对偶规则：设A，B为两个公式，在其中和不出现。A和B是在A和B中把和互换的结果。我们可有：（1）从 AB可得 BA；（2）从 AB可得 AB。,一些已证或待证定理的简化证明,T2 pp证：1ppq 公理22ppp 1代入q/p3ppp 公理14pp 2，3三段论T4 pp证：1pp 公理32pp 1析取交换,简化证明（2）,T6 pp证：1pp 定理5

11、2pp 1代入p/p3pppp 2附加4pp 定理45pp 3，4分离6pp 5析取交换7pp 6定义1置换T10 pp证：1pp 定理52pp 定理63pp 1，2等值构成,简化证明（3）,T7（pq）（qp）证：1pqqp 公理32pqqp 1代入p/p3pqqp 2等值置换4（pq）（qp）3定义置换1T11（pq）pq证：1（pq）pq 定理82pq（pq）定理93（pq）pq 1，2等值构成T12（pq）pq证：1（pq）pq 定理112（pq）pq 1对偶,简化证明（4）,T13 pqpT14 pqqpT15 pqpT16 pqqT17 p（qr）q（pr）T18 p（qr）（pq

12、）rT19（pq）rp（qr）T20 p（qr）（pq）rT21 q（pr）p（qr）T22 p（qpq）T23（p（qr）（q（pr）,简化证明（5）,T24（p（qr）（pqr）T25（p（pq）（pq）T26 p（qr）（pq）（pr）T27 p（qr）（pq）（pr）T28（pq）（pr）（pqr）T29 pp（qqr）T30 pp（qqr）T31（pq）（pq）T32（pq）（pq）（qp）T33（pq）（pq）（pq）T34（pq）（pq）（pq）以上只是P系统的部分定理，请读者自证。,33 P系统定理的演绎,令是P中的一组公式，它们可以是P中的公理或定理，也可以不是。P中以为前提

13、的演绎是一有穷的公式序列A1，An，其中每一公式Ai（1in）都适合下列条件之一：（1）Ai是一公理或定理；（2）Ai是中的一个公式（记为Hyp）；（3）Ai由本序列在先的一个或两个公式根据推理规则（系统内的基本变形规则和导出规则，但对假设前提公式不得使用代入规则）而得到。如果这样一个演绎存在，我们就称该序列最后的一个公式An以为前提是可演绎的，或称An为P中的后承，记为An。当假设前提集为空集时，P中关于空前提的演绎就是P中的一个证明。A是P中的定理，记作A，简记成A。,演绎定理,令A、B为P中任意公式，为P中任何公式集，如果，A B，那么 AB。意即如P中一前提集和另一前提A能推出B，那么

14、，由本身可推出AB。当为空集时，如果由一前提A能推出B，那么，AB可无前提推出，即为P的定理（AB）。,反证定理,令A为P中任意公式，为P中任何公式集，如果，A，那么 A。意即如果从P的一前提公式集和一命题公式A的否定推出了矛盾，则从该前提集可推出A。当为空集时，如果由一前提 A能推出，那么，A可无前提推出，即A为P的定理（A）。,对P系统部分定理的演绎证明（1）,T13 pqp证：1p Hyp2ppq 公理23pq 2，1分离4pqqp 公理35qp 4，3分离6pqp 1，5演绎定理（又一附加的导出规则：从p可得qp）,演绎证明（2）,T14 pqqp证：1pq Hyp2（pq）1定义2置

15、换3pqqp 公理34（qp）（pq）3假言易位 5（pq）（qp）4代入p/q，q/p6（qp）5，2分离7q p 6定义2置换8 pqqp 1，7演绎定理（合取交换的导出规则：从pq可得qp）,演绎证明（3）,T15 pqp证：1pq Hyp2（pq）1定义2置换3ppq 公理24ppq 3代入p/p，q/q5（pq）p 4假言易位（R导4）6p 5，2分离7p 6等值置换（R导6）8pqp 1，7演绎定理（导出规则：从pq可得p。与此相同的方法，可证定理T16pqq，得导出规则：从pq可得q。它们是合取分解规则）,演绎证明（4）,T22 p（qpq）证：1p Hyp2pp 定理23pqp

16、q 2代入p/pq4（pq）（pq）3定义1置换5（pq）（pq）4等值置换6p（q（pq）5析取结合（R导7）7q（pq）6，1分离8qpq 7定义置换9p（qpq）1，8演绎定理（合取组合的导出规则：从p和q可得pq）,演绎证明（5）,T23（p（qr）（q（pr）证：1p（qr）Hyp2q Hyp3p Hyp4qr 1，3分离5r 4，2分离6pr 3，5演绎定理7q（pr）2，6演绎定理8（p（qr）（q（pr）1，7演绎定理（由于演绎定理的引入，所有已证定理都可看作是一导出规则，而且象上节导出规则中前提与结论前的断定符都可去掉。如“换头”可表示为：从p（qr）可得q（pr）。）,演绎

17、证明（6）,T24（p（qr）（pqr）该定理的证明分两步，先证前件蕴涵后件，再证后件蕴涵前件。即：证：（p（qr）（pqr）1p（qr）Hyp2pq Hyp3p 2合取分解4q 2合取分解5qr 1，3分离6r 5，4分离7pqr 2，6演绎定理8（p（qr）（pqr）1，7演绎定理（合取构成的导出规则：从p（qr）可得pqr）,演绎证明（7）,再证：（pqr）（p（qr）1pqr Hyp2p Hyp3q Hyp4pq 2，3合取组合5r 1，4分离6qr 3，5演绎定理7p（qr）2，6演绎定理8（pqr）（p（qr）1，7演绎定理,35 命题逻辑的系统特征,当我们把命题演算系统作为研究对

18、象时，我们考察的是形式不同的各命题逻辑系统共同的特征，也称元逻辑问题，即一命题逻辑系统的所有可证公式或者说定理是否都是重言式，即可证的是否都是真的？这个问题称作系统的一致性问题。另一个问题是，是否所有命题逻辑的重言式都在一命题逻辑系统中可证，即真的是否都可证？这个问题称作系统的完全性问题。另外还有公理独立性问题，即一公理系统的每条公理，彼此应该互相独立，不能由一个公理而推出另一个公理；各演算系统间的关系问题，如P系统和NP系统是等价的，即两系统的定理集是相同的，相对于某些给出的推理规则，能彼此证明对方的公理和定理的是自己的公理或定理。以下我们仅考察一致性、完全性和独立性问题。,（一）一致性,一

19、命题逻辑的形式系统是一致的，即该系统的所有定理都是重言式（语义一致）。或者说并非该系统的一切公式都是定理（语法一致）。或者说对于该系统的任一公式A而言，A和A至少有一个不是该系统中的定理（古典的语法一致）。如何能确定或证明一个命题演算系统的所有定理都是重言式？通常的方法是为该系统找到一个解释，使得：（1）命题演算的公理都是真命题（重言式）；（2）应用命题演算的推理规则和定义，都能保证从重言式只能推出重言式。如果条件（1）、（2）都满足了，应用该推理规则从公理所推出的所有定理也是重言式，则证明了该系统是（语义）一致的。,（二）完全性,一命题逻辑的形式系统是完全的，即一切重言式都在该系统中可证（广义的、相对的或语义的完全性）。或者说，如果把在该系统不可证的公式作为新公理引进该系统，就会导致矛盾而使该系统不一致（狭义的、绝对的或语法的完全性）。或者说，对于该系统任一合式公式A而言，或者A是可证的，或者A是可证的（古典的完全性）。可以证明P系统是语义完全的和语法完全的。,（三）独立性,所谓独立性就是公理的不可推出性。根据给定的推理规则，如果从一类公式推不出某一特定公式，那么这一公式对于那一类公式就是独立的。不过，若应用某些推理规则推不出来，而用另一些推理规则就可能推出来。所以，独立性总是相对于已给定的推理规则而言的。可以证明P系统的公理都是独立的。,