logic - 如何证明排中律在 Coq 中是无可辩驳的？

Question

我试图证明以下来自 an online course 的简单定理排中间是无可辩驳的，但在第 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

如果我 apply H ，那么目标将是 P \/ ~P ，这是排中的，不能 build 性地证明。但除了 apply ，不知道对这个假设能做些什么 P \/ (P -> False) -> False : 寓意 ->是原始的，我不知道如何 destruct或分解它。这是唯一的假设。

我的问题是，如何仅使用原始策略来证明这一点( as characterized here ，即没有神秘的 auto s)？

谢谢。

Answer 1

我不是这方面的专家，但最近在 Coq mailing-list 上讨论了这个问题。 .我将总结这个线程的结论。如果你想更透彻地理解这类问题，你应该看看double-negation translation .

该问题属于直觉命题演算，因此可以由 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 .我没有看到构建 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.