Class theory with support for self-application of class functions?

Question

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?

Answer 1

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.