在 Isabelle 中使用规则 'classical'

Question

我在 Isabelle 中遇到了一个 problem set 的自然推论，它使用规则 classical:

( \<not> A ==> A) ==>A

我比较习惯使用'law of excluded middle'（excluded_middle）和'reductio ad absurdum'（ccontr）。

我假设 classical 等同于以上两个，但我无法从中证明它们中的任何一个，也无法证明问题集中的 lemma "A −→ ¬ ¬ A"。我不认为我只是误解了规则，因为我成功地使用它从问题集中证明了 lemma "¬ ¬ A −→ A"。有人可以给我一些 tips/strategies/demonstrations 来使用这个规则吗？

Answer 1

这个怎么样：

lemma "A ∨ ¬ A"
proof(rule classical)
  assume "¬ (A ∨ ¬ A)"
  have "A"
  proof(rule classical)
    assume "¬ A"
    hence "(A ∨ ¬ A)" by (rule disjI2)
    with ‹¬ (A ∨ ¬ A)›
    show ?thesis by (rule notE)
  qed
  hence "(A ∨ ¬ A)" by (rule disjI1)
  with ‹¬ (A ∨ ¬ A)›
  show ?thesis by (rule notE)
qed

注意A ⟶ ¬ ¬ A不需要经典推理：

lemma "A ⟶ ¬ ¬ A"
proof(rule impI)
  assume A
  show "¬ ¬ A"
  proof(rule notI)
    assume "¬ A"
    from this ‹A›
    show False by (rule notE)
  qed
qed

Answer 2

Joachim Breitner 的回答给了我所有我需要的信息，但我想把它变成一种我更好理解的格式，并且也适合我最初引用的问题集（据说只使用 apply 方法）。

以下是 Breitner 以这种格式编写的校样：

lemma 1: "A ∨ ¬ A"
apply (rule classical)
apply (rule disjI1)
apply (rule classical)
apply (erule notE)
apply (rule disjI2)
apply assumption
done

'Lemma 1' 我想我已经稍微缩短了，因为我没有使用第二个 notE（这是不必要的，因为 A ∨ ¬ A 已经显示了）。

lemma 2: "A ⟶ ¬ ¬ A"
apply (rule impI)
apply (rule notI)
apply (rule notE)
apply assumption
apply assumption
done

正如 Breitner 指出的那样，'Lemma 2' 不使用 classical，实际上在直觉逻辑中是有效的。

至于我使用规则 classical 学到的东西，可以将其形象化为一种 'proof by contradiction'：我们可以假设否定，并且必须证明我们的原始陈述。

在 Isabelle 中使用规则 'classical'

Using the rule 'classical' in Isabelle

logic

isabelle