Simplified cut elimination for Kripke-Platek set theory

The purpose of this article is to present a new and simplified cut elimination procedure for KP. We start off from the basic language of set theory and add constants for all elements of the constructible hierarchy up to the Bachmann-Howard ordinal ψ(εΩ+1). This enriched language is then used to set up an infinitary proof system IP whose ordinal-theoretic part is based on a specific notation system C(εΩ+1,0) due to Buchholz and his idea of operator controlled derivations. KP is embedded into IP and complete cut elimination for IP is proved.