Logic of Sets with Atoms

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 $\phi ^{PM(\mathcal{A})}$ be the relativisation of $\phi$ 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 $\kappa$, there is a structure $\mathcal{B}\equiv\mathcal{A}$ of size $\kappa$ such that for all formulae $\phi(x)$ in one variable, \begin{equation*} ZFC\vdash \phi(\underline{\mathcal{A}})^{PM(\mathcal{A})}\leftrightarrow\phi(\underline{\mathcal{B}})^{PM(\mathcal{B})} \end{equation*}