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

Question

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<i\leq n} \bigvee t=x_i)$

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<n} \bigwedge x_i \in x_{i+1} \land x_n=x_0)$

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?

Answer 1

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.

(That said, things become tamer if we "internalize" the definition; see e.g. this old MSE question of mine. That question uses the framework of arithmetic rather than finite set theory, but that's a purely superficial difference.)