Seemingly ill-founded recursion and the recursion theorem

Question

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?

Answer 1

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

Answer 2

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.

Answer 3

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

Answer 4

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.