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.

  • 3
    $\begingroup$ @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. $\endgroup$ Apr 6, 2014 at 9:17

2 Answers 2


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.

  • $\begingroup$ 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)". $\endgroup$ Apr 7, 2014 at 21:05
  • 1
    $\begingroup$ 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. $\endgroup$ Apr 7, 2014 at 21:36
  • $\begingroup$ Hmm, I think my answer might be incorrect. But it is too late now, I will think about it in the morning. $\endgroup$ Apr 7, 2014 at 22:15
  • $\begingroup$ 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. $\endgroup$ 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).

  • $\begingroup$ 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. $\endgroup$
    – Adam Barak
    Apr 6, 2014 at 15:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.