Skip to main content
2 of 2
enumeration, not necessarily increasing
Goldstern
  • 14k
  • 1
  • 47
  • 71

Given a program $P$ I can write a new program $f(P)$ that does the following:

  • Let $k$ be the input for $f(P)$.
  • Using an unbounded loop, find the first $n_0$ such that $P(n_0)=1$.
  • If $k=0$, output $n_0$ and stop.
  • Using a bounded loop, find the largest $i\le \max(n_0, k)$ such that $P(i)=1$.
  • Output $i$ and stop.

So far I have only transformed a program $P$ into a new program $f(P)$ -- even constructivists or intuitionists will agree that my function $f$ is explicitly computable.

Now assume that $P$ computes the characteristic function of a recursive set $A$ (and is in particular total and outputs only 0 and 1). Then I claim that (constructively):

  1. If $A$ is inhabited (i.e., there is some $n\in A$) then $f(P)$ is again total.

  2. Every value $f(P)(k)$ is an element of $A$, i.e., $P(f(P)(k))=1$ for all $k$.

  3. The function $f(P)$ is weakly monotone, i.e., $k\le k'$ implies $f(P)(k)\le f(P)(k')$. (I think that "weakly monotone" is not the same as "nondecreasing", constructively, but I assume that you meant "weakly monotone".)

  4. Every $x\in A$ is a value of $f(P)$. In fact, $f(P)(x)$ first computes some value $n_0 \le x$, and then the largest $i \le x$ with $P(i)=1$, which is $x$ itself.

Note: If there is an enumeration of $A$, then $A$ must be inhabited. I think that being nonempty (i.e., "from $A=\emptyset$ we can get a contradiction") is not enough.

Goldstern
  • 14k
  • 1
  • 47
  • 71