1.初始符号
(1) 符号π是合式公式。 (π取值A, B, …) (2) 若A是合式公式, 则 ![]() (3) 若A, B是合式公式, 则(A∧B), (A∨B), (A→B), (A ![]() (4) 只有符号(1) (2) (3)的符号序列才是合式公式。 (5) 任何合式公式是公式串, 空符号串也是公式串。 (6) 如果α和β是公式串, 则α,β和β,α也是公式串(两者不加区分)。 (7) 只有由(5)(6)形成的符号串才是公式串。 3. 定义 (1) 相继式。如果α和β都是公式串, 则称 ![]() 是相继式。α为前件, β为后件。 (2) 规定 ![]() ![]() (3) 相继式α→β为真, 便以 ![]() 4. 公理 如果公式串α和β中的公式都仅只是命题变项A, B, …(不再有联结词了), 则 ![]() 使用该算法证明定理, 总是把公式串中的各公式使用推理规则化成不再有联结词的形式。如A, B, ![]() ![]() ![]() ![]() A∧B∧C→B∨D 为真, 由于B出现在→的两侧, 这蕴涵式必真。 5. 变形(推理)规则 共有十条, 都是针对联结词的消除(如果反向使用这些规则)而建立的。其中有五条前件规则和五条后件规则。 |