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

Question

是否认为，如果我可以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).

Answer 1

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

另一方面，forall i, P i它是半可判定的：您可以返回一个证明它是错误的（通过找到一个反例）或不终止的证明，只需i依次检查每个值。