  Whilst Power Kripke-Platek set theory, KPP, shares many properties with
ordinary Kripke-Platek set theory, KP, in several ways it behaves quite
differently from KP. This is perhaps most strikingly demonstrated by a result,
due to Mathias, to the effect that adding the axiom of constructibility to KPP
gives rise to a much stronger theory, whereas in the case of KP the
constructible hierarchy provides an inner model, so that KP and KP+V=L have the
same strength. This paper will be concerned with the relationship between KPP
and KPP plus the axiom of choice or even the global axiom of choice, GAC. Since
L is the standard vehicle to furnish a model in which this axiom holds, the
usual argument for demonstrating that the addition of AC or GAC to KPP does not
increase proof-theoretic strength does not apply in any obvious way. Among
other tools, the paper uses techniques from ordinal analysis to show that
KPP+GAC has the same strength as KPP, thereby answering a question of Mathias.
Moreover, it is shown that KPP+GAC is conservative over KPP for Pi-1-4
statements of analysis. The method of ordinal analysis for theories with power
set was developed in an earlier paper. The technique allows one to compute
witnessing information from infinitary proofs, providing bounds for the
transfinite iterations of the power set operation that are provable in a
theory. As the theory KPP+GAC provides a very useful tool for defining models
and realizability models of other theories that are hard to construct without
access to a uniform selection mechanism, it is desirable to determine its exact
proof-theoretic strength. This knowledge can for instance be used to determine
the strength of Feferman's operational set theory with power set operation as
well as constructive Zermelo-Fraenkel set theory with the axiom of choice.
