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.
Constructively deciding whether a decidable predicate holds universally
logic;proof techniques;first order logic