# Seemingly ill-founded recursion and the recursion theorem

The following line well-defines a family of subsets $\{S_i\}_{i\in\mathbb N}$ of $\mathbb N$:

$n\in S_i$ iff $n=2i$ or $\exists j<i$ such that $n\in S_j$.

The following line does not:

$n\in S_i$ iff $n=2i$ or $\exists j$ such that $n\in S_j$.

Now what about the following line? I suspect that it does well-define a family of subsets, but I'm not sure how one would prove it; some clever application of the Recursion Theorem or Godel's fixed point theorem perhaps?

$n\in S_i$ iff $n=2i$ or $\mbox{Prov}_{PA}(\exists j\mbox{ such that }n\in S_j)$

And similarly

$n\in S_i$ iff $n=2i$ or $\exists j$ such that $\mbox{Prov}_{PA}(n\in S_j)$

In both cases $\mbox{Prov}_{PA}$ is a predicate symbol for provability from $PA$, and $\mbox{Prov}_{PA}(\phi)$ is shorthand for $\mbox{Prov}_{PA}(\ulcorner\phi\urcorner)$ where $\ulcorner\phi\urcorner$ is a Godel number of $\phi$. I suspect the latter two lines, suitably formalized (how?), do well-define sets $S_i$: because the ill-founded part (references to arbitrary $S_j$) are inside of $\mathrm{Prov}_{PA}$, they are not actually statements about $S_j$ at all, but only about what $PA$ proves about $S_j$ (which suggests using the Recursion Theorem).

In the literature, would it be acceptable to write either of the latter two lines while brushing aside the details?

-
Your second displayed line does seem to define a unique family of sets, namely, $S_i=\mathbb{N}$ for all $i$, which is the only family satisfying the property. Why do you say that it does not? –  Joel David Hamkins Dec 30 '13 at 16:52
I said so because membership in S_i depends on membership in S_i (circularly). But you're right, technically, so I'll change it to $n\in S_i$ iff $n=2i$ or $\exists j$ such that $n\in S_j$. Then to check whether $1\in S_0$, we are instructed (among other things) to check whether $1\in S_0$, which in turn means checking whether $1\in S_0$, etc. –  Anonymous Dec 30 '13 at 16:55
Could you clarify what you mean precisely by including $S_j$ inside the provability predicate? You seem to be asking whether a given equivalence determines a unique set, which is essentially a second order matter, but in this case, it makes no sense to refer to that set inside the provability predicate, which I take you to refer to first-order provability in PA. Your question seems to want clarification. –  Joel David Hamkins Dec 30 '13 at 17:00
Yes, the clarification IS the question. We don't bat an eye when we say, "There is a $\lambda$ such that $PA$ proves $\lambda\leftrightarrow \neg\mathrm{Prov}_{PA}(\lambda)$, even though your complaint applies there just as well. My question is, can the latter two definitions in my OP be justified in a similar way to this liar's paradox... As far as first-order-second-order issues, within the predicate, $S_j$ should not be considered as set, but as formula. –  Anonymous Dec 30 '13 at 17:04
Don't careful people write $\lambda \leftrightarrow \lnot \mathrm{Prov}_{PA}(\ulcorner \lambda \urcorner)$? –  Andrej Bauer Dec 30 '13 at 18:12

Let us think about the alleged definition of a family of sets $\lbrace S_i \rbrace_{i \in \mathbb{N}}$ as a fixpoint equation in the complete lattice $P(\mathbb{N} \times \mathbb{N})$, with the inclusion order. Under this view the family $\lbrace S_i \rbrace_{i \in \mathbb{N}}$ corresponds to the set $\lbrace (i, n) \in \mathbb{N} \times \mathbb{N} \mid n \in S_i \rbrace$. This way we can discuss not only whether the family is well defined (the endomap in question has a unique fixed point), but whether it is underdetermined (there are many solutions) or overdetermined (no solutions).

The first example is about fixed points of $\Phi : P(\mathbb{N} \times \mathbb{N}) \to P(\mathbb{N} \times \mathbb{N})$ where $$\Phi(S) = \lbrace (i,n) \mid (n = 2 i) \lor \exists j < i . (j, n) \in S\rbrace.$$ This is obviously a monotone map, therefore by Tarski's theorem it has both the least fixed point and the greatest fixed point. If I am doing this right, the least and greatest fixed points coincide, so this is indeed a good definition.

The next example asks about fixed points of $\Psi : P(\mathbb{N} \times \mathbb{N}) \to P(\mathbb{N} \times \mathbb{N})$ where $$\Psi(S) = \lbrace (i,n) \mid (n = 2 i) \lor \exists j . (j, n) \in S\rbrace.$$ Once again, this is a monotone map and so it has fixed points. But this time the least fixed point and the greatest fixed point differ, if I am not mistaken. So the definition is "underdetermined".

