Is there any research on set theory without extensionality axiom?

Question

In practice (say, in computer science), collections with many "labels" ("identities"), or collections which occur in many copies, are more frequently used than sets. Such collections do not satisfy the extensionality axiom, i.e. two different such collections A and B can have same elements (I would then say that A and B are "extensionally equivalent"). I am aware that extensionality axiom is independent of other axioms in ZF and possibly in other axiomatic set theories.

Is there any (systematic) research of a set theory without extensionality axiom? Say, how a model of such a theory can be obtained in ZF, or whether the model of such a theory ratio the "extensionality equivalence" is a model of a set theory with extensionality axiom? It sounds probable that such collections have to do with multisets, i.e. sets, the elements of which can occur in many copies - the atoms must be allowed to occur in many copies, once such collections can have many copies). By the way, is there an axiomatized multiset theory?

Answer 1

Going the other direction, it turns out that classical ZF (using collection + separation) can be embedded in the theory where you drop extensionality---everything in classical set theory is still possible in a sense even when extensionality is not available. The idea is that when one lacks extensionality, one may recover it by defining an equivalence of sets, namely, that of having the same members, but then one wants really to define sets as equivalent when they have equivalent members, and so in in a transfinite refining process of the equivalence relation. The result is that in any model of ZF- without extensionality, one can define a corresponding model of ZF.

This is proved in Harvey Friedman, The consistency of classical set theory relative to a set theory with intuitionistic logic, J. Symbolic Logic 38 (1973), 315--319. The main point of the article is not this extensionality issue, but rather to embed classical ZF in an intuitionist logical system.

So although the axiom of extensionality seems fundamental to set theory—and one can find many instances in the literature describing extensionality as the most fundamental axiom—in fact one does not need it to develop set theory.

The theory used in that article is a theory of the kind you seek, a set theory lacking extensionality.

Meanwhile, as Asaf Karagila points out in the comments below, one cannot expect to recover classical ZF in the version of ZF without extensionality, if this is axiomatized with replacment rather than collection. This is because Dana Scott proved that this version of ZF-E is interpretable in Z, and so the consistency strength is strictly less than full ZF, if consistent.

• Dana Scott, More on the axiom of extensionality, 1961 Essays on the foundations of mathematics pp. 115–131 Magnes Press, Hebrew Univ., Jerusalem.

My perspective on this result is that it shows that we should not axiomatize ZF-E using only replacement, since Scott's model violates the collection axiom in the same way that the Zermelo universe $V_{\omega+\omega}$ violates collection. A similar issue arises in other weakenings of ZFC, such as in the case of ZFC-powerset and ZFC-foundation, where one should typically use collection+separation rather than replacement.

Answer 2

There is a bunch of works on set theories featuring the naive (Cantor-style) comprehension axiom, over logics weaker than classical (such as, fragments of linear logic and their extensions), which abstain from extensionality because its presence introduces the contraction principle and, in tow, a contradiction. 1 gives the gist and a sample of references.

Two more comments: I don't think "practice" is a good enough impulse for omitting extensionality from ZF, because practice usually won't make use of all the strata ZF has to offer. Second, if "without extensionality" means just the omission of the axiom Ext, then the model of such a theory is easy to imagine since any model of ZF is also a model of ZF without Ext.