我有以下定理要证明:
Goal (exists x, ~P x) <-> ~(forall x, P x).
分手后
unfold not. split.
第一个含义很简单,基本上我们必须在存在量词中使用从forall引入的x
intros. destruct H. apply H. apply (H0 x).
但另一方面我不能这样继续下去,我认为应该有一个我找不到的想法。有什么建议吗?
我有以下定理要证明:
Goal (exists x, ~P x) <-> ~(forall x, P x).
分手后
unfold not. split.
第一个含义很简单,基本上我们必须在存在量词中使用从forall引入的x
intros. destruct H. apply H. apply (H0 x).
但另一方面我不能这样继续下去,我认为应该有一个我找不到的想法。有什么建议吗?
好吧,这确实是有充分理由的:我相信它在直觉逻辑中是无法证明的。
如您所见,问题在于,要通过反向推理取得进展,您需要立即提供证人,而要通过正向推理取得进展,您需要掌握一个荒谬的假设。所以这个目标被卡住了。
问题是全称量词的否定并没有给你否定属性的存在证人。
引入经典公理后,有很多方法可以证明这一点。这是一个带有排中律的笨拙的例子:
Parameter T : Type.
Parameter P : T -> Prop.
Axiom EM : forall (A : Prop), A \/ ~ A.
Goal (exists x, ~P x) <-> ~(forall x, P x).
Proof.
split; intro H.
destruct H as [x H]. intro A. apply H. easy.
destruct (EM (exists x, ~ P x)) as [?|NE].
easy.
elim H. intro x. destruct (EM (P x)) as [Px|NPx].
easy.
elim NE. exists x. easy.
Qed.