Applications of ZFA-Set Theory

Question

The set theory with atoms (ZFA), is a modified version of set theory, and is characterized by the fact that it admits objects other than sets, atoms. Atoms are objects which do not have any elements.

I have thusfar found two applications of ZFA-Set Theory. Firstly, ZFA can be used to prove the independence of the Axiom of Choice.

Secondly, one can show a correspondence between certain ZFA-models and a certain class of groups.

Both of these applications of ZFA make use of so-called permutation models.

I'd like to know what other applications ZFA might have. I would particularly be interested in applications that do not make use of permutation models.

Answer 1

Although you prefer models other than permutation models, let me point out an appearance of permutation models, particularly the basic Fraenkel model, at the border between computer science and logic. The topic concerns operators that bind variables, like $\forall$ and $\exists$ in logic, the $\lambda$ in lambda-calculus, and $\int$ in calculus. The actual variables used with such an operator don't matter, i.e., bound variables can be renamed, as long as there are no clashes. That suggests thinking of variables as atoms in a ZFA universe, thinking of the renaming process as permuting the atoms, and requiring each formula to be invariant under enough permutations (all permutations fixing the formula's free variables). The theory built up from these ideas is called "nominal sets".

Answer 2

Arnold Oberschelp used urelements in his relative consistency proof of a set theory with a universal set and the singleton function as a set. I followed his example in my variant of Alonzo Church’s “Set Theory with a Universal Set,” as Oberschelp’s technique was far easier than Church’s Hilbert Hotel. (Apologies for a bibliography longer than my answer, but the situation is messy in a number of respects; both Oberschelp and Church had uncharacteristic lapses.)

---

• Alonzo Church 1974a. “Set Theory with a Universal Set,” Proceedings of the Tarski Symposium, Proceedings of Symposia in Pure Mathematics XXV, ed. Leon Henkin, American Mathematical Society, ISBN: 978-0821814253, pp. 297-308. (Delivered 24 June 1971.)
• Alonzo Church 1974b. “Notes on a Relative Consistency Proof of Axioms A–K of Church’s Set Theory with a Universal Set,” unpublished lecture notes, Church Archives, box 47, Folder 5.
• Arnold Oberschelp 1964a. “Eigentliche Klasse als Urelemente in der Mengenlehre,” Mathematische Annalen 157 pp. 234-260. [Mathematical Reviews 31#2136]. (Delivered 20 August 1962)
• Arnold Oberschelp 1964b. “Sets and Non-Sets in Set Theory” (abstract), received 3 June 1964, Journal of Symbolic Logic XXIX p. 227
• Arnold Oberschelp 1973. Set Theory over Classes, Dissertationes Mathematicæ (Rozprawy Mat.) 106. [Mathematical Reviews 42 #8300].[29]
• Flash Sheridan 2016. “A Variant of Church’s Set Theory with a Universal Set in which the Singleton Function is a Set” (abridged), in Logique et Analyse, Vol 59, No 233 (2016) pp. 81–131, doi:10.2143/LEA.233.0.3149532. (The full version is available at the Centre National de Recherches de Logique: http://www.logic-center.be/Publications/Bibliotheque/SheridanVariantChurch.pdf .)

[29] Note that the crucial part of the consistency proof in both [Friedrichsdorf 1979] and [Oberschelp 1973] is merely a reference to [Oberschelp 1964a], which uses a significantly different formalism.