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 Σ 0 ‐formula φ ( x ) and a code c for a rudimentary function f , T ( φ , c , $ \vec x $ ) is a Σ ω ‐formula such that for any $ \vec a $ ∈ X , X ′ ⊧ φ [ f ( $ \vec a $ )] iff X ⊧ T ( φ , c , $ \vec x $ )[ $ \vec a $ ]. 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 Σ 0 extender ultrapower of X′ with respect to F , and the ultrapower embeddings agree on X . (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)