# Transfinite induction vs transfinite recursion

Let $\mathfrak{A}$ is a well-ordered set.

Let $f$ is a function which maps a start segment $\{ i\in\mathfrak{A} \,|\, i<c \}$ of a transfinite sequence of elements of atomic posets into an element of an atomic poset (to every $c\in\mathfrak{A}$ corresponds a poset).

Let a transfinite sequence $a$ on $\mathfrak{A}$ is defined by the formula:

$a_c = \Phi f\left(a|_{\{ i\in\mathfrak{A} \,|\, i<c \}}\right)$

where $\Phi$ is a function which maps an element of a poset into an atom under this element.

We have the axiom (in fact a theorem which follows from my definition of $f$ which I don't put here) that provided $a$ conforms to this formula, $f\left(a|_{\{ i\in\mathfrak{A} \,|\, i<c \}}\right)$ is a non-least element of the poset corresponding to $c$ and thus $\Phi f\left(a|_{\{ i\in\mathfrak{A} \,|\, i<c \}}\right)$ is correctly defined.

Now I am confused: to prove that such $a$ exists, is it transfinite induction or transfinite recursion? The formula $a_c = \Phi f\left(a|_{\{ i\in\mathfrak{A} \,|\, i<c \}}\right)$ looks like transfinite induction. But to prove that $f\left(a|_{\{ i\in\mathfrak{A} \,|\, i<c \}}\right)$ is a non-least looks like a transfinite recursion.

My questions:

• What is this: transfinite induction, transfinite recursion, or a combination of these two?
• How to describe all this in terms of transfinite induction and transfinite recursion?

Note: I intentionally ignore the "set of all sets" paradox, because it is not the thing I have trouble with.

Note: I want to define $\Phi$ using axiom of choice as an arbitrary function which maps a non-least element into an atom under this element.

-

Your definition of $a$ is transfinite recursion. The proof that $a$ behaves well is transfinite induction. You should however be clear if your $f$ and $\Phi$ are already "given" or if you build them up in parallel to your definition of $a$.
To simplify matters, it may be best to extend $f$ and $\Phi$ in such a way that they return a "default" value e.g. $\emptyset$ if the input $a|_\ldots$ is not well-behaved. This allows you to put everything in order: First you have $f$ and $\Phi$, then you define $a$ b yrecursion (which may end in $\emptyset$'s, but is defined once and for all), then you show by induction that the "default" never occurs.