逐点可判定性是否蕴含全局可判定性？Coq证明问询

1. 逐点可判定性是否蕴含全局可判定性？ #

简单来说：不蕴含。

先明确两个核心概念：

• 逐点可判定性：对每个自然数n，命题P n是可判定的（即要么能证明P n为真，要么能证明P n为假）。
• 全局可判定性：全称命题∀n, P n本身是可判定的（即要么能证明所有n都满足P n，要么能证明存在某个n不满足P n）。

你直觉里的“归纳覆盖所有情况”思路，问题出在自然数是无限集合——你没法完成无限次的检查。举个现实的例子：假设P n表示“n不是哥德巴赫猜想的反例”，对于任意给定的n，我们可以通过有限步骤验证它是否能拆成两个质数之和，所以每个P n都是可判定的。但∀n, P n就是哥德巴赫猜想本身，目前我们既没法证明它为真，也没法找到反例证明它为假，所以这个全称命题是不可判定的。

从构造性数学的角度看，逐点可判定只保证了每个单独的P n有判定算法，但全称命题的可判定需要一个有限算法：要么给出所有P n成立的证明，要么找到一个具体的反例——而无限集合的特性意味着这样的算法不一定存在。

2. 在Coq中证明dec_forall引理 #

首先要明确：这个引理在Coq的标准直觉主义逻辑中是无法证明的。

Coq的核心逻辑是构造性的，它不接受无限制的排中律（即A ∨ ¬A对所有命题A成立）。而decidable (∀i, P i)本质上就是(∀i, P i) ∨ ¬(∀i, P i)，要证明它，你要么构造出所有P i成立的全局证明，要么构造出一个反例k使得¬P k成立。但逐点可判定性只给了你对每个n单独判定P n的能力，并没有给你遍历无限自然数找反例的方法，也没法保证你能构造出全局证明。

不过，如果你愿意引入经典逻辑的公理（比如排中律），这个证明就变得非常简单：

首先定义decidable的标准形式：

Definition decidable (A : Prop) : Prop := A ∨ ¬A.

然后引入经典逻辑库，直接用排中律完成证明：

Require Import Classical.

Lemma dec_forall: forall (P : nat->Prop), (forall n, decidable (P n)) -> decidable (forall i, P i).
Proof.
  intros P H.
  (* 直接应用排中律，因为decidable的定义就是命题本身的排中律形式 *)
  apply Classical.em.
Qed.

但这其实是“作弊”——排中律直接断言了所有命题都是可判定的，不管逐点可判定的前提。而你直觉里的“归纳法”思路之所以行不通，是因为归纳法只能处理有限的自然数范围（比如证明所有n ≤ k满足P n），但无法覆盖无限的整个自然数集合。

在构造性逻辑的框架下，这个引理是不可证的，因为存在语义模型（比如基于递归函数的实现性模型），其中存在逐点可判定但全局不可判定的谓词P。

内容的提问来源于stack exchange，提问作者larsr