A note on ${\cal P}$-admissible sets with urelements.
Judy Green · Notre Dame Journal of Formal Logic · 1975
In [2] Barwise states that although the introduction of urelements into Zermelo-Fraenkel set theory is redundant, their introduction into the weaker Kripke-Platek theory for admissible sets is not.In this note* we will show that their introduction into the intermediate theory of power set admissible sets is once again redundant since all /'-admissible sets with urelements are of the same form as /^-admissible sets, i.e., V M M = H M (/ and the language in which it is formulated (see [2]).We also assume familiarity with the hierarchy of set theoretic predicates due to Levy [5], and the primitive recursive set functions of Jensen and Karp [4].We expand the notation of [2] as follows:Definition: A structure Sl^ (9W; A, E, P,...) for the language L(e, P, . ..) consists of (1) a structure 9JΪ = (M, . ..) for the language L, (2) a nonempty set A disjoint from M, (3) a relation E c (M U A) x A to interpret e, (4) a function P from A into A to interpret P, and (5) other functions, relations, and constants on MUA which interpret the other symbols in L(e, P, . ..).