Abstract In the first part of this paper, we consider several natural axioms in urelement set theory, including the Collection Principle, the Reflection Principle, the Dependent Choice scheme and its generalizations, as well as other axioms specifically concerning urelements. We prove that these axioms form a hierarchy over $\text {ZFCU}_{\text {R}}$ (ZFC with urelements formulated with Replacement) in terms of direct implication. The second part of the paper studies forcing over countable transitive models of $\text {ZFU}_{\text {R}}$ . We propose a new definition of ${\mathbb P}$ -names to address an issue with the existing approach. We then prove the fundamental theorem of forcing with urelements regarding axiom preservation. Moreover, we show that forcing can destroy and recover certain axioms within the previously established hierarchy. Finally, we demonstrate how ground model definability may fail when the ground model contains a proper class of urelements.

Abstract After reviewing various natural bi-interpretations in urelement set theory, including second-order set theories with urelements, we explore the strength of second-order reflection in these contexts. Ultimately, we prove that second-order reflection with the abundant atom axiom is bi-interpretable and hence also equiconsistent with the existence of a supercompact cardinal. The proof relies on a reflection characterization of supercompactness, namely, a cardinal $\kappa $ is supercompact if and only if every $\Pi ^1_1$ sentence true in a structure M (of any size) containing $\kappa $ in a language of size less than $\kappa $ is also true in a substructure $m\prec M$ of size less than $\kappa $ with $m\cap \kappa \in \kappa $ .