Positive set theory is an approach to rectifying Russel's paradox by restricting the syntactic form of formulas for which we allow comprehension. It can be motivated by the construction of certain topological models. Specifically, there exists a (unique) compact Hausdorff space $X$ which is homeomorphic to its own hyperspace $\mathcal{K}(X)$ (collection of closed subsets with the Vietoris topology). This induces a set membership relation $\in$ on $X$ which is closed in $X^2$. The structure $(X,\in)$ satisfies the following axioms (which I think are called $\mathsf{GPK}^+$):
- Extensionality.
- Generalized Positive Comprehension: For any generalized positive formula $\varphi(x,\bar{y})$ and any parameters $\bar{a}$, the set $\{x : \varphi(x,\bar{a})\}$ exists.
- Closure: For any formula $\varphi(x,\bar{y})$ and any parameters $\bar{a}$, there is a smallest set containing the class $\{x : \varphi(x,\bar{a})\}$.
A generalized positive formula is a formula in the smallest class containing $\bot$, $x = y$, and $x \in y$ and closed under variable substitution, conjunction, disjunction, quantification, and bounded quantification (although bounded quantification subsumes unbounded quantification, since in this context there is a universal set).
By modifying the construction of $X$, one can, for any compact Hausdorff space $A$, produce a (unique) compact Hausdorff space $X(A)$ with the properties that $X(A)$ is homeomorphic to $\mathcal{K}(A \sqcup X(A))$. The idea here, of course, is that $A$ is a set of urelements.
If we fix a language $\mathcal{L}$ and let $A$ be a finite set endowed with some $\mathcal{L}$-structure, then the two-sorted structure $(X(A),A,\in,...)$ (where $...$ is the non-logical symbols in $\mathcal{L}$) is a model of set theory with urelements that satisfies direct analogs of the axioms of $\mathsf{GPK}^+$—extensionality, generalized positive comprehension, and closure—where now the schemas range over formulas in the full language and generalized positive formulas are the smallest class of formulas containing $\bot$, $x=y$, $x \in y$, and all atomic $\mathcal{L}$-formulas and their negations (including $x\neq y$ in the urelement sort) and closed under variable substitution, conjunction, disjunction, quantification, and bounded quantification. Call this theory $\mathsf{GPKU}^+$. (Incidentally, I can't actually figure out what $\mathsf{GPK}$ stands for.)
We'll say that an $\mathcal{L}$-theory $T$ is consistent with $\mathsf{GPKU}^+$ if $T \cup \mathsf{GPKU}^+$ is consistent (i.e., if there is a model $A$ of $T$ that can be expanded to a model $(A,S,\dots)$ of $\mathsf{GPKU}^+$). By a standard compactness argument, there is an $\mathcal{L}$-theory $T_{\mathsf{GPKU}^+}$ with the property that $T$ is consistent with $\mathsf{GPKU}^+$ if and only if $T \cup T_{\mathsf{GPKU}^+}$ is consistent. Furthermore, since the axioms of $\mathsf{GPKU}^+$ are computably enumerable, this theory can be taken to be computably enumerable. (Assume that we have a fixed computable enumeration of $\mathcal{L}$.)
By the above discussion, any theory of a finite structure is consistent with $\mathsf{GPKU}^+$, and so any pseudo-finite theory is consistent with $\mathsf{GPKU}^+$. We know, however, that this cannot be a characterization of consistency with $\mathsf{GPKU}^+$. To see this, note that there is an $\mathcal{L}$-theory $T_{\text{PFin}}$, with the property that a complete theory $T$ is pseudo-finite if and only if it entails $T_{\text{PFin}}$. $T_{\text{PFin}}$ is the set of all $\mathcal{L}$-sentences that hold in all finite $\mathcal{L}$-structures. This theory is easily seen to be co-c.e., but more than this is it not computable (for $\mathcal{L}$ with enough symbols of high enough arity) since one can rephrase the halting problem as a question about the existence of finite models of certain first-order theories.
This means that $T_{\mathsf{GPKU}^+}$ cannot entail all of $T_{\text{PFin}}$, so there are non-pseudo-finite theories that are consistent with $T_{\mathsf{GPKU}^+}$. It is fairly easy to construct an example of this using the recursion theorem: Take the (finite) $\mathcal{L}$-theory $T_e$ that codes the computation of the $e$th Turing machine on a blank input and let $e$ be the index of the Turing operator that halts whenever it finds a proof that $T_e \cup T_{\mathsf{GPKU}^+}$ is inconsistent. (Since this theory is finite, if it were pseudo-finite, then it would have a finite model, implying that the computation $e$ halts, but this would mean that $T_e$ is inconsistent with $\mathsf{GPKU}^+$, which is a contradiction.)
It is tempting to ask about 'natural' examples of non-pseudo-finite theories that are consistent with $\mathsf{GPKU}^+$, but naturalness is a slippery concept and besides there is a much more immediate question that I do not know the answer to:
Question: Is there a theory $T$ that is not consistent with $\mathsf{GPKU}^+$?
