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



> 
> 1. $\underline{0}(f)=\mathrm{id}\_{\mathrm{dom}(f)}$
> 2. $\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?
> 
> 
> 



Class theory with support for self-application of class functions?
It seems to me that any of the usual class theories, such as GBC
or KM can handle this (and even ZFC since the relevant classes are
definable), and you have the key to the solution already in your remarks at the end of the question. Namely,
the operation of $\underline n$ on a class function $F$ is
determined by the operation of $\underline n$ on the set-sized (or
even finite) subfunctions of $F$, or in other words $$\underline
n(F)=\bigcup\_{f\subset F}\underline n(f),$$ where $f$ here ranges
over the set-sized functions. Thus, we may represent $\underline n$
as a single class function, which specifies how it operates on
sets, and with the understanding that $\underline n(F)$ is defined
as above, or equivalently $\underline n(F)=\bigcup\_{\alpha\in\text{Ord}}
\underline n(F\upharpoonright V\_\alpha)$. In this way, we can apply
$\underline n$ to other $\underline m$, including $\underline n$
itself, and derive all your interesting equations.


Indeed, since these functionals $\underline n$ are actually
definable classes, one can undertake the whole analysis in ZFC
itself, with no formal class objects. That is, for each
meta-theoretic natural number $n$, we have the definable class
$\underline n$, defined by your recursion (undertaken in the
meta-theory), which set-theoretically is defined only on sets, but
which can be applied to classes including itself by the extension
we have mentioned.


The idea here of extending functions defined on sets to become
defined on classes occurs quite commonly in set theory. For
example, one might have an elementary embedding $j:V\to M$ and
want to apply it to a class $A\subset V$. One can always do this,
by defining $j(A)=\bigcup\_{\alpha\in\text{Ord}} j(A\cap
V\_\alpha)$, with the point being that the right-hand-side
approximations to $j(A)$ increasingly cohere. In the set-theoretic
uses, the original map $j$ is often an elementary embedding, but
the situation here is that one doesn't generally get elementarity
for the extension of $j$ to all classes. For example, ultrapower
embeddings of a GBC universe (or even a KM universe) is not
necessarily elementary in the second-order language with classes
(but with KM+, it is).


A pertinent example occurs in the context of Laver's work on the
left-distributive algebra. He looked at the collection of all
elementary embeddings $j:V\_\lambda\to V\_\lambda$. The two natural
operations here are 


* *composition* $j\circ h$, but also
* *application* $j\cdot h$, pronounced "$j$ applied to $h$", which
is precisely what you are talking about, namely, $j\cdot h:=
\bigcup\_{\alpha<\lambda} j(h\upharpoonright V\_\alpha)$, which might also
be denoted $j(h)$ or "$j$ of $h$".


It is the application operation that leads to the left-distributive algebra, since application obeys $j\cdot(h\cdot k)=(j\cdot h)\cdot(j\cdot k)$, which is to say that application distributes over itself from the left. A similar equation holds for your operations. 


Finally, let me also mention another realm where the idea of
self-application of functions occurs: computability theory. Turing
machine programs can accept other Turing machine programs as
input, including themselves, and your Church numeral idea seems to
work out fine in that context. Indeed, such kind of
self-application is fundamental to the Recursion Theorem, which is
applied throughout the subject.


