Successor levels of the Jensen hierarchy

I prove that there is a recursive function T that does the following: Let X be transitive and rudimentarily closed, and let X ′ be the closure of X ∪ {X } under rudimentary functions. Given a Σ₀‐formula φ (x) and a code c for a rudimentary function f, T (φ, c, ) is a Σ_ω ‐formula such that for any ∈ X, X ′ ? φ [f ( )] iff X ? T (φ, c, )[ ]. I make this precise and show relativized versions of this. As an application, I prove that under certain conditions, if Y is the Σ_ω extender ultrapower of X with respect to some extender F that also is an extender on X ′, then the closure of Y ∪ {Y } under rudimentary functions is the Σ₀ extender ultrapower of X′ with respect to F, and the ultrapower embeddings agree on X. (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)