A few years ago, I had observed after hearing a talk by Benjamin Rin that the principle of firstorder transfinite recursion for set wellorders is equivalent to the replacement axiom over Zermelo set theory, and thus we may take transfinite recursion as a fundamental settheoretic principle, one which yields full ZFC when added to Zermelo’s weaker theory (plus foundation).
In later work, Victoria Gitman and I happened to prove that the principle of elementary transfinite recursion ETR, which allows for firstorder class recursions along proper class wellorders (not necessarily setlike) is equivalent to the principle of determinacy for clopen class games [1]. Thus, once again, a strong recursion principle exhibited robustness as a fundamental settheoretic principle.
The theme continued in recent joint work on the class forcing theorem, in which Victoria Gitman, myself, Peter Holy, Philipp Schlicht and Kameryn Williams [2] proved that the principle $\text{ETR}_{\text{Ord}}$, which allows for firstorder class recursions of length $\text{Ord}$, is equivalent to twelve natural settheoretic principles, including the existence of forcing relations for class forcing notions, the existence of Boolean completions for class partial orders, the existence of various kinds of truth predicates for infinitary logics, the existence of $\text{Ord}$iterated truth predicates, and to the principle of determinacy for clopen class games of rank at most $\text{Ord}+1$.
A few days ago, a MathOverflow question of Alec Rhea’s — Is there a stronger form of recursion? — led me to notice that one naturally gains additional strength by pushing the recursion principles further into secondorder set theory.
So let me introduce the secondorder recursion principle STR and make the comparatively simple observation that over GödelBernays GBC set theory this is equivalent to KelleyMorse set theory KM. Thus, we may take this kind of recursion as a fundamental settheoretic principle.
Definition. In the context of secondorder set theory, the principle of secondorder transfinite recursion, denoted STR, asserts of any formula $\varphi$ in the secondorder language of set theory, that if $\Gamma=\langle I,\leq_\Gamma\rangle$ is any class wellorder and $Z$ is any class parameter, then there is a class $S\subset I\times V$ that is a solution of the recursion, in the sense that
$$S_i=\{\ x\ \mid\ \varphi(x,S\upharpoonright i,Z)\ \}$$
for every $i\in I$, where where $S_i=\{\ x\ \mid\ (i,x)\in S\ \}$ is the section on coordinate $i$ and where $S\upharpoonright i=\{\ (j,x)\in S\ \mid\ j<_\Gamma i\ \}$ is the part of the solution at stages below $i$ with respect to $\Gamma$.
Theorem. The principle of secondorder transfinite recursion STR is equivalent over GBC to the secondorder comprehension principle. In other words, GBC+STR is equivalent to KM.
Proof. KelleyMorse set theory proves that every secondorder recursion has a solution in the same way that ZFC proves that every setlength wellordered recursion has a solution. Namely, we simply consider the classes which are partial solutions to the recursion, in that they obey the recursive requirement, but possibly only on an initial segment of the wellorder $\Gamma$. We may easily show by induction that any two such partial solutions agree on their common domain (this uses secondorder comprehension in order to find the least point of disagreement, if any), and we can show that any given partial solution, if not already a full solution, can be extended to a partial solution on a strictly longer initial segment. Finally, we show that the common values of all partial solutions is therefore a solution of the recursion. This final step uses secondorder comprehension in order to define what the common values are for the partial solutions to the recursion.
Conversely, the principle of secondorder transfinite recursion clearly implies the secondorder comprehension axiom, by considering recursions of length one. For any secondorder assertion $\varphi$ and class parameter $Z$, we may deduce that $\{x\mid \varphi(x,Z)\}$ is a class, and so the secondorder class comprehension principle holds. $\Box$
It is natural to consider various fragments of STR, such as $\Sigma^1_n\text{}\text{TR}_\Gamma$, which is the assertion that every $\Sigma^1_n$formula $\varphi$ admits a solution for recursions of length $\Gamma$. Such principles are provable in proper fragments of KM, since for a given level of complexity, we only need a corresponding fragment of comprehension to undertake the proof that the recursion has a solution. The full STR asserts $\Sigma^1_\omega\text{}\text{TR}$, allowing any length. The theorem shows that STR is equivalent to recursions of length $1$, since once you get the secondorder comprehension principle, then you get solutions for recursions of any length. Thus, with secondorder transfinite recursion, a little goes a long way. Perhaps it is more natural to think of transfinite recursion in this context not as axiomatizing KM, since it clearly implies secondorder comprehension straight away, but rather as an apparent strengthening of KM that is actually provable in KM. This contrasts with the firstorder situation of ETR with respect to GBC, where GBC+ETR does make a proper strengthening of GBC.

 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., , 2016, Newton Institute preprint ni15064.
[Bibtex]
@INCOLLECTION{GitmanHamkins2016:OpenDeterminacyForClassGames,
author = {Victoria Gitman and Joel David Hamkins},
title = {Open determinacy for class games},
booktitle = {{Foundations of Mathematics, Logic at Harvard, Essays in Honor of Hugh Woodin's 60th Birthday}},
publisher = {},
year = {2016},
editor = {Andr\'es E. Caicedo and James Cummings and Peter Koellner and Paul Larson},
volume = {},
number = {},
series = {AMS Contemporary Mathematics},
type = {},
chapter = {},
pages = {},
address = {},
edition = {},
month = {},
note = {Newton Institute preprint ni15064},
url = {http://wp.me/p5M0LV1af},
eprint = {1509.01099},
archivePrefix = {arXiv},
primaryClass = {math.LO},
abstract = {},
keywords = {},
}