在《伊莎贝尔》中使用“经典”规则

Question

我在 Isabelle 中遇到了一个使用以下规则的自然演绎问题集classical：

\n\n

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

\n\n

我更习惯使用“排中律”（excluded_middle）和“归谬法”（ccontr）。

\n\n

我假设这classical与上述两者相同，但我无法从中证明它们中的任何一个，也无法证明lemma "A \xe2\x88\x92\xe2\x86\x92 \xc2\xac \xc2\xac A"问题集中的哪个。我不认为我只是误解了这个规则，因为我成功地使用它lemma "\xc2\xac \xc2\xac A \xe2\x88\x92\xe2\x86\x92 A"从问题集中证明了。有人可以给我一些使用此规则的提示/策略/演示吗？

\n

Answer 1

这个怎么样：

\n\n

lemma "A \xe2\x88\xa8 \xc2\xac A"\nproof(rule classical)\n  assume "\xc2\xac (A \xe2\x88\xa8 \xc2\xac A)"\n  have "A"\n  proof(rule classical)\n    assume "\xc2\xac A"\n    hence "(A \xe2\x88\xa8 \xc2\xac A)" by (rule disjI2)\n    with \xe2\x80\xb9\xc2\xac (A \xe2\x88\xa8 \xc2\xac A)\xe2\x80\xba\n    show ?thesis by (rule notE)\n  qed\n  hence "(A \xe2\x88\xa8 \xc2\xac A)" by (rule disjI1)\n  with \xe2\x80\xb9\xc2\xac (A \xe2\x88\xa8 \xc2\xac A)\xe2\x80\xba\n  show ?thesis by (rule notE)\nqed\n

\n\n

请注意，A \xe2\x9f\xb6 \xc2\xac \xc2\xac A不需要经典推理：

\n\n

lemma "A \xe2\x9f\xb6 \xc2\xac \xc2\xac A"\nproof(rule impI)\n  assume A\n  show "\xc2\xac \xc2\xac A"\n  proof(rule notI)\n    assume "\xc2\xac A"\n    from this \xe2\x80\xb9A\xe2\x80\xba\n    show False by (rule notE)\n  qed\nqed\n

\n