伊莎贝尔矛盾的惯用证明？答案

【问题标题】：Idiomatic Proof by Contradiction in Isabelle?伊莎贝尔矛盾的惯用证明？
【发布时间】：2013-05-18 22:28:53
【问题描述】：

到目前为止，我在 Isabelle 中以以下风格编写了矛盾证明（使用 Jeremy Siek 的模式）：

lemma "<expression>"
proof -
  {
    assume "¬ <expression>"
    then have False sorry
  }
  then show ?thesis by blast
qed

没有嵌套的原始证明块{ ... }，有没有一种方法可以工作？

【问题讨论】：

【解决方案1】：

经典的反证法有规则ccontr：

have "<expression>"
proof (rule ccontr)
  assume "¬ <expression>"
  then show False sorry
qed

有时使用by contradiction 来证明最后一步可能会有所帮助。

还有规则classical（看起来不太直观）：

have "<expression>"
proof (rule classical)
  assume "¬ <expression>"
  then show "<expression>" sorry
qed

有关使用classical 的更多示例，请参阅$ISABELLE_HOME/src/HOL/Isar_Examples/Drinker.thy

【讨论】：

如果<expression>很大，用assume "~ ?thesis"开头比较方便。
旁白：ccontr（AFAIK 缩写为“经典矛盾”）也是经典推理。因此，将第二种模式称为经典推理听起来有点奇怪。
@chris，你说得对，我应该把这个引用改成“经典推理”。但是，我们应该用什么词来描述“经典”规则？
“经典”规则以完全残酷的方式表达了经典推理，没有任何辅助连接词。在“ccontr”的形式中，它看起来更文明一点，但它是等价的。据我所知，Isabelle/FOL 和 HOL 中这些规则的名称可以追溯到 Larry Paulson。

【解决方案2】：

为了更好地理解规则classical，可以像这样以结构化的 Isar 样式打印：

print_statement classical

输出：

theorem classical:
  obtains "¬ thesis"

因此，对于直觉主义者来说，纯粹的邪恶似乎更直观一些：为了证明一些武断的论点，我们可以假设它的否定成立。

对应的规范证明模式是这样的：

notepad
begin
  have A
  proof (rule classical)
    assume "¬ ?thesis"
    then show ?thesis sorry
  qed
end

这里?thesis是A上述主张的具体论点，可能是一个任意复杂的陈述。这种通过缩写?thesis 进行的准抽象是惯用Isar 的典型代表，以强调推理的结构。

【讨论】：