3
$\begingroup$

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:

  1. Define $\operatorname{Set} : \sigma \rightarrow \mathbb{P}$ via $\operatorname{Set}(x) = (x = \emptyset \vee \exists y : \sigma.\, y \in x)$
  2. Define $\operatorname{Ur} : \sigma \rightarrow \mathbb{P}$ via $\operatorname{Ur}(x) = \lnot \operatorname{Set}(x)$
  3. $\forall x : \sigma.\, \operatorname{Set}(x) \longrightarrow \operatorname{Ur}(\operatorname{Box}(x))$
  4. $\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.

Improve this question
$\endgroup$
18
  • $\begingroup$ Actually, looking at the definition, I don't see a reason not to declare $\emptyset$ an urelement as well, so an alternative definition of $\operatorname{Ur}$ could be: $$\operatorname{Ur}(x) = \forall y : \sigma.\,y \notin x$$ $\endgroup$
    – Steven Obua
    Jul 19, 2020 at 13:39
  • 1
    $\begingroup$ There's no issue unless you want the urelements to form a set. In that case, the injectivity requirement will be problematic. $\endgroup$
    – François G. Dorais
    Jul 19, 2020 at 21:43
  • $\begingroup$ That's great to hear! No, I don't need the urelements to form a set. $\endgroup$
    – Steven Obua
    Jul 20, 2020 at 3:34
  • $\begingroup$ Do you intend to allow $\mathrm{Box}$ to be used in separation instances in your basic set-theory or is it just an addition on top? $\endgroup$
    – François G. Dorais
    Jul 20, 2020 at 10:04
  • 1
    $\begingroup$ Actually, there is a problem: for any $x$ we have $\operatorname{Box}(\operatorname{Box}(x)) = \operatorname{Box}(x)$ by 2 & 3, but then $\operatorname{Box}(x) = x$ by 4. I recommend dropping 3. $\endgroup$
    – François G. Dorais
    Jul 20, 2020 at 23:29

1 Answer 1

Reset to default
2
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Does this not beg the question: why only admit pairs as primitive, and not other objects, such as elements of disjoint sums and quotients? $\endgroup$
    – Andrej Bauer
    Jul 29, 2020 at 14:54
  • $\begingroup$ You can just consider it as a convenient tool to provide consistency for free because the ZFP paper has already been written. You can use $\operatorname{Box}$ to construct all sorts of data types. $\endgroup$
    – Steven Obua
    Jul 29, 2020 at 18:55

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .