将已解答的练习调整到您的课程。 免费注册
推理规则
| 图例 | |
|---|---|
| α, β, γ | 是合式公式。 |
| ψ | 是一个谓词（P, Q, R...） |
| c, c´, c´´... | 是个体常元（a, b, c...） |
| v, v´, v´´ | 是个体变元（x, y, z...） |
基本规则
| B | ∧ | ∨ | → | ↔ | ¬ | ∀ | ∃ | = | ι |
|---|---|---|---|---|---|---|---|---|---|
| (I) |
α β -- α ∧ β
|
α --- α∨β |
┌α |... ┗β --- α→β |
α→β β→α --- α↔β |
┌ ¬α |......... ┗β∧¬β ----- α
|
α --- ∀vα |
α --- ∃vα |
ψϲ -- ∀v(v=ϲ →ψv) |
ψ(ιvα) --- ∃v∀v´ ( α ↔ x=y) |
| (E) |
α ∧ β -- α β
|
┌α |... ┗ γ ┌β |... ┗ γ --- γ |
α→β α --- β |
α↔β ---- α→β β→α |
¬¬α ---- α |
∀vα --- α
|
∃vα --- α |
∀v(v=ϲ →ψv) -- ψϲ |
∃v∀v´ ( Φ ↔ x=y) --- ψ(ιvΦ) |
派生规则
蕴涵的派生规则
| 规则 | → |
|---|---|
| 条件传递律 (Tr→) | α→β β→γ ---- α→γ |
| 否定后件式 (MT) | α→β ¬β ---- ¬α |
| 二难推理 (Dil) | Dil1 α ∨ β α→γ β→γ ---- γ
Dil2 ¬α ∨ ¬β γ→α γ→β ---- ¬γ |
| 前提载入 (CrPr) | β ---- α→β |
| 换位律 (Ctrp) | α→β ---- ¬β→¬α |
| 条件互换 (Mut →) | α→(β→γ) ---- β→(α→γ) |
| 输入/输出 (Imp/Exp) | α→(β→γ) ---- α∧β→γ |
| 单调性 (Mon) | α→β ---- α ∧ γ→β |
合取/析取的派生规则
| 规则 | ∧ | ∨ |
|---|---|---|
| 选言三段论 (SD) | α ∨ β ¬α ---- β
α ∨ β ¬β ---- α |
|
| 幂等律 (Idp ∧ / Idp ∨) | α ∧ α ----- α |
α ∨ α ---- α |
| 吸收律 (Absc ∧/Absc ∨) | α ∧ (α ∨ β) ---- α |
α ∨ (α ∧ β) ---- α |
| 交换律 (Conm ∧) | α ∧ β ---- β ∧ α |
α ∨ β ---- β ∨ α |
| 结合律 (Asoc ∧/Asoc ∨) | (α ∧ β) ∧ γ ---- α ∧ (β ∧ γ) |
(α ∨ β) ∨ γ ---- α ∨ (β ∨ γ) |
| 分配律 (Dist ∧/Dist ∨) | α ∧ (β ∨ γ) ---- (α ∧ β) ∨ (α ∧ γ) |
α ∨ (β ∧ γ) ---- (α ∨ β) ∧ (α ∨ γ) |
量词的派生规则
| 规则 | ∀ | ∃ | ||
|---|---|---|---|---|
| 全称量词或存在量词否定 (Neg Gen 或 Neg Par) | ¬∀vα ---- ∃v¬α |
¬∃vα ---- ∀v¬α |
||
| 量词降格 (Des Cuant) | ∀vα ---- ∃vα |
---- | ||
| 变元替换 (Mut Var) | ∀vα ---- ∀v´α |
∃vα ---- ∃v´α |
||
| 全称或存在量词收缩 (Contrac Gen Disy 或 Contrac Part Cond) | ∀vα ∨ ∀vβ ---- ∀v(α ∨ β) |
∃vα → ∃vβ ---- ∃v(α → β) |
||
全称量词交换 (Perm Gen) |
∀v∀v´α ----- ∀v´∀vα |
∃v∃v´α ----- ∃v´∃vα |
||
∃v∀v´α ----- ∀v´∃vα |
||||
| 全称或存在量词在合取中的分配 (Dist Gen ∧ / Dist Part ∧) | ∀v(α ∧ β) ---- ---- ∀vα ∧ ∀vβ |
∃v(α ∧ β)
---- ∃vα ∧ ∃vβ |
||
| 存在量词在析取中的分配 (Dist Part ∨) | ---- | ∃v(α ∨ β) ---- ---- ∃vα ∨ ∃vβ |
||
| 全称和存在量词在条件中的分配 (Dist Gen →/Dist Part →) | ∀v(α→β) ----
∀vα→∀vβ |
∃v(α→β) ---- ---- ∀vα→∃vβ |
||
| 全称量词在双条件中的分配 (Dist Gen ↔) | ∀v(α↔β)
----
∀vα↔∀vβ |
|||
全称量词在合取、析取、前件和后件中的条件分配 (Dist Gen ∧/∨/Antec/Consec) |
α ∧ ∀vβ ---- ∀v(α ∧β) |
α ∨ ∀vβ ---- ∀v(α ∨β) |
∀vβ → α --- ∃v(β →α) |
α→∀vβ ---- ∀v(α→β) |
存在量词在合取、析取、前件和后件中的条件分配 (Dist Part ∧/∨/Antec/Consec) |
α ∧ ∃vβ ---- ∃v(α ∧β) |
α ∨ ∃vβ ---- ∃v(α ∨β) |
∃vβ → α --- ∀v(β →α) |
α→∃vβ ---- ∃v(α→β) |
等词的派生规则
| 规则 | = |
|---|---|
| 莱布尼茨1 | c=c' ψc ---- ψc' |
| 莱布尼茨2 | c=c' ψc´ ---- ψc
|
| 莱布尼茨3 | ψc ¬ψc´ ---- c≠c´ |
| 莱布尼茨4 | ¬ψc ψc´ ---- c≠c´ |
| 等词自反律 (Refl =) | ---- c=c' |
| 等词对称律 (Sim =) | c = c´ ---- c´= c |
| 等词传递律 (Tr =) | c=c' c´=c´´ ---- c = c´´ |
| 不可分辨性 (Indescer) | c=c' ---- ψc↔ψc´ |
| 欧几里得 | c=c' ---- fc=fc´ |
定义规则
| 规则 | 连接词 1 | 连接词 2 |
|---|---|---|
| 德摩根 ∧/∨ ∨/∨ | ¬(α ∧ β) ---- ¬α ∨ ¬ β |
¬(α ∨ β) ---- ¬α ∧ ¬ β |
| 定义 ∧/∨ ∨/∧ | α ∧ β ---- ¬(¬α ∨ ¬ β) |
α ∨ β ---- ¬(¬α ∧ ¬ β) |
| 定义 ∧/→ ∨/→ | α ∧ β ---- ¬(α → ¬ β) |
α ∨ β ---- ¬α → β |
| 定义 ∃/∀ ∀/∃ | ∀vα ---- ¬∃v¬α |
∃vα ---- ¬∀v¬α |
返回自然演绎练习
请留下您对本网站练习的意见，以便我改进或扩展。非常感谢大家！
评论、建议和批评