Vaught's theorem on axiomatizability by a scheme (Q2915888)

Vaught's set theory \(\mathsf{VS}\) is the theory (in the language with \(=\) and \(\in\)) with the axioms NEWLINE\[NEWLINE\forall x_0,\dots,x_{n - 1} \, \exists y \, \forall u \, (u \in y \leftrightarrow \bigvee_{i < n} u = x_i)\text{ for }n= 0,1,2,\dots.NEWLINE\]NEWLINE A Vaught theory is a theory that directly interprets (that is, the interpretation is not relativized and translates identity to identity) \(\mathsf{VS}\). Vaught's theorem says: all recursively enumerable Vaught theories are axiomatizable by a scheme.NEWLINENEWLINEThe theory of unordered pairing \(\mathsf{VS}_2\) is the theory (in the language with \(=\) and \(\in\)) with (essentially) the axiom \(\forall x_0,x_1 \, \exists y \, \forall u \, (u \in y \leftrightarrow u = x_0 \vee u = x_1)\). A pair theory is a theory that directly interprets \(\mathsf{VS}_2\). The main theorem of the paper under review says: all recursively enumerable pair theories are axiomatizable by a scheme.NEWLINENEWLINEVisser's theorem strictly improves Vaught's theorem (because there are consistent decidable pair theories but all consistent Vaught theories are essentially undecidable).