The examples involving provability need to be considered in a different setting, but they are still about existence of fixed points. As far as I can tell they just reduce to the arithmetic fixed-point theorem, as discussed in this question. The point is that we need to differentiate between a formula $S$ and its Gödel code $\ulcorner S \urcorner$. In your example, you are asking for a formula $S$ whose only free variables are $i$ and $n$ such that $$S \iff (n = 2 i \lor \mathrm{Prov}_PA(\ulcorner \exists j . S[j/i] \urcorner).$$ I think such a formula exists, but it may not be unique.

In any case, the point of my answer is that (a) it is less confusing to think about fixed points of endomaps than mysterious self-referential constructions and (b) that you need to put in some Gödel codes when you speak about provability.

-

This is essentially a too-long comment on Will Sawin's answer. That answer assumes that the definition of $S_i$, namely the equivalence $$n\in S_i \iff (n=2i \lor \exists j\,\text{Prov}_{PA} (n\in S_j)),$$ is to be provable in PA. But if we merely assume that this equivalence is true, then there are more possibilities for what $S_i$ could be. Specifically, in addition to Will's answer, that each $S_i=\mathbb N$, there is the possibility that each $S_i$ is the set of even natural numbers. With this choice of $S_i$, the crucial clause in the definition, $\exists j\,\text{Prov}_{PA} (n\in S_j)$, has the following two properties. First, PA proves that this clause is equivalent to "$n\text{ is even}\lor PA\text{ is inconsistent}$." Second, since $PA$ is in fact consistent, this clause is equivalent to simply "$n\text{ is even}$" (but $PA$ can't prove that because $PA$ can't prove its own consistency). So, if we take all the $S_i$ to be the set of even numbers, then the definition of $S_i$ is satisfied, but $PA$ can't prove that it is satisfied. [Technical point: I'm assuming here that "$n\text{ is even}$" is formalized in a natural way, say as $\exists x\, (n=x+x)$, so that $PA$ can prove for each even $n$ that it is even and for each odd $n$ that it is not even.]

The moral of this story is that one must be very careful about how the definition of $S_i$ is to be understood. Because it involves the provability predicate and because $PA$ doesn't prove all the facts that we know about this predicate, it makes a big difference whether the definition is intended to constrain the $S_i$ so that the defining equivalence is provable in $PA$ or merely to constrain them so that the defining equivalence is true. The former, stronger constraint makes, as Will showed, the $S_i$ unique, but the latter constraint does not.

Note also that the "solution" where all the $S_i$ are the set of even numbers is the least fixed-point of the operator as in Andrej's answer (and I think it is the solution that would be produced by the usual proof of the recursion theorem.)

-

You can think of your lines as defining a set $S$ where $\langle n,i\rangle\in S$ means $n\in S_i$.

In each of your examples the right hand side is a $\Sigma^0_1$ condition whose $\Sigma^0_1$ index depends in a computable way on a $\Sigma^0_1$ index for $S$. That is, if $S=W_e$, the $e$th $\Sigma^0_1$ subset of $\mathbb N$, then the right hand side defines $W_{f(e)}$, where $f$ is a total computable function or "program transformation".

In all such cases, by the Recursion Theorem there will be at least one set $S$ satisfying the equivalence (there will be an $e$ with $W_e=W_{f(e)}$). However, there need not be only one such set. Indeed, consider the definition $$n \in S_i \longleftrightarrow n \in S_i$$ which is satisfied by all sets $S$ (in particular, continuum many sets).

-
Thank you! Not only have you provided a great answer, you even read between the lines the true question I was trying (so unsuccessfully) to get at. By the way, this doesn't actually hinge on $\Sigma^0_1$, does it? It would work for any $\Sigma^0_k$ as long as the $k$ is constant (and doesn't depend on which slice of $S$ is being defined at the moment), right? (For example, throw in a new disjunct "or W_n is nonempty" to each right hand side, say.) –  Anonymous Dec 30 '13 at 18:16

You do have uniqueness in your final case. Let $S'(i,n)$ and $S^*(i,n)$ be two fixed points, as described by Andrej Bauer.

As you guessed, we need to use a Godel fixed point argument. The most convenient way to do that will be to apply Lob's theorem.

We will show in PA that if there is a proof in PA that $\forall i \forall n S'(i,n) \iff S^*(i,n)$, then indeed $\forall i \forall n S'(i,n) \iff S^*(i,n)$. This is clear, because then the statements $\mathrm{Prov}_{PA}(\ulcorner \exists j . S^*(i,j) \urcorner)$ and $\mathrm{Prov}_{PA}(\ulcorner \exists j . S'(i,j) \urcorner)$ will be equivalent, so $S^*$ and $S'$ are equivalent.

By Lob's theorem, there is indeed a proof of PA of the equivalence, so they are indeed equivalent.

-
Therefore, each set $S_i$ consists of all of $\mathbb N$. –  Will Sawin Dec 30 '13 at 19:31