否定集合成員資格，等於

Question

我注意到，Isabelle自動簡化了¬ (a ∈ (- A))和¬ (x = y)到a ∉ A和x ≠ y。

下面是一個簡單的筆和紙證明自然推演，但在伊莎貝爾失敗。在第二行中，¬ (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只是一個證明事實和否定的推理方法。