L3命题逻辑公理化.ppt

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