# 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.

• @David: I think rather that for P(x) = isEven(x), it would show that either it is the case that every number is even, or it is not the case that every number is even. Apr 6, 2014 at 9:17

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.

• From the desription in the linked Wikipedia article, isn't it LPO? LPO is "every 0-1 sequence is all 0s or contains a 1"; LLPO is "every 0-1 sequence that contains at most one 1 has zeroes at all odd-indexed positions or at all even-indexed positions (or both)". Apr 7, 2014 at 21:05
• LPO corresponds to $(\forall n \in \mathbb{N} . P(n)) \lor (\exists n \in \mathbb{N} . \lnot P(n))$, which is stronger than our statement because $\exists n \in \mathbb{N} . \lnot P(n))$ implies $\lnot \forall n \in \mathbb{N} . P(n)$, but not vice versa. I'll explain a bit more as this has been moved to CS. Apr 7, 2014 at 21:36
• Hmm, I think my answer might be incorrect. But it is too late now, I will think about it in the morning. Apr 7, 2014 at 22:15
• I have updated the link so that it points to nLab, where LLPO is explicitly stated in the desired form. If anyone cares to see a proof that the logical form is equivalent to the one with sequences, I suppose I could spell it out. Apr 8, 2014 at 16:16

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).

• Perfect! The trick you suggested probably wont work for my problem, but in my problem $x$ ranges over a finite domain, so I can still use the $x\le y$ argument. I wanted to know if ∀x∈ℕ,P(x)∨¬P(x) was decidable and you have shown me how to conclude that. Apr 6, 2014 at 15:00