如何在一阶逻辑（FOL）中完成如下谓词逻辑证明？

前提 #

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

待证结论 #

∃x¬(Gx ∧ ¬Hx)

证明过程 #

• 步骤1：对前提2使用合取消去规则（∧E），拆分得到两个子前提：
  • 1.1 ∀xFx
  • 1.2 ∃xGx
• 步骤2：对前提1使用存在实例化规则（∃E），假设存在个体常量a，使得：

  Fa → (Ga → Ha) （临时假设，后续可消去）

• 步骤3：对1.1使用全称实例化规则（∀E），代入个体常量a，得到：

  Fa

• 步骤4：结合步骤2和步骤3，使用蕴含消去规则（→E，假言推理），得到：

  Ga → Ha

• 步骤5：利用逻辑等价式「A→B ≡ ¬(A∧¬B)」，对步骤4的公式进行等价替换，得到：

  ¬(Ga ∧ ¬Ha)

• 步骤6：对步骤5使用存在引入规则（∃I），将个体常量a替换为约束变量x，得到：

  ∃x¬(Gx ∧ ¬Hx)

• 步骤7：由于步骤2的临时假设已完成推导目标，可消去该假设，最终结论得证。

注：前提2中的∃xGx在本证明路径中未被直接使用，因为仅通过∀xFx和前提1即可推导出结论；若需结合∃xGx，可额外通过存在实例化得到Gb，再结合Gb→Hb（同理推导）验证结论的合理性，但不影响最终结果的有效性。

内容的提问来源于stack exchange，提问作者Is_Show