l3命题逻辑公理化.pdf

命题逻辑的公理化
形式化与公理化
• 此前我们讨论命题逻辑,是从语义角度,非形式
化地、不严谨地进行解释性的讨论.
• 而数学传统追求的是严格的形式化、公理化系
统.
– 形式化:符号化,只有语法定义,并无语义解释.
– 公理化:从初始符号串(公理)出发,根据符号变换规则,
推导出其他符号串(定理).
具体的公理化系统:语法+语义
形式的公理化系统:语法.
– 欧氏几何就是一个经典的(具体)公理化系统.
Lu Chaojun, SJTU 2
形式系统的组成
• 形式系统的组成:
– 初始符号:可用符号的集合.
– 形成规则(wff定义):规定如何构成合法的符号串.
– 初始公式(公理):进行推导的出发点.
– 变形规则(推理规则):规定如何从几个wff经过符号变
换得出另一wff.
• 建立了形式系统,即可进行推理,从老wff产生新
的wff(定理).
– 不是所有wff都是定理.
Lu Chaojun, SJTU 3
例:一个形式系统
• 形式系统:
– 初始符号:⊕, #, ♣
– 形成规则:⊕, #, ♣的任意有限序列都是wff.
– 初始公式:令x是任一♣串,系统有唯一公理(模式)
A1: x⊕♣#x♣
– 变形规则: 令x, y, z表示任意♣串.
R1: 若x⊕y#z是定理, 则 x⊕y♣#z♣也是定理.
• 在此系统里可以证明♣♣⊕♣♣#♣♣♣♣是定理.
证明: (1) ♣♣⊕♣#♣♣♣ A1[x/♣♣]
(2) ♣♣⊕♣♣#♣♣♣♣. (1)R1
• 此系统有意义吗?
– 试试这个解释: ⊕解释为+, #解释为=.
Lu Chaojun, SJTU 4
命题逻辑的重言式公理系统
• 可以为命题逻辑的重言式建立公理系统.
– 后面将给出这个形式化公理系统A.
• 系统A的语义可以是:
– 初始符号表示有真假的命题及真值联结词;
– 初始命题(公理)是重言式;
– 从公理出发,利用推理规则,可以推导出定理,
且定理都是重言式;
– 该系统推出的都是重言式,而且能推出所有重
言式.
Lu Chaojun, SJTU 5
命题逻辑公理系统A
• 初始符号
– 命题符号: A,B,C,……
– 联结词: ¬, ∨
– 辅助符号: (, )
– 可证符号: |⎯ (后接公式,表示该公式在系统
中是可证明的)
Lu Chaojun, SJTU 6
命题逻辑公理系统A(续)
• 形成规则
(1)命题符号是公式;
(2)若α是公式, 则¬α是公式;
(3)若α和β是公式, 则(α ∨β )是公式;
(4)公式仅限于此.
Lu Chaojun, SJTU 7
命题逻辑公理系统A(续)
• 定义
D1. α ∧ β 定义为¬(¬α ∨ ¬β )
D2. α → β 定义为¬α ∨ β
D3. α ↔ β 定义为(α → β ) ∧ (β → α )
– ∧→↔作为初
始符号,并增加相应形成规则.
Lu Chaojun, SJTU 8
命题逻辑公理系统A(续)
• 公理
A1. |⎯ (P ∨ P ) → P
A2. |⎯ P → (P ∨ Q )
A3. |⎯ (P ∨ Q ) → (Q ∨ P )
A4. |⎯ (Q → R ) → ((P ∨Q ) →(P ∨R ))
Lu Chaojun, SJTU 9
命题逻辑公理系统A(续)
• 变形规则(推理规则)
R1. 代入规则:若|⎯ α, 则|⎯ α [p/β ].
(将公式α中