Least Fixed Point of Enumeration Operator is Recursively Enumerable

Theorem

Let $\psi : \powerset \N \to \powerset \N$ be an enumeration operator.

Then there exists a recursively enumerable set $A$ such that:

$A$ is a fixed point of $\psi$

Every fixed point of $\psi$ is a superset of $A$

Proof

By Least Fixed Point of Enumeration Operator, such an $A$ can be defined as:

$\ds \bigcup_{i \mathop \in \N} A_i$

where:

$A_0 = \O$

$A_{n + 1} = \map \psi {A_n}$

By definition of enumeration operator, there exists a recursively enumerable set $\phi \subseteq \N$ such that:

$\map \psi A = \set {x \in \N : \exists \text { finite } B \subseteq A : \map \pi {x, b} \in \phi}$

where:

$b \in \N$ is the code number for $B$

$\pi : \N^2 \to \N$ is the Cantor pairing function

Suppose that there is no $x_0 \in \N$ such that:

$\map \pi {x_0, 0} \in \phi$

Then, for every $x \in \N$:

$\map \pi {x, 0} \notin \phi$

By induction, we will show that every $A_i = \O$.

$A_0 = \O$ by definition.

If $A_i = \O$, then by Subset of Empty Set iff Empty, for every $B \subseteq A_i$:

$B = \O$

Therefore:

$b = 0$

But then:

$\map \pi {x, b} \notin \phi$

for every $x \in \N$.

Thus, by definition of $A_{i + 1}$:

$A_{i + 1} = \O$

By Principle of Mathematical Induction:

$A_i = \O$

for every $i \in \N$.

Thus:

$\ds A = \bigcup_{i \mathop \in \N} A_i = \empty$

As $\phi$ is recursively enumerable and $A = \phi$:

$A$ is recursively enumerable

$\Box$

Now, suppose there is some $x_0 \in \N$ such that:

$\map \pi {x_0, 0} \in \phi$

Then:

$x_0 \in A_1 \subseteq A$

as $0$ codes the empty set.

Thus, $A$ is non-empty.

By Corollary to Recursively Enumerable Set is Image of Primitive Recursive Function:

There exists a primitive recursive function $f : \N \to \N$ such that:

$\Img f = \phi$

Define:

$\map g {t, b} = \begin{cases}

\map {\pi_1} {\map f t} & : \map {\RR_\subseteq} {\map {\pi_2} {\map f t}, b} \\ x_0 & : \text {otherwise} \end{cases}$ where:

$\pi_1$ and $\pi_2$ are the projections of the Cantor pairing function

$\map {\RR_\subseteq} {x, y}$ if and only if $x$ and $y$ respectively code finite sets $X$ and $Y$ such that $X \subseteq Y$

Work In Progress In particular: Need proof that $\RR_\subseteq$ is primitive recursive; in progress You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{WIP}} from the code.