Constructively deciding whether a decidable predicate holds universally 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.
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.