2
$\begingroup$

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.

$\endgroup$

migrated from cstheory.stackexchange.com Apr 7 '14 at 11:49

This question came from our site for theoretical computer scientists and researchers in related fields.

  • 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$ – Niel de Beaudrap Apr 6 '14 at 9:17
12
$\begingroup$

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.

$\endgroup$
  • $\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$ – David Richerby Apr 7 '14 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$ – Andrej Bauer Apr 7 '14 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$ – Andrej Bauer Apr 7 '14 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$ – Andrej Bauer Apr 8 '14 at 16:16
5
$\begingroup$

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

$\endgroup$
  • $\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 '14 at 15:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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