To every natural number $n$, we can assign its Church numeral $\underline{n}.$ A formal definition would be:

$\underline{0}(f)=\mathrm{id}_{\mathrm{dom}(f)}$

$\underline{n+1}(f) = \underline{n}(f) \circ f$

where each line is to be understood as implicitly universally quantified over every endofunction $f$. This gives us nifty formulae like:

- $\underline{a} \circ \underline{b} = \underline{a\cdot b}$
- $\underline{a}(f) \circ \underline{b}(f) = \underline{a+b}(f)$

Unfortunately, size issues block the existence of Church numerals inside models of ZFC. But that's fine, we can just move to a class theory with support for this kind of thing.

However there's a more fundamental issue. One of the coolest formulae regarding Church numerals involves their application to *themselves*:

- $\underline{a}(\underline{b}) = \underline{b^a}$

Even for set-functions in ZFC, this kind of self-application is disallowed; if we're furthermore talking about class-functions in one of the usual class theories, then it is somehow "even more disallowed" if that is even possible, since proper classes typically aren't allowed to have (as elements) other proper classes, let alone themselves.

Yet somehow, I am convinced of the sentence "Church numerals exist; they're legitimate mathematical entities." So I ask myself: from a set-theoretic viewpoint, what is a reasonable justification of Church numerals?

I came up with the following idea: to every natural number $n$ and every inaccessible cardinal $\kappa$, let us write $\overline{\kappa}(n)$ for the partial function $V_\kappa \rightarrow V_\kappa$ define inductively as above. Then we can use the standard ZFC existence principles to guarantee that $\overline{\kappa}(n)$ is well-defined for all $n \in \mathbb{N}$.

Furthermore, we can prove that for all natural numbers $n$ and all inaccessible cardinals $\kappa$ and $\nu$, if $\kappa \leq \nu$, then $\overline{\kappa}(n) \subseteq \overline{\nu}(n),$ by which I mean that the latter (partial) function is an extension of the former. Thus in any sufficiently nice class theory, we should be able to define (the proper class) $\underline{n}$ by taking the (class-sized) union of all the $\overline{\kappa}(n).$ That the resulting relation is deterministic should follow from the fact that we've taken a union of deterministic relations.

**We can go further.** Observe that for all natural numbers $n$ and all (set-sized) endofunctions $f$ and $g$, we have that if $f \subseteq g$, then $\underline{n}(f) \subseteq \underline{n}(g).$ Meaning $\underline{n}(f)$ is extended by $\underline{n}(g).$ Intuitively, this allows us to define the meaning of the expression $\underline{a}(\underline{b})$ as a "limit." Just consider the expression $\underline{a}(\overline{\kappa}(b))$ and take the union as $\kappa$ becomes arbitrarily large.

Hence by the above arguments, it should be possible (and useful!) to axiomatize a class theory in which there is formal support not only for proper classes, but also for the evaluation of class functions at other class functions, like Church numerals evaluated at other Church numerals.

Question.Has anyone formally laid out a class theory in which class functions can be self-applied?