How do we justify functions on the Ordinals In ZFC there seem to be two ways to define a function, as an ordered triple of domain, codomain and the set of ordered pairs that make its graph, or a relation over the two sets. 
Whichever we use doesn't matter, but this seems to present a certain problem. Both are defined over sets, but no-one seems to have any problem defining functions on the ordinals like Hartog's function giving the minimum ordinal that doesn't have an injective function on to the given ordinal. I know we want to be able to obviously, but how are we supposed to justify this, because the definitions of functions don't seem to include classes. Or is there a nicer definition I've missed?
 A: Instead of a set, require that a function is a collection of ordered pairs with the property that if $\langle u,x\rangle$ and $\langle u,y\rangle$ are both in the collection then $x=y$.
Classes in ZFC are syntactic objects, these are the definable sub-collections of "$V=\{x\mid x=x\}$", so a class is a collection (which might not be a set) of the form $\{x\mid\varphi(x)\}$ for some $\varphi$.
Ordinal functions, or in general class functions, are (in the context of ZF) definable classes of the form $\{\langle x,y\rangle\mid\varphi(x,y)\}$ which has the functional property. For example the Hartogs number function makes use of the fact that we can define from ZF what are the ordinals, what are injective functions, etc. then using a parameter $x$ we can define the least ordinal which is not injected into $x$. This goes into a formula $\varphi(x,y)$ which says all of the above.
Two simple and even more natural examples of class functions are:


*

*The power set function, $\{\langle x,\mathcal P(x)\rangle\mid x\in V\}$ where $\mathcal P(x)$ denotes the power set of $x$. The axiom of power set tells us that this set exists and extensionality tells us it is unique.

*The union function, $\{\langle x,\bigcup x\rangle\mid x\in V\}$ where $\bigcup x=\{z\mid\exists u(u\in x\land z\in u)\}$. Again we adhere to the axioms, this time to the axiom of union and the axiom of extensionality to argue that this function is well defined.
The von Neumann hierarchy, the Constructible hierarchy, the Fine structure hierarchy, and many other similar ways to construct models of set theory are exactly class-functions from the ordinals.

To read some more:


*

*class function question

*What are some examples of classes that are not sets?

*In NBG set theory how could you state the axiom of limitation of size in first-order logic?
