命题逻辑公理化.ppt

命题逻辑公理化
第一页，共15页
形式化与公理化
此前我们讨论命题逻辑,是从语义角度,非形式化地、不严谨地进行解释性的讨论.
而数学传统追求的是严格的形式化、公理化系统.
形式化:符号化,只有语法定义,并无语义解释.
公理化:从初始符号串(公理)出发,根据符号变换规则,推导出其他符号串(定理).
具体的公理化系统:语法+语义
形式的公理化系统:语法.
欧氏几何就是一个经典的公理化系统.
Lu Chaojun, SJTU
*
第二页，共15页
形式系统的组成
形式系统组成:
初始符号:可用符号的集合.
形成规则(wff定义):规定如何构成合法的符号串(wff).
初始公式(公理):进行推导的出发点.
变形规则(推理规则):规定如何从几个wff经过符号变换得出另一wff.
建立了形式系统,即可进行推理,从老wff产生新的wff(定理).
不是所有wff都是定理.
Lu Chaojun, SJTU
*
第三页，共15页
例:一个形式系统
形式系统:
初始符号:, , 
形成规则:, , 的任意有限序列都是wff.
初始公式:令x是任一串,系统有唯一公理(模式)
A1: xx
变形规则: 令x, y, z表示任意串.
R1: 若xyz是定理, 则 xyz也是定理.
在此系统里可以证明是定理.
证明: (1)  A1[x/]
(2) . (1)R1
此系统有意义吗?
试试这个解释: 解释为+, 解释为=.
Lu Chaojun, SJTU
*
第四页，共15页
命题逻辑的重言式公理系统
命题逻辑的重言式可组成一个公理系统.
:
初始符号表示有真假的命题及真值联结词;
初始命题是重言式;
从公理出发,利用推理规则,
该系统推出的都是重言式,而且能推出所有重言式.
Lu Chaojun, SJTU
*
第五页，共15页
命题逻辑公理系统
初始符号
命题符号: A,B,C,……
联结词: , 
辅助符号: (, )
可证符号: | (后接公式,表示该公式在系统中是可证明的)
Lu Chaojun, SJTU
*
第六页，共15页
命题逻辑公理系统(续)
形成规则
(1)命题符号是公式;
(2)若是公式, 则是公式;
(3)若和是公式, 则 是公式;
(4)公式仅限于此.
Lu Chaojun, SJTU
*
第七页，共15页
命题逻辑公理系统(续)
定义
D1.    定义为(   )
D2.    定义为  
D3.    定义为(   )  (   )
作为初始符号,并增加相应形成规则.
Lu Chaojun, SJTU
*
第八页，共15页
命题逻辑公理系统(续)
公理
A1. | (P  P )  P
A2. | P  (P  Q )
A3. | (P  Q )  (Q  P )
A4. | (Q  R )  ((P Q ) (P R ))
Lu Chaojun, SJTU
*
第九页，共15页
命题逻辑公理系统(续)
变形规则(推理规则)
R1. 代入规则:若| , 则|  [p/ ].
(将公式中的某符号p处处代以公式, 称为代入,结果记作 [p/ ].)
R2. 分离规则:若| , |  , 则| .
R3. 置换规则:施以置换后得到公式. 若| , 则| .
Lu Chaojun, SJTU
*
第十页，共15页