coq - 逐点可判定性是否意味着总可判定性？

是否认为如果我可以为每个特定的 P n 决定一个命题 n ，那么我也可以决定是否 forall n, P n ？感觉它应该可以通过对 n 的一些归纳来实现，但是我如何在 Coq 中证明这一点？

Lemma dec_forall:
  forall (P : nat->Prop),
    (forall n, decidable (P n)) ->
    decidable (forall i, P i).

最佳答案

这不应该是可行的。如果 forall i, P i 为真，则确认这一点的唯一方法是无限次运行 decidable (P n)。任何终止决策过程只能分析 i 的有限多个值，因此永远无法得出 forall i, P i 为真的结论。

另一方面，forall i, P i 是半可判定的:只需依次检查 i 的每个值，就可以返回证明它为假(通过找到反例)或不终止的证明。

关于coq - 逐点可判定性是否意味着总可判定性？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/49689530/