Skip to main content
2 of 2
replaced http://mathoverflow.net/ with https://mathoverflow.net/

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.

Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239