3

Does it hold that if I can decide a proposition P n for each specific n, then I can also decide whether or not forall n, P n ? It feels like it should be doable by some induction over n, but how can I prove that in Coq?

Lemma dec_forall:
  forall (P : nat->Prop),
    (forall n, decidable (P n)) ->
    decidable (forall i, P i).
larsr
  • 5,447
  • 19
  • 38
  • 3
    I am not sure this would be provable, take `P n = some Turing machine reaches the halt state in n steps`. Obviously, `P n` is decidable, by running `P` up to `n` steps, however, I am not sure you are gonna be able to construct a decision procedure for all `n`. – ejgallego Apr 06 '18 at 10:12
  • 2
    If you could, a lot of people would be thrilled if you could run it on `fun n => n > 2 -> even n -> exists p q, prime p /\ prime q /\ n = p + q` and then report the results. – Daniel Schepler Apr 06 '18 at 23:59
  • @DanielSchepler Touché! :-) – larsr Apr 09 '18 at 09:18
  • You can tell whether a duck has one or two heads. Can you say whether all ducks have one or two heads? Have you considered space ducks? – Patrick87 Nov 01 '18 at 12:57

1 Answers1

3

This shouldn't be doable. If forall i, P i is true, the only way to confirm so is to run decidable (P n) infinitely many times. Any terminating decision procedure could only analyze finitely many values of i and therefore could never conclude that forall i, P i is true.

On the other hand, forall i, P i is semi-decidable: you can return a proof that it is false (by finding a counter-example) or not terminate, simply by checking each value of i in turn.

Tej Chajed
  • 3,749
  • 14
  • 18
  • Can this be shown formally, with something like ejgallego’s idea? – larsr Apr 06 '18 at 16:21
  • Btw, @Tej Chajed, I saw your answer to https://cs.stackexchange.com/questions/80590/is-possible-to-prove-undecidability-of-the-halting-problem-in-coq which was a nice proof using diagonalization. – larsr Apr 06 '18 at 16:25
  • 1
    @larsr you cannot formalize this inside Coq in a shallow way due to this axiom being actually compatible with Coq's theory. But indeed my idea should, you just need to turn the Turing machine with number `m` into the predicate `P`, that's kind of a standard transformation. – ejgallego Apr 06 '18 at 18:53
  • > This shouldn't be doable. If forall i, P i is true, the only way to confirm so is to run decidable (P n) infinitely many times. Umm, that's strange, there may be many other realizers for that proposition, unless I'm misunderstanding what you mean by "only". – ejgallego Apr 06 '18 at 18:54
  • @ejgallego: admittedly my comment is not precise or formal, but more an intuition based on the fact that this lemma is supposed to work for _all_ P, and an intuition about how Coq functions work. There's surely a stronger and more formal answer. – Tej Chajed Apr 08 '18 at 21:00
  • 2
    @TejChajed indeed you may want to be careful, recall there is a whole family of "Limited Principles of Ommiciense" that are non-constructive but neither classical, so they kind of stay in the middle and can be realized in some weird ways. – ejgallego Apr 09 '18 at 00:12