用 Isabelle 证明谓词逻辑

Question

我试图证明以下引理：

lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"

我试图从消除 forall 量词开始，所以这是我尝试过的：

lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"
  apply(rule iffI)
  apply ( erule_tac x="x" in allE)
  apply (rule allE)
  (*goal now: get rid of conj on both sides and the quantifiers on right*)
  apply (erule conjE) (*isn't conjE supposed to be used with elim/erule?*)
  apply (rule allI)
  apply (assumption)
  
  
  apply ( rule conjI) (*at this point, the following starts to make no sense... *)
    
   apply (rule conjE) (*should be erule?*)
   apply ( rule conjI)
   apply ( rule conjI)

  ...

最后我只是根据之前申请的结果开始行动，但我觉得这是错误的，可能是因为一开始有一些错误......有人可以向我解释我的错误以及如何正确完成这个证明？

提前致谢

Answer 1

在这个早期阶段消除全称量词不是一个好主意，因为那时你甚至没有任何可以插入的值（你给出的 x 不在范围内）那一点，这就是为什么它在 Isabelle/jEdit).

中用橙色背景打印的原因

完成 iffI 之后，您有两个目标：

goal (2 subgoals):
 1. ∀x. A x ∧ B x ⟹ (∀x. A x) ∧ (∀x. B x)
 2. (∀x. A x) ∧ (∀x. B x) ⟹ ∀x. A x ∧ B x

现在让我们关注第一个。您应该首先应用右侧的引入规则，即 conjI 和 allI。这让你

goal (3 subgoals):
 1. ⋀x. ∀x. A x ∧ B x ⟹ A x
 2. ⋀x. ∀x. A x ∧ B x ⟹ B x
 3. (∀x. A x) ∧ (∀x. B x) ⟹ ∀x. A x ∧ B x

现在您可以应用 allE 实例化为 x，第一个目标变为 ⋀x. A x ∧ B x ⟹ A x，然后您可以使用 erule conjE 和 assumption 解决。第二个目标的工作方式类似。

最后一个目标，又是类似的：先套用介绍规则，再套用淘汰规则，assumption就大功告成了。

当然，Isabelle 的所有标准证明器，例如 auto、force、blast，甚至是 metis、meson 等简单的证明器, iprover 可以很容易地自动解决这个问题，但这可能不是你想要的。

用 Isabelle 证明谓词逻辑

proving Predicate logic with Isabelle

predicate

proof

isabelle

hol