Why are extenders defined using finite sequences?

152 Views Asked by At

My question is inspired by definitions 3.1 and 3.2 (3) of "Double helix in large large cardinals and iteration of elementary embeddings" by Kentaro Sato 2007 but I think my question is relevant to what most set theorists call extenders, despite Sato's unusual terminology. The relevant part of definition 3.1 is:

For ordinals $\mu \le \lambda$, partition space(s) [...] $\mathcal{E}_{\lambda,\mu}$ [is] defined as follows: $$\mathit{P} \in \mathcal{E}_{\lambda,\mu} \iff (\exists \mathit{a} \subset \lambda)(\vert\mathit{a}\vert \lt \omega \And \mathit{P} \sqsupset \{\{\mathit{s} \in D(\mathcal{E}_{\lambda,\mu} \mid \mathit{s}\upharpoonright\mathit{a} = \mathit{f} \} \mid \mathit{f} \in ^\mathit{a}\mu \})$$

Why are the sets $\mathit{a}$ (which determine whether functions $\mathit{s}$ belong to a given $\mathit{E}$-large set for some ultrafilter $\mathit{E}$) restricted to be finite? With higher bounds on the size of $\mathit{a}$ I can probably prove closure properties of ultrapowers by ultrafilters of $\mathcal{E}_{\lambda,\mu}$ (extenders), which would be useful for placing ultrahuge cardinals in the large cardinal hierarchy, but with the bound $\omega$ it's not obvious to me that the ultrapower is even countably closed.