Language: first-order logic

Primitives: $=, S, \in $ (the first denotes identity, the second denotes “is a successor of”, and the third denotes membership relation).

Axioms: those of identity theory +

Existence: $\exists y, x (y \ S \ x)$

Define: $y \text{ is a successor } \iff \exists x (y \ S \ x)$

Succession: $\forall x,y (y \ S \ x \to \exists z (z \ S \ y))$

Uniqueness: $\forall a,b,c,d (a \ S \ b \wedge c \ S \ d \to[a=c \leftrightarrow b=d])$

Extensionality: $\forall x,y (\forall z (z \in x \leftrightarrow z \in y) \to x=y) $

Comprehension: If $\phi$ is a formula in which $x$ is not free, then all closures of $(\exists x \forall y (y \in x \leftrightarrow [y \text{ is a successor} \lor \forall z \in y ( z \text{ is a successor})] \wedge \phi))$ are axioms.

Well-foundedness: $\forall x [\exists m \in x \to \ \exists y (y \in x \wedge \forall z \in x (\neg [y \ S \ z])) ]$

This is, I think, equivalent to third-order arithmetic ($\text{Z}_3)$. Now if we weaken Comprehension to the following:

Comprehension': If $\phi$ is a formula in which $x$ is not free, then $ \forall w_1,..,w_n \exists x \forall y (y \in x \leftrightarrow [y=w_1 \lor ..\lor y=w_n] \wedge \phi)$ is an axiom.

Question: Could that weakened theory be stronger than bounded arithmetic? Or is it actually weaker than that?

  • The modified “Comperehension’” axiom is no comprehension axiom at all. It is simply equivalent to the existence of $n$-element sets: $\forall w_1,\dots,w_n\, \exists x\, \forall y (y \in x \leftrightarrow [y=w_1 \lor \dots\lor y=w_n])$ (for $n\ge0$, i.e., including the existence of an empty set). – Emil Jeřábek Jun 11 at 9:05
  • As far as I can see, this theory is locally interpretable in the theory of pairing, hence it is much weaker than bounded arithmetic. – Emil Jeřábek Jun 11 at 9:09
  • @EmilJeřábek what do you mean by "the theory of pairing". – Zuhair Al-Johar Jun 11 at 16:23
  • I meant one of the theories (mostly mutually interpretable) in Section 3.1 of . However, I’m no longer sure this is correct in the presence of extensionality. But anyway, the theory is weaker than bounded arithmetic. It is interpretable in, say, $Q$, and it is locally interpretable in Vaught’s set theory VS (axiomatized by the schema in my first comment) plus extensionality. This means it does not interpret $Q$, as I’m pretty sure $Q$ is not interpretable in (a finite fragment of) VS + extensionality. (Note that without extensionality, ... – Emil Jeřábek Jun 11 at 16:38
  • ... finite fragments of VS are interpretable in theories of pairing, and as such have decidable consistent extensions.) – Emil Jeřábek Jun 11 at 16:38
up vote 8 down vote accepted

$\let\itp\vartriangleright\def\mr{\mathrm}\DeclareMathOperator\dom{dom}\let\bez\smallsetminus\let\sset\subseteq$The weakened theory is much weaker than bounded arithmetic.

Let me denote the theory as $\mr{WT}$. Notice that the weakened comperehension schema is simply equivalent to the schema $$\tag{$V_n$}\forall w_1,\dots,w_n\,\exists x\,\forall y\,\Bigl(y\in x\leftrightarrow\bigvee_{i=1}^ny=w_i\Bigr)$$ for $n\in\omega$ (here $V_0$ asserts the existence of the empty set). Indeed, by excluded middle, $\{y:(y=w_1\lor\dots\lor y=w_n)\land\phi\}$ is one of the $2^n$ classes $\varnothing$, $\{w_1\}$, $\{w_2\}$, $\{w_1,w_2\}$, $\{w_3\}$, ..., $\{w_1,w_2,\dots,w_n\}$, each of which is a set by $V_n$.

Let $\mr{WT}_k$ denote the finite fragment of $\mr{WT}$ with axioms $V_n$ only for $n\le k$ (it is enough to take $V_0\land V_k$).

First, $\mr{WT}$ is at most as strong as bounded arithmetic. Note that all reasonable fragments of bounded arithmetic are mutually interpretable with Robinson’s arithmetic $Q$, hence I will use that as a gauge.

Theorem 1: $\mr{WT}$ is interpretable in $Q$ (which I will henceforth write as $Q\itp \mr{WT}$).

