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?
 A: 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.
