I have only little knowledge concerning ordinals and transfinite induction, but I encountered a definition in a paper where a countably infinite set $H$ (the set consists of formulae, but this does not matter) is partitioned into disjoint sets $H_0,\ldots,H_\alpha,\ldots$ where $\alpha < \gamma$ and $\gamma$ is a countable ordinal.
My question is what does this sequence exactly look like in the sense, what effect does this side condition on $\gamma$ have? Can the partition be uncountable in size? As I said, I don't have any knowledge with respect to these things, so I would appreciate an explanation nearly from the scratch (overview articles of Wikipedia did not help me either).
Edit: Here's the definition.
A program $P$ is called locally stratified if it is possible to decompose the Herbrand base $H$ of $P$ into disjoint sets, called strata, $H_0,H_1,\ldots,H_\alpha,\ldots$, where $\alpha < \gamma$ and $\gamma$ is a countable ordinal so that for every ground instance of a clause $A_1,\ldots,A_m,\neg B_1,\ldots,\neg B_n \rightarrow C_1 \vee \cdots C_p$ we have
(i) all the $C_i$ belong to the same stratum, say $P_k$;
(ii) all the positive premises $A_i$ belong to $\bigcup \{P_j : j \leq i\}$;
(iii) all the negative premises $B_i$ belong to $\bigcup \{P_j : j < i\}$.
Thank you!
If $\mathscr{P}$ is a partition of a set $H$, necessarily $|\mathscr{P}|\le|H|$, since the parts of a partition are required by definition to be non-empty. In your case $|H|=\omega$, so if $\mathscr{P}=\{H_\alpha:\alpha<\lambda\}$ is the partition in question, then $|\lambda|=|\mathscr{P}|\le\omega$: either $\mathscr{P}$ is finite, or it’s countably infinite. In particular, $\lambda$ must necessarily be a countable ordinal: $\lambda<\omega_1$, where $\omega_1$ is the smallest uncountable ordinal.
Without seeing the argument, I don’t know why the partition isn’t simply indexed by some finite ordinal if it’s finite and by $\omega(=\Bbb N)$ if it’s countably infinite; I suspect that it has to do with the way the partition is constructed. Specifically, I suspect that $\mathscr{P}$ is constructed by transfinite recursion, so that $H$ might not actually be exhausted when all of the $H_n$ ($n\in\omega$) have been constructed. In that case $\lambda$ is simply the ordinal at which the construction is forced to stop because every member of $H$ has already been included in some $H_\alpha$ with $\alpha<\lambda$, and we know that $\lambda$ is countable for the reason given in the first paragraph.
As a very simple example of what might happen, it’s possible, for instance, that $\lambda=\omega+\omega$, so that the partition consists of the sets
$$H_0,H_1,H_2,\dots,H_n,\dots,H_\omega,H_{\omega+1},H_{\omega+2},\dots,H_{\omega+n},\dots\;.$$
That is, the indexing makes it look like two simple sequences of sets placed end to end. But $\lambda$ could be a much larger, much more complicated-looking countable ordinal. I suspect, however, that there’s no real need to visualize $\lambda$; you probably just need to know that it’s countable (because $H$ is) and perhaps that it gives you a well-ordering of the members of the partition.