Proof sketch: Let us start by interpreting in $Q$ a decent fragment of arithmetic such as $S^1_2$. Inside this theory, we can define a well-behaved coding of sequences e.g. as follows: we first represent a sequence $\langle x_0,x_1,\dots,x_n\rangle$ by a string over the alphabet $\{0,1,2\}$ as $2_\smile x_0{}_\smile2_\smile x_1{}_\smile\dots_\smile x_n$ where each $x_i$ is written in binary (with no leading $0$s), and then we reinterpret the string as an integer written in ternary. Using this, we represent finite sets of numbers by strictly increasing sequences. We define $x\in y$ in accordance with this encoding scheme; if $y$ is not a valid representation of a set, we put $x\in y\iff x\ne y$ in order to maintain extensionality. We define $y\mathrel Sx$ as the usual successor relation $y=x+1$. Then it is routine to check that all axioms of $WT$ are valid under this interpretation. QED

We aim to show that $\mr{WT}$ is in fact strictly weaker than $Q$ in terms of strength, i.e., $\mr{WT}\not\itp Q$. To this end, we will relate $\mr{WT}$ with other theories.

Vaught’s set theory $\mr{VS}$ is a theory in the language of set theory $\langle\in\rangle$, axiomatized just by the schema $V_n$ for $n\in\omega$. Let $\mr{VSE}$ denote $\mr{VS}$ + the extensionality axiom. I will write $\mr{VS}_k$ and $\mr{VSE}_k$ for the finite fragments of $\mr{VS}$ and $\mr{VSE}$ (resp.) with $V_n$ axioms only for $n\le k$.

As mentioned in Visser [1,§3], $\mr{VS}$ interprets Robinson’s theory $R$, and as such it is essentially undecidable, however all finite fragments $\mr{VS}_k$ are interpretable in $\mr{VS}_2$, which is just a theory of unordered pairs (denoted $\mr{PAIR_{uno,ns}}$ in [1]); in particular, since there are decidable theories with pairing, it follows that each finite fragment of $\mr{VS}$ has a decidable extension. Consequently, $\mr{VS}\not\itp Q$, and more generally, $\mr{VS}$ does not interpret any finitely axiomatizable essentially undecidable theory.

Notice that $\mr{VSE}$ is a subtheory of $\mr{WT}$. We will show that these two theories are close enough to each other, and generalize to them the results above: finite fragments of $\mr{WT}$ are interpretable in finite fragments of $\mr{VSE}$, and both have decidable extensions.

Theorem 2: $\mr{WT}$ is locally interpretable in $\mr{VSE}$. Specifically, $\mr{VSE}_k\itp\mr{WT}_k$.

Proof: In $\mr{VSE}_k$, we can use the standard Kuratowski pairing function $\langle x,y\rangle=\{\{x\},\{x,y\}\}$ to define $(k+1)$-tuples as $\langle x_0,\dots,x_k\rangle=\langle x_0,\langle x_1,\langle\dots\rangle\rangle\rangle$. Let us put $$\begin{align} x\in^*y&\iff\begin{cases}x\in y&\text{if }|y|\le k,\\x\ne y&\text{otherwise,}\end{cases}\\ y\mathrel{S^*}x&\iff\exists\text{ pairwise distinct }x_0,\dots,x_k\:(x=\langle x_0,\dots,x_k\rangle\land y=\langle x_1,\dots,x_k,x_0\rangle). \end{align}$$ It is easy to see that under this interpretation, axioms of $\mr{VSE}_k$ are valid. Since $S^*$ consists of a nonempty collection of $(k+1)$-cycles, the axioms of Existence, Succession, and Uniqueness also hold. Finally, Well-foundedness also holds: any counterexample would have to include at least one full $S^*$-cycle, but none of the infinitely many elements that are not part of any cycle. However, all sets under the interpretation have either at most $k$ elements, or include all but one elements of the universe. QED

Note: it is perfectly possible that $\mr{WT}$ is in fact globally interpretable in $\mr{VSE}$, but I didn’t try.

Theorem 3: Each finite fragment $\mr{VSE}_k$ has a decidable consistent extension.

Corollary: Each finite fragment $\mr{WT}_k$ has a decidable consistent extension. Neither $\mr{VSE}$ nor $\mr{WT}$ interprets $Q$, or any finite essentially undecidable theory for that matter.

I will assume $k\ge2$. In order to prove Theorem 3, working in a usual set theory (e.g., ZFC), let $H_k$ denote the collection of all hereditarily $\le k$-element sets: the least family of sets such that $$x\sset H_k\land|x|\le k\implies x\in H_k.$$ Note that $H_k\sset V_\omega$. Clearly, $$(H_k,\in)\models\mr{VSE}_k,$$ thus Theorem 3 follows from

