Constructively deciding whether a decidable predicate holds universally

Question

I am trying to obtain the proof of the proposition:

$(\forall x \in \mathbb{N}, P(x)) \vee (\neg \forall x, P(x))$

given that the property $P$ is decidable for every $x \in \mathbb{N}$, i.e.

$\forall x \in \mathbb{N}, P(x) \vee \neg P(x)$

This is easy to prove (even without using the decidability of $P$) if I include the law of excluded middle, i.e.,

$\forall P, P \vee \neg P$.

However, I am trying to obtain a constructive proof for the same. Is the proposition true without including the law of excluded middle? If so, how do I prove it? This seemingly simple property is needed to prove something about a complex system, and I am trying to not use the law of excluded middle unless it's absolutely necessary.

The best I could come up with is the following:

$\forall y, (\forall x \le y, P(x)) \vee \neg (\forall x \le y, P(x))$

I do not know how to proceed beyond this (or if this is even useful).

Any help would be appreciated.

Answer 1

You are asking for a constructive proof of the Lesser limited principle of omniscience (LLPO), which states (in one of its forms) that for a decidable proposition $P$ on natural numbers $$(\forall n \in \mathbb{N} \,.\, P(n)) \lor \lnot \forall n \in \mathbb{N} \,.\, P(n).$$ That's exactly your problem. It is well known that LLPO is not provable constructively.

Unless you have some further conditions on $P$ which you did not tell us about, you're stuck.

Answer 2

From a proof of $Q \lor \neg Q$ you can extract a witness saying whether $Q$ or $\neg Q$. From a proof of $\forall M~ (Q \lor \neg Q)$, you can extract an algorithm mapping $M$ to whether $Q$ or $\neg Q$.

$P(M,x)$ could be "Turing machine $M$ does not stop within $x$ steps on the empty input", which is indeed decidable; but then $\forall x~P(M,x)$ means "Turing machine $M$ never stops on the empty input. Since you made no hypothesis on $M$, $(\forall x~P(M,x)) \lor \neg \forall x~P(M,x))$ means that you can decide the termination of $M$.

Note: there is the converse — if $P$ is a decidable property such as $A(x)=\mathit{true}$, then you can prove $\neg \neg P \Rightarrow P$. I reckon that, for instance, Georges Gonthier sometimes proves complicated properties with double negations added everywhere (so with classical-like reasoning), then concludes by this trick. This gives you the ease of proving in classical logic but still an intuitionistic result (without assuming excluded middle).