**Q:** What exactly is a power admissible model?


**Background:** Admissible models, introduced by Jon Barwise, form the building blocks of inner model theory. They are transitive models $\mathcal M = (M; \in)$ satisfying a suitable fragment of set theory, namely **K**ripke-**P**latek set theory. Sifting through a couple of papers by John Steel, the term *power admissible model* sprung up a few times and since no definition or reference was given, I more or less assumed that they were just admissible models with enough closure properties such that the given argument would work.


Today I decided to take a closer look at them and after some online research I found a definition of power admissible sets in [Cook, Rathjen. Classifying the Provably Total set Functions of $\operatorname{KP}$ and $\operatorname{KP}(\mathcal{P})$](http://www.collegepublications.co.uk/downloads/ifcolog00008.pdf), namely Definition 8.2. According to them, a transitive model $\mathcal{M} = (M; \in)$ is *power admissible* iff it satisfies $\operatorname{KP}^{\mathcal{P}}$, the extension of $\operatorname{KP}$ to formulae in $\mathcal L = \{ \in, \mathcal{P}\}$, interpreting, for any $x, y \in \mathcal{M}$,
$$
\mathcal{P}^{\mathcal{M}}(x,y) \iff y \subseteq x.
$$
It seems very likely to me that this is in fact the kind of structure Steel has in mind. However, since I am interested in some technical details of his constructions that rely on the precise properties of $\mathcal{M}$, I'd like to verify this educated guess.



What is a 'power admissible model'?
Stefan, in the paper "The Strength of Mac Lane Set Theory," Mathias says that the notion is due to Harvey Friedman, and essentially coincides with what you describe, except that in KP$^P$, foundation is restricted to universal formulae. (See page 47 of Mathias' paper 
<https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf>)


