Logic of Sets with Atoms
Jake Masters
TL;DR
The paper extends orbit-finite computation from countable atom structures to uncountable ones within set theory with atoms, establishing that finite-support permutation models (PMs) are well-defined and can be captured by automorphism groups. It develops transfer theorems showing that permutation models induced by differing atom-structures can be elementarily equivalent, enabling the transfer of orbit-finite results via structure-induced PMs, and strengthens foundational results by replacing global choice with SVC. It demonstrates the FO-expressibility of key orbit-finite notions inside PMs, and provides forcing-based downward transfer techniques to collapse atom cardinalities while preserving essential structure, including the uniqueness of the first Fraenkel model. Together, these results illuminate when and how orbit-finite constructions transfer across models and offer concrete tools for analyzing computation over atoms in uncountable settings.
Abstract
Orbit-finite models of computation generalise the standard models of computation, to allow computation over infinite objects that are finite up to symmetries on atoms, denoted by $\mathbb{A}$. Set theory with atoms is used to reason about these objects. Recent work assumes that $\mathbb{A}$ is countable and that the symmetries are the automorphisms of a structure on $\mathbb{A}$. We study this set theory to understand generalisations of this approach. We show that: this construction is well-defined and sufficiently expressive; and that automorphism groups are adequate. Certain uncountable structures appear similar to countable structures, suggesting that the theory of orbit-finite constructions may apply to these uncountable structures. We prove results guaranteeing that the theory of symmetries of two structures are equal. Let: $PM(\mathcal{A})$ be the universe of symmetries induced by adding atoms in bijection with $\mathcal{A}$ and considering the symmetric universe; $\underline{\mathcal{A}}$ be the image of $\mathcal{A}$ on the atoms; and $φ^{PM(\mathcal{A})}$ be the relativisation of $φ$ to $PM(\mathcal{A})$. We prove that all symmetric universes of equality atoms have theory $Th(PM(\left\langle \mathbb{N}\right\rangle))$. We prove that for structures $\mathcal{A}$, `nicely' covered by a set of cardinality $κ$, there is a structure $\mathcal{B}\equiv\mathcal{A}$ of size $κ$ such that for all formulae $φ(x)$ in one variable, \begin{equation*} ZFC\vdash φ(\underline{\mathcal{A}})^{PM(\mathcal{A})}\leftrightarrowφ(\underline{\mathcal{B}})^{PM(\mathcal{B})} \end{equation*}