你如何在FOL中证明∃x[Fx →(Gx → Hx)]，∀xFx ∧ ∃xGx ∴ ∃x¬(Gx ∧ ¬Hx)？

Question

给定：

∃x[Fx → (Gx → Hx)]
∀xFx ∧ ∃xGx

证明：

∃x¬(Gx ∧ ¬Hx)

Answer 1

启动：

∃x[Fx → (Gx → Hx)]
∀xFx ∧ ∃xGx

我们知道F对所有x都是真的(因为∀xFx)，所以我们可以在第一个语句中将Fx替换为真。

∃x[true → (Gx → Hx)]

我们知道A→B是-VB的缩写，所以我们可以在这里这样做：

∃x[¬(true) V (Gx → Hx)]
∃x[false V (Gx → Hx)]

我们知道false or X等于X:

∃x[false V (Gx → Hx)]
∃x[(Gx → Hx)]

我们可以应用隐含的定义(→)再次：

∃x[(Gx → Hx)]
∃x[¬Gx V Hx]

最后，我们可以使用德摩根定律((A V B) <=> ¬(¬A ∧ ¬B))来反转括号的内容，并简化nots:

∃x[¬Gx V Hx]
∃x[¬(¬(¬Gx) ∧ ¬(Hx))]
∃x[¬(¬¬Gx ∧ ¬Hx)]
∃x[¬(Gx ∧ ¬Hx)]
∃x¬[Gx ∧ ¬Hx]

这就是你想要证明的。