伊莎贝尔的反证法证明

Question

我理解

ccontr

是如何工作的，但是我不确定如何（或者即使可能）在用假设声明的引理上使用它。

举这个简单的例子，一切都很好：

lemma l1: "A⊆B ⟶ A ∩ B = A"
proof(rule ccontr)
  assume "¬(A⊆B ⟶ A ∩ B = A)"
  then show False
    by auto
qed

从技术上讲，引理相当于（**注）：

lemma l2: 
  assumes P: "A⊆B"
    shows Q: "A ∩ B = A"
proof(rule ccontr)
  assume "¬(P ⟶ Q)"
  then show False ...
qed

在“然后显示...”行上出现错误

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (¬ (P ⟶ Q)) ⟹ False

似乎我无法在

ccontr

版本（l2）中使用

assumes... shows...

。我尝试使用

assume Q ∧ ¬P

，但出现同样的错误。 有没有办法继续进行某种形式的证明“假设（Q和~P）显示 False 因此引理是正确的”？

（**注）：附带问题：我假设引理 l1 和 l2 在逻辑上是等价的吗？有什么东西让他们彼此显着不同（在伊莎贝尔身上）？

提前谢谢您！

Answer 1

你应该否定你的主张（在

shows

中），然后证明给定的假设会导致

False

：

lemma l2: 
assumes P: "A⊆B"
shows "A ∩ B = A"
proof (rule ccontr)
  assume "¬(A ∩ B = A)"
  with P show False by auto
qed

我在 Isabelle/ZF 检查过这一点，但在 Isabelle/HOL 中应该是相同的。

至于附带问题，严格来说，这两种形式在逻辑上并不相同，第一种形式使用对象逻辑蕴涵

⟶

，而第二种形式使用元逻辑中的==>。然而，这两种形式都表达了相同的想法，我个人更喜欢第二种，因为它更具可读性并且在 Isabelle 中与自动化配合得更好。