集合成员资格的否定，平等

Question

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

这是自然演绎中的简单纸笔证明，但在伊莎贝尔中失败了。在第 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) 和 [=14= 的缩写].这些语句在内部完全按照您上面编写的方式表示，只是为了提高可读性而以不同方式打印。

您不能应用规则 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 只是在证明一个事实及其否定时推导出任何东西的一种好方法。

集合成员资格的否定，平等

Negation of set membership, equality

isabelle