Theorem 4: $\mathrm{Th}(H_k,\in)$ is decidable.

Since any r.e. complete theory is decidable, it is enough to show that $\mathrm{Th}(H_k,\in)$ is recursively axiomatizable. In fact, I claim that it coincides with the theory $S_k$ axiomatized as follows:

  • $\mr{VSE}_k$ (i.e., extensionality, $V_0$ and $V_k$),

  • every set has at most $k$ elements,

  • there are no finite $\in$-cycles: i.e., the schema $$\forall x_0,\dots,x_n\,\neg(x_0\in x_1\in\dots\in x_n\in x_0)$$ for $n\in\omega$.

Obviously $H_k\models S_k$, it thus suffices to show that $S_k$ is complete, i.e., that any two models of $S_k$ are elementarily equivalent. We will prove more generally a characterization of elementary equivalence of finite tuples in models of $S_k$.

Let $A,B$ be models of $S_k$, and $\bar a\in A$, $\bar b\in B$ finite tuples of the same length. We write $A,\bar a\equiv B,\bar b$ if $\bar a$ and $\bar b$ are elementarily equivalent.

We define levels of the transitive closure of $\bar a$ (as subsets of $A$): $$\begin{align} t^A_0(\bar a)&=\{\bar a\},\\ t^A_{n+1}(\bar a)&=t^A_n(\bar a)\cup\bigcup_{u\in t^A_n(\bar a)}u^A,\\ t^A_\infty(\bar a)&=\bigcup_{n\in\omega}t^A_n(\bar a), \end{align}$$ where $u^A$ denotes the extension of $u\in A$ in $A$: $u^A=\{v\in A:v\in^A u\}$. Notice that each $t^A_n(\bar a)$ is finite: $|t^A_n(\bar a)|\le|\bar a|k^{n+1}$ or so. Also, each $t^A_n(\bar a)$ is definable (as a class) in $A$ from $\bar a$; the definition is uniform if $n$ and $|\bar a|$ are fixed.

Let us define $$\begin{align} A,\bar a\sim_n B,\bar b&\iff(t^A_n(\bar a),\in,\bar a)\simeq(t^B_n(\bar b),\in,\bar b),\\ A,\bar a\sim B,\bar b&\iff(t^A_\infty(\bar a),\in,\bar a)\simeq(t^B_\infty(\bar b),\in,\bar b). \end{align}$$ Recall that elementarily equivalent finite structures are isomorphic. Thus, the finiteness and definability of $t^A_n(\bar a)$ implies

Claim 5: $A,\bar a\equiv B,\bar b\implies A,\bar a\sim_n B,\bar b$ for all $n\in\omega$.

Notice that $\bar a\sim_m\bar b$ implies $\bar a\sim_n\bar b$ for $n\le m$, as an isomorphism $t^A_m(\bar a)\simeq t^B_m(\bar b)$ must map $t^A_n(\bar a)$ to $t^B_n(\bar b)$. Thus, if we look at the set of all isomorphisms $f\colon t^A_n(\bar a)\simeq t^B_n(\bar b)$ for all $n\in\omega$, it forms a tree ordered by inclusion, and finiteness of the structures implies that the tree is finitely branching. Thus, if it is infinite, it has an infinite branch by König’s lemma, which is then an isomorphism $t^A_\infty(\bar a)\simeq t^B_\infty(\bar b)$. Thus,

Claim 6: $A,\bar a\sim B,\bar b\iff\forall n\in\omega\:A,\bar a\sim_n B,\bar b$.

Corollary 7: $A,\bar a\equiv B,\bar b\implies A,\bar a\sim B,\bar b$.

We intend to prove the converse

Claim 8: $A,\bar a\sim B,\bar b\implies A,\bar a\equiv B,\bar b$.

This finishes the proofs of Theorems 3 and 4, as it implies $A,\varnothing\equiv B,\varnothing$ for any $A,B\models S_k$.

By definition, it’s clear that $A,\bar a\sim_0 B,\bar b$ implies $\bar a$ and $\bar b$ have the same atomic diagram. Thus, by standard model-theoretic machinery, Claim 8 follows from the following back-and-forth property:

Claim 9: If $A,\bar a\sim B,\bar b$ and $c\in A$, there exists an elementary extension $B'$ of $B$ and $d\in B'$ such that $A,\bar a,c\sim B',\bar b,d$.

Finally, the fact that $\sim_n$ can be characterized by satisfaction of suitable formulas implies that the condition on $d$ can be expressed as satisfiability of a certain type; thus, by the compactness theorem, it is enough to show

