点态可判定性是否意味着完全可判定性？

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的每个值即可。