时间戳

首页 > 解决方案 > 如何在 Coq 中不使用自动化策略来证明这个 DeMorgan 定律？

coq - 如何在 Coq 中不使用自动化策略来证明这个 DeMorgan 定律？

问题描述

这是我想在这里证明的定律：

Goal forall (X : Type) (p : X -> Prop), (exists x, ~ p x) <-> ~ (forall x, p x).

这是我的代码，直到我不知道该朝哪个方向前进：

Proof. 
  intros. split.
  - intros. destruct H as [x H]. intros nh. apply H. apply (nh x).
  - intros H.

显示的子目标和我所拥有的前提似乎是可证明的，但下一步是什么？

我试过用exfalso., 去apply H.之后。这给了我另一个前提x : X和一个子目标px。

不知道以后怎么办。谢谢您的帮助！

标签： coqcoq-tacticcoqidedemorgans-law

解决方案

从右到左的方向在直觉逻辑中是不可证明的。提出存在主义的证人需要任何将你推向经典逻辑的公理。以排中原理为例：

Axiom excluded_middle : forall (P : Prop), P \/ ~ P.

Goal  forall (X : Type) (p : X -> Prop),
  (exists x, ~ p x) <-> ~ (forall x, p x).
Proof. 
  intros. split.
  - intros. destruct H as [x H]. intros nh. apply H. apply (nh x).
  - intros Hnfapx.
    (* new hyp:  Hnfapx : ~ (forall x, p x) *)
    pose proof (excluded_middle (exists x, ~ p x)) as [? | Hnexnpx]; [assumption|].
    (* new hyp:  Hnexnpx : ~ (exists x, ~ p x)
       from this (and excluded middle again) we can deduce (forall x, p x)
       this contradicts Hnfapx *)
    exfalso. apply Hnfapx. intros x.
    (* new hyp:  x : X
       goal:     p x *)
    pose proof (excluded_middle (p x)) as [? | Hnpx]; [assumption|].
    (* new hyp:   Hnpx : ~ p x
       so there exists x such that ~ p x
       this contradicts Hnexnpx *)
    exfalso. apply Hnexnpx. exists x. assumption.
Qed.

更一般地说，直觉主义逻辑失去了德摩根定律（某些方向）。事实上，德摩根定律通过否定表达了两个逻辑连接词之间的二元性。这在经典逻辑中很好，因为双重否定抵消了。但直觉主义逻辑并非如此：双重否定的消除 (∀ P, ¬¬P → P) 是不可证明的。这个原理实际上相当于排中原理。（然而，(∀ P, ¬¬¬P → ¬P) 是可证明的。）

这就是为什么直觉逻辑需要量词 ∃ 和 ∀：没有一个可以用另一个来定义。

（这首先是作为评论说的；我期待有人提出更彻底的答案，但由于没有人这样做，我现在发布我的。感谢@Arthur Azevedo De Amorim 纠正我哪个公理是足够的。）

推荐阅读