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?

  • 2
    $\begingroup$ Any consistent theory that includes all the $V_n$ (including $n=0$) is undecidable. $\endgroup$ Commented May 4 at 11:56
  • 2
    $\begingroup$ 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. $\endgroup$ Commented May 4 at 12:21
  • 1
    $\begingroup$ 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. $\endgroup$ Commented May 4 at 12:48
  • 2
    $\begingroup$ $\cal S$ isn't complete, it doesn't prove or disprove "the largest natural number is even". $\endgroup$
    – paste bee
    Commented May 4 at 12:58
  • 3
    $\begingroup$ 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.) $\endgroup$ Commented May 4 at 12:58

1 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.)

  • $\begingroup$ what is co-c.e. $\endgroup$ Commented May 4 at 19:53
  • $\begingroup$ @ZuhairAl-Johar Complement of c.e. The only sets which are both c.e. and co-c.e. are the computable ones; nothing which is co-c.e. complete is also c.e. The complement of the halting problem is the standard example of a co-c.e.-complete set. $\endgroup$ Commented May 4 at 20:16
  • $\begingroup$ it appears to me that your bounded companion to PA theory has the exact motivation of this theory, though in another language. However, your theory is recursively axiomatized while this is not. We can internalize the definition if we can pass to finite Zermelo, I assume. How can we achieve a consistency criterion for the theory presented here? According to your theory it was equi-consistent with PA, so is this theory super-consistent to PA? Though not necessarily strictly so. Is its consistency incomparable to that of PA? $\endgroup$ Commented May 5 at 6:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.