11

我试图从一个在线课程中证明以下简单的定理，排除中间是无可辩驳的，但在第 1 步几乎被卡住了：

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
Proof.
  intros P. unfold not. intros H.

现在我得到：

1 subgoals
P : Prop
H : P \/ (P -> False) -> False
______________________________________(1/1)
False

如果 I apply H，那么目标将是P \/ ~P，它被排除在中间并且不能被建设性地证明。但除此之外apply，我不知道可以对假设做些什么P \/ (P -> False) -> False：暗示->是原始的，我不知道如何destruct分解或分解它。这是唯一的假设。

我的问题是，如何仅使用原始策略（如这里所描述的，即没有神秘auto的 s）来证明这一点？

谢谢。

4

1 回答 1

18

我不是这方面的专家，但最近在Coq 邮件列表中讨论了它。我将从这个线程中总结出结论。如果你想更彻底地理解这类问题，你应该看看双重否定翻译。

该问题属于直觉命题演算，因此可以由 决定tauto。

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  tauto.
Qed.

该线程还提供了更详细的证明。我将尝试解释我将如何提出这个证明。请注意，我通常更容易处理引理的编程语言解释，所以这就是我要做的：

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  unfold not.
  intros P f.

我们被要求编写一个函数，该函数接受该函数f并产生一个类型的值False。到达这一点的唯一方法False是调用函数f。

 apply f.

因此，我们被要求为函数提供参数f。我们有两个选择，通过P或P -> False。我看不到构建 a 的方法，P所以我选择了第二个选项。

  right.
  intro p.

我们又回到了第一方，只是我们现在有一个p可以合作的！所以我们申请f，因为这是我们唯一能做的。

  apply f.

再一次，我们被要求提供论据f。不过现在这很容易，因为我们有一个p可以使用的。

  left.
  apply p.
Qed.

该线程还提到了一个基于一些更简单的引理的证明。第一个引理是~(P /\ ~P)。

Lemma lma (P:Prop) : ~(P /\ ~P).
  unfold not.
  intros H.
  destruct H as [p].
  apply H.
  apply p.
Qed.

第二个引理是~(P \/ Q) -> ~P /\ ~Q：

Lemma lma' (P Q:Prop) : ~(P \/ Q) -> ~P /\ ~Q.
  unfold not.
  intros H.
  constructor.
  - intro p.
    apply H.
    left.
    apply p.
  - intro q.
    apply H.
    right.
    apply q.
Qed.

这些引理足以说明：

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  intros P H.
  apply lma' in H.
  apply lma in H.
  apply H.
Qed.
于 2015-09-27T21:37:29.570 回答