What does $\upharpoonright$ in $G(F\upharpoonright\alpha)$ mean?

Question

More formally, we can state the Transfinite Recursion Theorem as follows. Given a class function $G\colon V\to V$, there exists a unique transfinite sequence $F\colon\mathrm{Ord}\to V$ (where $\mathrm{Ord}$ is the class of all ordinals) such that $F(\alpha) = G(F\upharpoonright\alpha)$ for all ordinals $\alpha$. (Wikipedia, transfinite induction)

First question is, what does $\upharpoonright$ mean? Also, what exactly is $F$ in this usage? $F$ seems to be some form of function, but it says its transfinite sequence...

Answer 1

As Brian mentions, the $\upharpoonright$ symbol denotes the restriction of the function (on the left) to the set (on the right).

In the theorem, $F$ is a function whose domain is the class $\mathbf{On}$ of all ordinals. As $\mathbf{On}$ is ordered by $<$ it is nice to think about $F$ instead as a "sequence" indexed by all ordinals: $F = \langle x_\alpha : \alpha \in \mathbf{On} \rangle$ (so that $F(\alpha) = x_\alpha$). Note that given any ordinal $\alpha$ as $\mathbf{On} \cap \alpha = \alpha$ it follows that the restriction $F \upharpoonright \alpha = \left( \langle x_\alpha : \alpha \in \mathbf{On} \rangle \right) \upharpoonright \alpha$ is just the $\alpha$-sequence $\langle x_\xi : \xi < \alpha \rangle$. The theorem then tells us what the $\alpha$th coordinate of $F$ is: $$x_\alpha = G ( \langle x_\xi : \xi < \alpha \rangle ).$$ Note that since $\alpha$ is a set it follows that the restriction $F \upharpoonright \alpha = \langle x_\xi : \xi < \alpha \rangle$ is also set, and is thus a legitimate argument for the function $F$.

---

Depending on the axiom system used, the exact meaning of this theorem may differ.

• If you are using some set theory with classes as objects, then $F$ is just some class which is a function defined on all ordinals. As classes really exist in such theories, we don't have to look any deeper than this.
• More likely, you are instead looking at ZF(C) where the only objects are sets. Then this theorem — theorem schema, actually — says something quite different. Here classes are just notational placeholders for formulae, so $G$ is really some formula $\theta ( x , y , \ldots )$ (with possible parameters), and $G(x) = y$ is an abbreviation for $\theta ( x , y , \ldots )$. The theorem then says that given any appropriate formula $\theta ( x , y , \ldots )$ (one defining a function on all of $\mathbf{V}$) there is another formula $\phi (x , y , \ldots )$ (defining a function on $\mathbf{On}$) such that for any ordinal $\alpha$ we have that $$\phi ( \alpha , y , \ldots ) \Leftrightarrow \theta ( \{ \langle \xi , z \rangle : \xi < \alpha , \phi ( \xi , z , \ldots ) \} , y , \ldots ).$$ The important point here is that such a formula can be constructed, and so we can ignore the fine details of the construction and just think of $F$ as a function in the normal sense; this is, in my opinion, the whole point of introducing classes as meta-linguistic objects in the first place.

Answer 2

$F\upharpoonright\alpha$ is the restriction of the function $F$ to the set $\alpha$. You may be more accustomed to $F|\alpha$ or $F|_\alpha$ for this. Every sequence, transfinite or otherwise, is a function. For instance, a sequence $\langle x_n:n\in\omega\rangle$ of real numbers is just a function $x:\omega\to\Bbb R:n\mapsto x_n$. A sequence $\langle k_0,k_1,\dots,k_{n-1}\rangle$ of natural numbers is just a function $k$ from $n$, thought of as $\{0,1,\dots,n-1\}$, to $\Bbb N$: $k(i)=k_i$.

Here $F$ is a proper class sequence/function defined on the ordinals and taking sets as values. Note that even though $F$ is a proper class, the axiom schema of replacement (together with some of the other axioms) ensures that $F\upharpoonright\alpha$ is a set for every ordinal $\alpha$, so that it is meaningful to talk about $G(F\upharpoonright\alpha)$: $G$ requires sets as input.