命题逻辑的形式系统

《命题逻辑的形式系统》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

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

2、算—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）））。（附加律，或蕴析公理）第一节公理演算—P系统的出法点（3）5．推理规

3、则（或变形规则，用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）真值联结词的结合力

4、依下列次序递减：¬，∧、∨，→，↔(二）语义部分，关于符号和公式解释的理论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。对公理的解释每一条

5、公理都是本系统最基本的重言式，其真值，可用真值表方法判定。关于推理规则（1）（1）关于代入规则（R1）该规则要求只有命题变项π才能被代入，而其他多于一个符号的公式，例如¬p都不能被代入。但是，对于代入的公式B是没有限制的。另外，如果在A中的π出现不止一次，那么在代入时必须到处都用同一公式B代替，不能用不同的公式代替，也不能有的不代替。举例：设公式├A为：├p∨q→q∨pA中被代入的变项π为：q代入的公式B为：¬q合法代入（├A（π/B））：├p∨¬q→¬q∨p不合法代入：p∨¬q→q∨p（未对π在A中的所以出现即每一个q进行代替）关

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

7、式的简化。例如根据本规则，P公理可简化为：A1．├p∨p→pA2．├p→p∨qA3．├p∨q→q∨pA4．├（q→r）→（p∨q→p∨r）3．2P系统定理的证明所谓P定理的证明，乃是一有穷的公式序列A1，…，An，其中每一公式Ai（1≤i≤n）都适合以下条件之一：（1）Ai是一公理；（2）Ai是一已证定理；（3）Ai由本序列在先的一个公式经代入或置换所得到；（4）Ai由本序列在先的两个公式Aj和Ak（其形式分别为B和B→Ai，ji，ki）经分离所得到；（5）最后一个公式An是要证明的定理。定理的证明T1├（q→r）→（（p→q）

8、→（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置换T2├p→p证：1．├p→p∨q公理22．├p→p∨p1代入q/