给定一个具有对象逻辑含义的定理"P(t)⟶(∃x.P(x))",为什么证明目标"P(t)⟹(∃x.P(x))"与meta-给出逻辑含义？

Question

我刚开始使用Isabelle/HOL并试图用自然演绎规则证明一个简单的HOL语句"P(t)⟶(∃x.P(x))".我从一个仅包含该定理的理论文件开始:

theory simple imports Main
begin

lemma T: shows "P(t) ? (?x . P(x))"
proof
  (* x *)
qed  

end

在注释中标记为x的位置处,当前目标已经是"P(t)⟹(∃x.P(x))",即逻辑蕴涵已经简化为元逻辑蕴涵.

通过反复试验,我得出以下证据:

proof
  assume "P(t)" then
  have "? x . P(x)" by (rule exI) then
  have "P(t) ? (?x . P(x))" by (rule impI)
  then show "P(t) ? (?x . P(x))" by (rule impE)
qed

这看起来有些奇怪:我正在介绍这个含义,只是为了在下一步中消除它.

我现在的问题是:

1. 重写我的目标来自哪里,哪里可以找到更多关于它的信息？
2. 如何简化证明(不使用auto绕过ND)？

Answer 1

\n

我的目标重写从何而来？我在哪里可以找到更多相关信息？

\n

\n\n

proof当您这样使用时，它就向您的目标迈出了一个简单的步骤。对于你的情况，它适用rule impI。如果您不想这样，请使用proof -.

\n\n

但您可能确实想使用隐式rule impI。请注意，它会改变您的目标，您可以这样写：

\n\n

proof\n  assume "P(t)"\n  then show "\xe2\x88\x83 x . P(x)" by (rule exI)\nqed\n

\n\n

这回答了你的第二个问题。

\n