寻找一个可判定谓词的反例

Question

感觉下面的Coq语句应该是建设性的:

Require Import Decidable.
Lemma dec_search_nat_counterexample (P : nat -> Prop) (decH : forall i, decidable (P i))
: (~ (forall i, P i)) -> exists i, ~ P i.

如果存在上界，我希望能够证明如下形式的东西:假设并非每个i < N都满足P i。然后是i < N，其中~ P i"实际上，您可以编写一个函数，通过从0开始搜索来查找最小示例。

当然，最初的说法没有上界，但我觉得应该有一个归纳论证，从上面的有界版本得到上界。但我不够聪明，不知道怎么做!我是不是错过了一个聪明的把戏?还是说，尽管自然数是有序的，但有什么根本原因使它不能成立?

Answer 1

Meven Lennon-Bertrand评论后的返工答案

这个语句等价于交换P和~P的马尔可夫原理。由于P是可决定的，我们有P <-> (~ ~ P)，因此可以进行此替换。

这篇论文(http://pauillac.inria.fr/~herbelin/articles/lics-Her10-markov.pdf)认为马尔科夫原理在Coq中是不可证明的，因为作者(Coq的作者之一)在这篇论文中提出了一个新的逻辑，允许证明马尔科夫原理。

老答:

这在道德上是"全知有限原则"。- LPO(见https://en.wikipedia.org/wiki/Limited_principle_of_omniscience)。它需要经典公理在Coq中证明，或者你可以断言它是一个公理。

看到例如:

Require Import Coquelicot.Markov.
Check LPO.
Print Assumptions LPO.

如果没有它的标准库版本