| 极小命题演算 minimal propositional calculus 由逻辑学家约翰森(I.Johansson)所建立的一种命题逻辑公理系统。它可以用如下的方式来表述： 1. 初始符号： (1) p1，p2，……;它们可解释为可数个命题变元。 (2) ，∨，∧，→，(，、);它们可分别解释为逻辑联结词“否定”、“析取”、“合取”、“蕴涵”以及左、右括号。 2. 形成规则： (1) p1，p2，……是公式; (2) 若A、B是公式，则A、(A∨B)、(A∧B)和(A→B)是公式。 3. 公理(A、B、C是任意的公式)： (1) A→(B →A) (2) (A→(B →C))→((A→B)→(A→C)) (3) A→(B →(A∧B)) (4) (A∧B)→A (5) (A∧B)→B (6) A→(A∨B) (7) B →(A∨B) (8) (A→C)→((B →C)→((A∨B)→C)) (9) (A→B)→((A→ B)→ A) 4. 推演规则： 分离规则：由A和A→B可推出B。 极小命题演算是直觉主义命题演算和经典命题演算的真子系统。若在极小命题演算的基础上再添加公理A→(A→B)，即为直觉主义命题演算;若在极小命题演算的基础上添加公理A→A，即为经典命题演算。 |