Claim 9’: If $A,\bar a\sim B,\bar b$, $c\in A$, and $n\in\omega$, there exists $d\in B$ such that $A,\bar a,c\sim_n B,\bar b,d$.

Proof: Let us fix an isomorphism $f\colon t^A_\infty(\bar a)\simeq t^B_\infty(\bar b)$. We need to extend $f$ to an isomorphism $g$ whose domain includes $t^A_n(c)$. For convenience, we will actually define $g$ as a map on $t^A_{n+1}(c)$, but it will not necessarily behave as an isomorphism on the extra points. Notice that $t^A_{n+1}(c)$ is a finite set, and $\in^A$ is acyclic, hence well founded, on it.

If there is $u\in t^A_{n+1}(c)\bez\dom(f)$ such that $u\sset\dom(f)$, we may extend $f$ right away so that $f(u)=\{f(x):x\in^A u\}^B$ (this exists in $B$, as it has at most $k$ elements). This maintains the salient property that $f$ is an isomorphism between two transitive closures of finite tuples. By repeating this construction as many times as necessary, we may assume without loss of generality that every $u\in t^A_{n+1}(c)\bez\dom(f)$ contains an element outside $\dom(f)$.

Now, let $\{u_i:i<m\}$ be an enumeration of $t^A_{n+1}(c)\bez(t^A_n(c)\cup\dom(f))$. We pick suitable $\{v_i:i<m\}\sset B$ (to be determined below), and define $g\supseteq f$, $g(u_i)=v_i$. We then extend the definition to all $u\in t^A_{n+1}(c)$ inductively by $g(u)=\{g(x):x\in^A u\}^B$.

We need to make sure $g$ is injective. Now, if $u,u'\in t^A_n(c)\cup\dom(f)$ are distinct, there is $x$ in (say) $u\bez u'$; we have $x\in\dom(g)$, and $g(x)\in g(u)$, hence $g(x)\in g(u')$, i.e., $g(x)=g(x')$ for some $x'\ne x$, $x'\in u'$. By continuing down, we eventually arrive at $v_i=g(u)$ for some $u\ne u_i$. If $u\in\dom(f)$, this means $v_i=f(u)$. Otherwise we have $u_j=x_1\in\dots\in x_l\in u$ for some $j<m$, $0\le l\le n+1$, $x_1,\dots,x_l\in t^A_n(c)$. Thus, $v_j\in g(x_2)\in\dots\in g(u)=v_i$. (This can only happen for $j\ne i$.)

It follows that $g$ is injective if we choose $v_i$ to satisfy two conditions: (1) $v_i\notin\mathrm{im}(f)$ for any $i<m$, and (2) for any $i\ne j<m$, $v_i\notin t^B_{n+1}(v_j)$. It is easy to see that such $\{v_i:i<m\}$ exist: for example, we may put $w=\langle b_0,b_1,\dots\rangle$, and $v_i=\{w\}^{(n+2)i+1}$, where $\{w\}^0=w$, $\{w\}^{r+1}=\{\{w\}^r\}$.

It is clear from the definition that once $g$ is injective, we have $x\in u\iff g(x)\in g(u)$ for any $x\in\dom(g)$, $u\in\dom(f)\cup t^A_n(c)$. In particular, putting $d=g(c)$, the restriction of $g$ to $t^A_n(\bar a,c)$ is an isomorphism $t^A_n(\bar a,c)\simeq t^B_n(\bar b,d)$. QED

Let me mention that Claim 8 also implies a quantifier elimination result for $S_k$. By compactness, for any formula $\phi(\bar x)$, there is $n$ such that the truth of $\phi$ is preserved by $\sim_n$. Thus, $\phi$ is equivalent to a disjunction of some of the (finitely many) formulas saying that $t_n(\bar x)$ looks such and such. This easily implies the following:

Corollary 10: In $S_k$, every formula is equivalent to a Boolean combination of bounded existential formulas. If we expand the language with a predicate symbol $x\sset\{x_1,\dots,x_k\}$, every formula is equivalent both to a bounded existential formula and to a universal existential formula.


[1] Albert Visser: Pairs, sets and sequences in first-order theories, Archive for Mathematical Logic 47 (2008), 299–326, doi: 10.1007/s00153-008-0087-1.

  • I believe Claim 9' strengthens to: $A,\bar a\sim_{r(n)}B,\bar b\implies \forall c\in a\,\exists d\in B\,A,\bar a,c\sim_n B,\bar b,d$, where $r(n)$ is $O(k^n)$. This also implies that $S_k$ is decidable in $n$-times-iterated-exponential time, matching the Ferrante–Rackoff lower bound for theories with pairing. – Emil Jeřábek Jun 13 at 15:41

Your Answer


By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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