A metric set theory with a universal set

Motivated by ideas from the model theory of metric structures, we introduce a metric set theory, $\mathsf{MSE}$, which takes bounded quantification as primitive and consists of a natural metric extensionality axiom (the distance between two sets is the Hausdorff distance between their extensions) and an approximate, non-deterministic form of full comprehension (for any real-valued formula $\varphi(x,y)$, tuple of parameters $a$, and $r < s$, there is a set containing the class $\{x: \varphi(x,a) \leq r\}$ and contained in the class $\{x:\varphi(x,a) < s\}$). We show that $\mathsf{MSE}$ is sufficient to develop classical mathematics after the addition of an appropriate axiom of infinity. We then construct canonical representatives of well-order types and prove that ultrametric models of $\mathsf{MSE}$ always contain externally ill-founded ordinals, conjecturing that this is true of all models. To establish several independence results and, in particular, consistency, we construct a variety of models, including pseudo-finite models and models containing arbitrarily large standard ordinals. Finally, we discuss how to formalize $\mathsf{MSE}$ in either continuous logic or {\L}ukasiewicz logic.