Problem #2 Template

In problem 1 we saw that arbitrarily large n-valleys could be found in a decreasing function f : nat -> nat. However, it was also mentioned that we wouldn’t be able to prove the infinite analog (i.e., f is eventually constant) without using classical reasoning. The purpose of this problem will be to (in some sense) demonstrate this.

Limited Principle of Omniscience

The limited principle of omniscience (LPO) says every binary sequence is either 0 everywhere or 1 somewhere. The LPO is obviously true classically, but is not constructive. Informally, we see that when trying to decide whether or not a sequence is 1 somewhere, we run into something like the halting problem: at what point do we give up our search for a 1? We may have just run past 10 billions 0’s, but there’s no way we can know that a 1 isn’t right around the corner.

Infinite Valleys

By an infinite valley, we will mean a point at which a function f : nat -> nat is eventually constant. If we naively search for infinite valley in a given f, we see that we run into a similar problem to the one above: how do we know when to stop looking? Of course, if f is decreasing and hits 0, we can stop, but it seems like that is the best we can do.

As it turns out, there is more than just a superficial similarity between these two sorts of problems:

Problem: Show that the LPO is logically equivalent to the statement that every decreasing f : nat -> nat achieves an infinite valley.