第八讲-命题演算系统

第六讲命题演算形式系统Lp命题演算形式系统Lp命题演算形式系统Lp；命题演算系统的可靠性；命题演算系统的完全性。命题演算系统Lp命题演算系统通常记为：P，分为公理演算系统和自然演绎推理系统，它们都是用形式语言构造出来的。所谓公理演算系统，指的是由一些基本命题（即公理）和推导规则以及由此推出的一些命题（即定理）而形成的演绎系统。所谓自然演绎系统，指的是没有公理只依赖推导规则推出一些命题（即定理）而形成的演绎系统。命题演算系统Lp形式化的公理系统又称为形式系统。一个形式系统主要由形式语言、初始公式、变形规则以及由它们得到的公式四部分组成。下面具体介绍命题演算系统。命题演算系统Lp初始符号1、命题变元：p，q，r，……；2、命题联接词：、、、、﹁；3、辅助符号：（，）。形成规则1、任何命题变元是合式公式；2、如果A是合式公式，则（﹁A）是合式公式；3、如果A、B是合式公式，则（AB）、（AB）、（AB）、（AB）是合式公式；4、只有按照1、2、3的规定形成的符号串才是合式公式。下面给出初始公式（即公理演算系统的公理）和初始规则：命题演算系统Lp初始公式AP1A→（B→A）AP2（A→（B→C））→（（A→B）→（A→C））AP3（﹁A→B）（（﹁A→﹁B）→A）初始规则（又叫变形规则）MP分离规则若├A→B且├A，则├B。SB代入规则若├A，则├A（p1/B1，p2/B2，…，pn/Bn）其中，A（p1/B1，p2/B2，…，pn/Bn）表示将A中的命题变元p1，p2，…，pn（如果有的话）处处分别换成B1，B2，…，Bn。这就是代入规则，运用代入规则时请注意，一定是处处代入。命题演算系统Lp一个使用形式语言的形式系统，通过初始公式和初始规则得到的公式就是这个系统的定理。一个形式系统的任务也就是证明这些定理的成立。下面给出系统中的一些定义。命题演算系统Lp定义3（证明的定义）LP中的证明是一个合式公式的有限序列：A1，A2，…An，且满足以下条件：对每一个Ai（1in）要么是公理，要么是由前面的公式根据变形规则得到的。定义4（A证明的定义）如果一个证明A1，A2，…An中的An=A，我们就称这个证明叫做关于A的证明，也就是A证明。定义5（定理的定义）如果有一个A证明，则称A是这个系统的定理。记作：├LPA。定理1、2的证明详见教材。命题演算系统Lp定义6（推演的定义）如果A1，A2，…An是一个满足如下条件的公式序列，则称它是以为前提的推演。条件：任一Ai（1≤i≤n）是中的元素，或者是公理，或者是由前面的公式根据变形规则得到的。定义7从到A的推演：如果A1，A2，…An是以为前提的推演，并且An=A，我们就称它是从到A的推演，或者说A是从出发得到的推论，记作：├A。如果={B}，可以记作：B├A；如果={B，C}，可以记作：B，C├A；如果=Ø，就记作：├A。从Ø出发推出A，A就是一个定理。演绎定理的证明见教材。命题演算系统的可靠性命题演算系统LP的可靠性古典的一致性系统S是一致的，当且仅当，不存在公式，和都是S-可证的。语法的一致性系统S是一致的，当且仅当，并非任一公式都是S-可证的。语义的一致性系统S是一致的，当且仅当，S的内定理都是有效的。语义一致性就是可靠性，因此，通常情况下把系统的一致性和可靠性看作是相同的。可靠性定理的证明见教材。命题演算系统的完全性古典的完全性系统S是古典完全的，当且仅当，对于任意A，或者A不可证，或者A不可证。语法的完全性系统S是语法完全的，当且仅当，把一个不可证的公式当作公理，将会导致系统的不一致。语义的完全性系统S是语义完全的，当且仅当，系统中的有效式都是S-定理，即：Aiff├A。命题演算系统的完全性命题演算系统的古典完全性和语法完全性都是显而易见的，这里我们主要证明它的语义完全性，语义完全性证明的方法有很多，我们采用极大一致集的方法来证明命题演算系统的语义完全性。具体证明过程见教材。