# Can we effectively define a theory of all upward absolute sentences over theories of hereditarily bounded sets?

Lets' take the theory of hereditarily bounded sets[1][2]. We know that every $$S_k$$ where $$k \in \omega$$ is decidable and has as its canonical model the set $${\sf H}_k$$ of all sets hereditarily of size at most $$k$$.

Can we recursively define a theory $$\cal S$$ in the language of set theory whose sentences are those that are upward absolute over sequence of structures $$({\sf H}_k)_{k \in \omega}$$. That is, any sentence $$\psi$$ such that there is some $$l \in \omega$$ such that $${\sf H}_l \models \psi$$ and such that for any $$k > l; k \in \omega$$, we have: $${\sf H}_k \models\psi$$; then $$\psi$$ is an axiom of $$\mathcal S$$. So, we do have axioms of $$V_n$$ for $$n \in \omega$$, Extensionality, and the Acyclicity axioms $$C_n$$; and on top of those we have the upward absolute sentences.

Here is the exposition of theories $$S_k$$ where $$k \in \omega$$.

Let $$k \in \omega$$. The theory $$S_k$$ in the language of set theory $$\langle \in \rangle$$ [it extends first order logic with equality, so "$$=$$" is considered a logical constant, and all axioms of equality are there] is axiomatized by

$$(V_\emptyset) \space \space \space \exists x \forall y: y \not\in x$$

$$(V_n) \space \space \space \forall x_1,\cdots, \forall x_n \exists y \forall t \, (t \in y \leftrightarrow \underset {0

for all $$n \in \omega, n>0$$.

$$(E) \space \space \space \forall x \forall y \, (\forall t \, (t \in x \leftrightarrow t \in y) \to x=y)$$

$$(B_k) \space \space \space \forall y,x_0,\dots,x_k\,\bigl(\bigwedge_ix_i\in y\to\bigvee_{i\ne j}x_i=x_j\bigr)$$

$$(C_n) \space \space \space \forall x_0,\cdots,\forall x_n \neg(\underset{i

for all $$n \in \omega$$. Prohibiting finite $$\in$$-cycles.

So, $$S$$ is kind of a merger theory of all $$S_k$$ theories, maintaining all of what is upwardly absolute in these theories.

If we cannot recursively define $$\cal S$$, then is it complete?

• Any consistent theory that includes all the $V_n$ (including $n=0$) is undecidable. Commented May 4 at 11:56
• It's obviously consistent, as any finite subset has a model. I don't know how to meaningfully define "consistency strength" of something that, on the face of it, does not even look recursively axiomatizable. Consistency strength is not a property of a theory, but of (a formula that defines) a set of axioms for the theory. Commented May 4 at 12:21
• Another take on “consistency strength” is that if I define an axiom set for $S$ directly by the formula $\exists n\,\forall m\ge n\,S_m\vdash\phi$ (which is $\Sigma_3$, but equivalent to a $\Sigma_2$ formula in any metatheory that proves the completeness of the $S_n$’s), then the ($\Pi_3$, or $\Pi_2$ under the condition from the previous comment) sentence expressing its consistency is implied by $\forall n\,\mathrm{Con}_{S_n}$, which I’m pretty sure is provable in $I\Delta_0+\mathrm{SUPEXP}$ by formalizing the decision procedure in my paper. Commented May 4 at 12:48
• $\cal S$ isn't complete, it doesn't prove or disprove "the largest natural number is even". Commented May 4 at 12:58
• The theory is not complete, as it does not decide the truth of the sentence “the largest Von Neumann natural number is even” (where “even” means, say, that it has a partition to two-element sets). The point is that this holds in $S_k$ for $k$ even, and fails when $k$ is odd. (I see that this was just mentioned by paste bee. I’ll leave the comment here anyway as it has a bit more details.) Commented May 4 at 12:58

Here's a very easy argument showing that $$\mathcal{S}$$ is not computably axiomatizable: each $$\Pi_1$$ (in the Levy hierarchy) sentence $$\psi$$ will be in $$\mathcal{S}$$ iff it is satisfied by $$V_\omega$$. So the $$\Pi_1$$ consequences of $$\mathcal{S}$$ are co-c.e. complete, but (since being $$\Pi_1$$ is a computable property) the set of $$\Pi_1$$ consequences of any computably axiomatizable theory is computably enumerable.