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)141pages 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, vol4281. 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.

13more comments