命题演算的推理理论

公理系统的组成公式

  1. 公理(极其重要)
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    公理1: P → P
    公理2: (P → (Q → R)) → (Q → (P → R))
    公理3: (P → Q) → ((Q → R) → (P → R))
    公理4: (P → (P → Q)) → (P → Q)
    公理5: (P ↔ Q) → (P → Q)
    公理6: (P ↔ Q) → (Q → P)
    公理7: (P → Q) → ((Q → P) → (P ↔ Q))
    公理8: (P ∧ Q) → P
    公理9: (P ∧ Q) → Q
    公理10: P → (Q → (P ∧ Q))
    公理11: P → (P ∨ Q)
    公理12: Q → (P ∨ Q)
    公理13: (P → R) → ((Q → R) → ((P ∨ Q) → R))
    公理14: (P → ¬Q) → (Q → ¬P)
    公理15: ¬¬P → P

公理和定理的导出规则

1
2
3
4
5
6
7
8
9
10
掉头规则 P → (Q → R) ├Q → (P → R) 
挖心规则 P → (Q → R)，Q ├P → R
传递规则 P → Q，Q → R ├P → R
凝缩规则 P → (P → Q) ├P → Q
充要规则 P → Q，Q → P ├P ↔ Q
合取规则 P，Q ↔ ├P ∧ Q
析取规则 P → R，Q → R ├(P ∨ Q) → R
逆否规则 P → ¬Q ├Q → ¬P
拒取规则 P → Q ├¬Q → ¬P
加头规则 P → Q ├(R → P) → (R → Q)

注意代入时，例如 P → ¬Q，Q 用 ¬Q代入，需要写成 P → ¬¬Q；代入时只能替换单独的命题变元，而不是一个命题项

命题演算的假设推理系统

假设推理证明定理的方法
（1）把待证公式的前件一一列出，作为假设（或把待证公式的后件的否定作为假设）
（2）按永真推理方法进行推理，但此时不能对假设实施代入规则
（3）当推导处待证公式的后件时，就说明了该定理