# What is a 'power admissible model'?

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 Kripke-Platek 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})$, 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.

• I guess that like He-Man, these models HAVE THE POWERRRRRRRRRRR!!!!! (And they are admissible, of course.) Dec 22 '16 at 17:10

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)
• In this paper, Mathias also includes the axiom of infinity and the powerset axiom in $\operatorname{KP}^{\mathcal{P}}$. Infinity is fine with me, as it will always hold in the structures I am interested in. Also, since all my models are transitive, I have full foundation for free. However, the powerset axiom typically fails. Including the powerset axiom in $\operatorname{KP}^{\mathcal{P}}$ seems curious to me, as - on first sight - it appears to render the additional predicate $\mathcal{P}$ rather pointless... I'll think about it for a little while. Dec 22 '16 at 18:26
• Recall that you only have $\Delta_0^{\mathcal{P}}$-collection and separation! (Although Adrian shows that the $\Delta_1^{\mathcal{P}}$ versions follow) This does not let you do much with power sets, since the power-set axiom has a higher complexity. Thus, adding the power-set operator as primitive sidesteps this and results in a stronger theory.
• Right. On first instinct I thought that adding the predicate $\mathcal{P}$ may end up pushing the complexity of the powerset axiom to $\Delta_0^{\mathcal{P}}$, but that's not the case. After checking the papers once again, I'm fairly convinced that Steel's power admissibility is the one you linked to, but without the powerset axiom. Thanks for your help! Dec 23 '16 at 10:46