# Is there a stronger form of recursion?

I'm wondering if there are any recursion principles more general than the following, first given by Montague, Tarski and Scott (1956):

Let $\mathbb{V}$ be the universe, and $\mathcal{R}$ be a well-founded relation such that for all $x\in Fld\mathcal{R}$, $\{y:y\mathcal{R}x\}$ is a set. Further, let $\mathbb{F}$ be a function with $dmn\mathbb{F}=Fld\mathcal{R}\times\mathbb{V}$. Then there exists a unique function $\mathbb{G}$ such that $dmn\mathbb{G}=Fld\mathcal{R}$ and for all $x\in Fld\mathcal{R}$, $$\mathbb{G}(x)=\mathbb{F}(x,\mathbb G\restriction\{y:y\mathcal{R}x\}).$$

Specifically, I would like to be able to drop the requirement that $\{y:y\mathcal{R}x\}$ be a set. I am attempting to define by recursion a function on $O_n\times O_n$ ordered lexicographically, which is a well ordering and consequently a well-founded relation, however $\{y:y<(0,\alpha)\}$ is a proper class for all $\alpha>0$. The proof of the above theorem in the context of MK class theory (and even its statement) rely pretty explicitly on this not happening, however I am aware that category theorists often work in situations where they need to aggregate together many proper classes and manipulate them/construct morphisms between them.

Is there a (perhaps large-cardinal based) strengthening of this theorem that would allow one to legitimately make such a definition by recursion in a class-theoretical context?

• If you would like to see the function in question, it's on page 21 of this paper arxiv.org/pdf/1706.08908.pdf -- note that my proof is invalid for the reasons mentioned here however, so it needs an update. – Alec Rhea Jul 21 '17 at 21:55
• This post just received a downvote for some reason -- is there something I can do to clarify the question better? I've considered this for about a month on my own now and come up with no obvious generalizations, so prior to really digging in and trying to generalize it myself I was wondering if it had already been done. – Alec Rhea Jul 21 '17 at 23:38

Yes, there are such principles. In fact, there is a natural hierarchy of such class-theoretic recursion principles, which form a hierarchy of strength transcending Gödel-Bernays set theory GBC. These principles have become important in the emerging field known as the reverse mathematics of second-order set theory, which seeks to classify various natural second-order set theoretic principles into a hierarchy over GBC.

The principle of elementary transfinite recursion asserts that for any well-ordered class relation $\Gamma$ on a class $I$, not necessarily set-like, and any first-order property $\varphi$, allowing class parameters $Z$, there is a solution $S$, meaning a class $S\subset I\times V$, such that $S_i=\{x\mid \varphi(x,S\upharpoonright i,Z)\}$, where $S\upharpoonright i=\{(j,x)\in S\mid j<_\Gamma i\}$ is the part of the solution below $i$. Thus, we define a class by recursion along $\Gamma$, where at each stage we define a new class in terms of the solution previous to that stage.

One can formalize your function-based recursion using this kind of formalism.

In my recent paper

V. Gitman and J. D. Hamkins, Open determinacy for class games, in Foundations of Mathematics, Logic at Harvard, Essays in Honor of Hugh Woodin’s 60th Birthday, A. E. Caicedo, J. Cummings, P. Koellner, and P. Larson, Eds., American Mathematical Society, 2016. (arxiv:1509.01099)

we proved that ETR is equivalent to the principle of clopen determinacy for class games. Meanwhile, open determinacy is a little stronger, and below $\Pi^1_1$-comprehension.

In my recent paper

V. Gitman, J. D. Hamkins, P. Holy, P. Schlicht, and K. Williams, The exact strength of the class forcing theorem, under review, (arxiv:1707.03700)

we proved that the principle of $\text{ETR}_{\text{Ord}}$, which allows recursions only of length $\text{Ord}$, is equivalent to a list of 12 natural statements, including the class forcing theorem, the existence of truth predicates of various kinds for infinitary logic, the existence of iterated truth predicates for first-order logic, the existence of Boolean set-completions of partial orders, and others.

The picture that is emerging from this analysis is that the natural second-order set theories are ranked by the amount of recursion they support.

• This is exactly what I was looking for and more -- thank you. – Alec Rhea Jul 22 '17 at 1:56
• Great! I'm glad you found it useful. Please feel free to post further questions about ETR if there are any other issues, since it isn't exactly the same as the set-up you described. – Joel David Hamkins Jul 22 '17 at 2:02
• I wonder if you could use these ideas to come up with strong recursion principles in type theory and programming languages. In type theory we know recursion principles which allow one to compute fixed points of universe-forming operators, which amounts more or less to Mahlo cardinals. But nobody has gone beyond that. I see little reason that Mahlo cardinals would present a natural barrier. – Andrej Bauer Jul 22 '17 at 8:56
• @JoelDavidHamkins Much appreciated -- for starters, my paper is written in the context of MK class theory, so if I understand the premise of your paper correctly I should be able to prove ETR directly, no? – Alec Rhea Jul 22 '17 at 15:01
• Incidentally, I just made a blog post at jdh.hamkins.org/… concerning the principle of second-order transfinite recursion, observing that it is equivalent to KM over GBC. – Joel David Hamkins Jul 23 '17 at 16:49