集合成员的否定，平等

Question

我注意到 Isabelle 自动将 ¬ (a ∈ (- A)) 和 ¬ (x = y) 分别简化为 a ∉ A 和 x ≠ y。

这是自然演绎中的简单纸笔证明，但在 Isabelle 中失败了。在第 2 行中，¬ (a ∈ (- A)) 被简化为 a ∉ - A。从后者，我们不能应用 ComplD，但是为什么呢？

lemma "- (- A) ⊆ (A::'a set)"   
proof 
   fix a assume "a ∈ - (- A)"
   hence "¬ (a ∈ (- A))" by (rule ComplD)
   hence "¬ (¬ (a ∈ A))" by (rule ComplD) (* fail! *)
   thus "a ∈ A" by (rule notnotD)
qed

有没有办法回到非简化表达式？

当然，引理可以通过 simp 在一行中证明。但我的目的是明确使用自然演绎规则（用于教学）。

Answer 1

这些不是简化。如果您查看 Isabelle 中 a ≠ b 和 x ∉ A 的定义（例如，通过 ctrl 单击符号），您会发现它们只是 ¬(a = b) 和 ¬(x ∈ A) 的缩写。这些语句的内部表示方式与您在上面编写的方式完全相同，只是为了提高可读性而以不同的方式打印。

您不能应用规则ComplD 的原因是它根本不匹配。 ComplD 说?c ∈ - ?A ⟹ ?c ∉ ?A。但是，在失败的步骤中，您的假设是a ∉ -A，并且不能统一到ComplD 的前提?c ∈ -?A，因此rule 失败。

我相对肯定你需要经典推理来证明这个证明，因为你的陈述在直觉上不成立。这意味着您必须通过矛盾进行证明，例如像这样：

lemma "- (- A) ⊆ (A::'a set)"   
proof
  fix a assume a: "a ∈ - (- A)"
  show "a ∈ A"
  proof (rule ccontr)
    assume "a ∉ A"
    have "a ∈ -A"
    proof (rule ComplI)
      assume "a ∈ A"
      with ‹a ∉ A› show False by contradiction
    qed
    moreover from a have "a ∉ -A" by (rule ComplD)
    ultimately show False by contradiction
  qed
qed

里面的rule ccontr开始反证；证明方法contradiction 只是一个很好的方法，当一个人已经证明了一个事实和它的否定时。