Axiomatization and Forcing in Set Theory with Urelements

TL;DR

This paper explores axioms in urelement set theory, establishing their hierarchy, and develops forcing techniques over models with urelements, revealing how axioms can be preserved or destroyed and examining ground model definability issues.

Contribution

It introduces a hierarchy of axioms in urelement set theory and proposes a new approach to forcing over models with urelements, including fundamental theorems and definability results.

Findings

Axioms form a hierarchy over ZFC with urelements.

New definition of forcing with urelements ensures axiom preservation.

Forcing can destroy and recover axioms; ground model definability may fail.

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 $\ZFCUR$ (ZFC with urelements formulated with Replacement) in terms of direct implication. The second part of the paper studies forcing over countable transitive models of $\ZFUR$. We propose a new definition of $\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.