第六讲 命题演算系统.ppt

第六讲
命题演算形式系统Lp
命题演算形式系统Lp
命题演算形式系统Lp;
命题演算系统的可靠性;
命题演算系统的完全性。
命题演算系统Lp
命题演算系统通常记为:P,分为公理演算系统和自然演绎推理系统,它们都是用形式语言构造出来的。所谓公理演算系统,指的是由一些基本命题(即公理)和推导规则以及由此推出的一些命题(即定理)而形成的演绎系统。所谓自然演绎系统,指的是没有公理只依赖推导规则推出一些命题(即定理)而形成的演绎系统。
命题演算系统Lp
形式化的公理系统又称为形式系统。一个形式系统主要由形式语言、初始公式、变形规则以及由它们得到的公式四部分组成。下面具体介绍命题演算系统。
命题演算系统Lp
初始符号
1、命题变元:p,q,r,……;
2、命题联接词: ∧,∨,→,,﹁;
3、辅助符号:(,)。
形成规则
1、任何命题变元是合式公式;
2、如果A是合式公式,则(﹁A)是合式公式;
3、如果A、B是合式公式,则(A ∧ B)、(A ∨ B)、(A → B)、(A  B)是合式公式;
4、只有按照1、2、3的规定形成的符号串才是合式公式。
命题演算系统Lp
下面给出初始公式(即公理演算系统的公理)和初始规则:
初始公式
AP1 A→(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是这个系统的定理。记作:├LP A。
定理1 ├ A→A
证明:
(1) A →(B → A) AP1
(2) A →((A → A ) → A) (1)SB
(3)(A →(B → C)) →((A → B) →(A → C)) AP2
(4)A →((A → A ) → A) →((A →(A → A)) →(A → A)) (3)SB
(5)(A →(A → A)) →(A → A) (2)(4)MP
(6)A →(A → A) (1)SB
(7)A → A (5)(6)MP
命题演算系统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就是一个定理。
演绎定理的证明见教材。