Data abstraction in set theory via Urelements

Question

I am working in a setting of set theory where set theory is embedded in simply-typed higher-order logic, basically as described for example in

Chad E. Brown and Cezary Kaliszyk and Karol Pak (2019) Higher-Order Tarski Grothendieck as a Foundation for Formal Proof, In: John Harrison and John O'Leary and Andrew Tolmach (eds) 10th International Conference on Interactive Theorem Proving (ITP 2019), Leibniz International Proceedings in Informatics (LIPIcs) 141 pages 9:1--9:16,
doi:10.4230/LIPIcs.ITP.2019.9

or in

Steven Obua (2006) Partizan Games in Isabelle/HOLZF, In: Barkaoui K., Cavalcanti A., Cerone A. (eds) Theoretical Aspects of Computing - ICTAC 2006. ICTAC 2006. Lecture Notes in Computer Science, vol 4281. doi:10.1007/11921240_19.

In particular, there is a type $sigma$ that corresponds to the universe of sets, there is a type $mathbb{P}$ of propositions, and there are types which are higher-order functions $alpha rightarrow beta$ for all types $alpha$ and $beta$. Classes can be represented in this setting by the type $sigma rightarrow mathbb{P}$, for example.
Unlike in the referenced papers, I would also like to allow urelements, that is values of type $sigma$ which are not sets. I am wondering now if the following axiomatic addition would be somehow (obviously?) inconsistent:

EDIT: Due to the inconsistency of the original axioms uncovered by the comment of François G. Dorais, I changed the axioms in the following.

Assume that we have a higher-order function $operatorname{Box} : sigma rightarrow sigma$ which sends sets to urelements in an unambiguous way.
We leave $operatorname{Box}$ unspecified on urelements, and the above can then be expressed more formulaic as follows:

Define $operatorname{Set} : sigma rightarrow mathbb{P}$ via $operatorname{Set}(x) = (x = emptyset vee exists y : sigma., y in x)$
Define $operatorname{Ur} : sigma rightarrow mathbb{P}$ via $operatorname{Ur}(x) = lnot operatorname{Set}(x)$
$forall x : sigma., operatorname{Set}(x) longrightarrow operatorname{Ur}(operatorname{Box}(x))$
$forall x : sigma., forall y : sigma.,(operatorname{Set}(x) wedge operatorname{Set}(y) wedge operatorname{Box}(x) = operatorname{Box}(y)) longrightarrow x = y$

Obviously the other axioms of set theory have to be adapted to account for urelements, but apart from that, would it be OK to add these axioms?
The background for my question is that I would like to use set theory as the basis of a mechanised theorem proving system, but a big problem of set theory as opposed to type theory in that setting is data abstraction. Having a function $operatorname{Box}$ at my disposal should solve that problem.

Steven Obua · Answer

In their CICM 2020 paper

Dunne C., Wells J.B., Kamareddine F. (2020) Adding an Abstraction Barrier to ZF Set Theory. In: Benzmüller C., Miller B. (eds) Intelligent Computer Mathematics. CICM 2020. Lecture Notes in Computer Science, vol 12236. Springer, Cham. doi:10.1007/978-3-030-53518-6_6

the authors introduce ZFP, which is ZF set theory with a primitive notion of ordered pairs $(x, y)$ which are not sets, i.e. they are urelements. They also create a model for ZFP (even in Isabelle/ZF).
Obviously, ZFP can be obtained as a special case via the $operatorname{Box}$ function:
$$(x, y) = operatorname{Box}({x, {x, y}})$$
But, as pointed out to me by Mario Carneiro in a CICM 2020 discussion channel, the other direction is maybe even more obvious as $operatorname{Box}$ can be defined in terms of ordered pairs:
$$operatorname{Box}(x) = (x, x)$$
Thus, the model of ZFP also induces a model for $operatorname{Box}$, and thus boxing is consistent relative to ZF set theory.

Data abstraction in set theory via Urelements

One Answer

Add your own answers!

Ask a Question