Logic of Sets with Atoms

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; $\underset{‾}{\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(⟨\mathbb{N}⟩))$. 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 φ(\underline{$\mathcal{A}$})^{PM($\mathcal{A}$)}\leftrightarrowφ(\underline{$\mathcal{B}$})^{PM($\mathcal{B}$)} \end{equation*}