如何证明排中在 Coq 中是无可辩驳的?
Posted
技术标签:
【中文标题】如何证明排中在 Coq 中是无可辩驳的?【英文标题】:How to prove excluded middle is irrefutable in Coq? 【发布时间】:2015-12-25 02:17:41 【问题描述】:我试图从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
,它被排除在中间并且不能被建设性地证明。但是除了apply
之外,我不知道假设P \/ (P -> False) -> False
可以做什么:暗示->
是原始的,我不知道如何destruct
或分解它。这是唯一的假设。
我的问题是,如何仅使用原始策略(as characterized here,即没有神秘的auto
s)来证明这一点?
谢谢。
【问题讨论】:
也许看看证明项(用tauto
和一些简化创建)是有道理的:Check fun (P : Prop) (H : ~ (P \/ ~ P)) => False_ind False (H (or_intror (fun H0 => H (or_introl H0)))).
【参考方案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.
【讨论】:
+1感谢您的指点。这如宣传的那样工作。但正如邮件列表所说,它仍然很神秘。 (邮件列表中的解释是用非英文字符写的,数学部分真的很难读)。你有没有机会用英语添加对大局的解释?以上是关于如何证明排中在 Coq 中是无可辩驳的?的主要内容,如果未能解决你的问题,请参考以下文章