A Complete Bounded Theory with Unbounded Types
February 25, 2026
Abstract
One measure of the complexity of a first-order theory, and similarly a type, is the complexity of the formulas required to axiomatize it. We say a theory is bounded if there is an axiomatization involving only \(\forall_n\)-formulas for some finite \(n\), and unbounded otherwise. One might expect bounded theories to have only bounded types. In fact, an analogue holds in infinitary logic, where the complexity of a Scott sentence roughly agrees with the complexity of the most complicated automorphism orbit. Our main result, however, shows this is not the case in the first-order setting: Namely, there can be a bounded theory, in fact \(\forall_1\)-axiomatizable, which has unbounded types.
1 Introduction↩︎
There have been many ways to measure the complexity of a theory. To begin with, finite axiomatizability has been studied since the very early days of logic: For example, the contrasting results that ZFC is not finitely axiomatizable [1] and that NBG (von Neumann–Bernays–Gödel set theory) is [2] remain one of the greatest distinctions between the two versions of set theory. One weakening of this notion is recursive axiomatizability, which is about the computational complexity of the set of formulas in the axiomatization and is featured in Gödel’s Incompleteness Theorems [3]. The notion of complexity we will use is another weakening of finite axiomatizability, looking at the syntactical complexity of individual formulas instead:
Definition 1. Say a theory is boundedly axiomatizable (or bounded for short) if it is \(\forall_n\)-axiomatizable (see 2) for some finite \(n\). Otherwise, it is not boundedly axiomatizable (or unbounded for short).
There has been recent interest in this notion. For example, Enayat and Visser [4] showed the incompleteness of any consistent bounded sequential theory in a finite language. In addition, it relates nicely with descriptive complexity: Andrews, Gonzalez, Lempp, Rossegger, and Zhu [5] showed that given a theory \(T\), its set of (countable) models (see 3) is \(\mathbf{\Pi}^0_n\) if and only if \(T\) is \(\forall_n\)-axiomatizable. Therefore, a theory is bounded if and only if its set of models is \(\mathbf{\Pi}^0_n\) for some finite \(n\). In addition, the authors showed in the same paper that if \(T\) is complete (hence also if \(T\) is a type), then it is unbounded if and only if its set of models is \(\mathbf{\Pi}^0_\omega\)-complete.
The main goal of this paper is to investigate the relationship between the boundedness of a theory and that of the types of the theory. Observe that unbounded theories always have unbounded types, since the theory is the type of the empty tuple. Therefore, one could conjecture that the converse holds as well, that bounded theories will only have bounded types. In a sense, this holds in infinitary logic: There, the analogue of a complete theory is a Scott sentence, which completely characterizes a countable structure; And the analogue of a (complete) type is an infinitary definition (without parameters) of an automorphism orbit. Montalbán [6] shows that for any structure \(\mathcal{A}\), having a \(\Pi^{\mathrm{in}}_{\alpha+1}\) Scott sentence is equivalent to all automorphism orbits being \(\Sigma^{\mathrm{in}}_{\alpha}\)-definable. Nevertheless, our main result shows that this is not the case in the first-order setting:
43 1. There is a complete theory \(T\) which is bounded (in fact \(\forall_1\)-axiomatizable) but has unbounded types. In addition, it is strictly superstable.
One major difficulty in proving this theorem is obtaining an unbounded type. Usually, such types show up either when the theory is already complicated to begin with (e.g. true arithmetic), or as Marker extensions which simultaneously increase the complexity of the theory and the types. In both cases, the underlying theories are unbounded, so we needed new machinery.
Notably, such a theory is far from being model complete, despite being \(\forall_2\)-axiomatizable: Any unbounded type must contain, for any \(n\), formulas not equivalent to any \(\forall_n\)-formula (otherwise there would be a \(\forall_n\)-axiomatization of the type). However, every formula in a model complete theory is equivalent to both a \(\forall_1\)-formula and an \(\exists_1\)-formula. So in a sense, our result witnesses strongly the failure of the converse of the well-known theorem that every model-complete theory is \(\forall_2\)-axiomatizable (see for example [7]).
The existence of such a theory also connects to the \(\omega\)-Vaught’s Conjecture, a structural strengthening of Vaught’s Conjecture, introduced by Gonzalez and Montalbán [8]. There, the authors introduce the notion of Vaught ordinal for a theory, which quantifies the level at which the “countable-or-continuum” behavior occurs in the models of the given theory. The \(\omega\)-Vaught’s Conjecture asserts the existence of such an ordinal below \(\omega\) for all (infinitary) theories, while the original Vaught’s Conjecture is equivalent to the existence of it below \(\omega_1\), which could then be called the \(\omega_1\)-Vaught’s Conjecture. In an upcoming paper [9], the author will prove a slight weakening of \(\omega\)-Vaught’s Conjecture for \(\omega\)-stable theories, namely the \((\omega\cdot2)\)-Vaught’s Conjecture. Due to the use of types there, if a bounded \(\omega\)-stable theory can have only bounded types, the result would then be improved to the full \(\omega\)-Vaught’s Conjecture for \(\omega\)-stable theories. In light of such discussions, our main result suggests that such an improvement may be too much to hope for.
The remainder of the paper is devoted to constructing such a theory \(T\). The main idea used is to introduce complexity in types by allowing for arbitrarily complicated trees in the theory, and then obfuscate it by adding all finite trees so that a sentence without parameters cannot have access to the complexity. A key motivation of the entire construction is the following theorem:
28 1. Finite-height trees (in the language \(\left\{\operatorname{Pred}\right\}\) with only the predecessor relation or, equivalently, in the language \(\left\{\operatorname{\le}\right\}\)) are pseudofinite.
2 Background↩︎
First, we make precise what is meant by \(\forall_n\)- and \(\exists_n\)-formulas.
Definition 2.
\(\forall_0=\exists_0\) is the set of quantifier-free formulas.
The set of \(\forall_{n+1}\)-formulas consists of all formulas of the form \(\forall x_1\ldots\forall x_n\;\varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)\) where \(\varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)\) is an \(\exists_n\)-formula.
The set of \(\exists_{n+1}\)-formulas consists of all formulas of the form \(\exists x_1\ldots\exists x_n\varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)\) where \(\varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)\) is a \(\forall_n\)-formula.
If a theory has an axiomatization consisting entirely of \(\forall_n\)-formulas, then we say it is \(\forall_n\)-axiomatizable.
Next, we adopt standard conventions in computable structure theory that the language \(\mathcal{L}\) is always countable, the countable structures always have domain \(\omega\), and that the countable models of a theory are viewed as a subset in Cantor space:
Notation 3. Fix a listing \(\left\{\varphi_i\mid i\in\omega\right\}\) of all atomic \((\mathcal{L}\cup\omega)\)-sentences, where elements of \(\omega\) are viewed as constants. We identify any \(\mathcal{L}\)-structure \(\mathcal{A}\) with domain \(\omega\) with its atomic diagram \(\mathcal{D}(\mathcal{A})\in2^\omega\), i.e. \(\mathcal{D}(\mathcal{A})(i)=1\) if \(\mathcal{A}\vDash\varphi_i\) and 0 otherwise.
The set \(\mathop{\mathrm{Mod}}(T)\) of an \(\mathcal{L}\)-theory \(T\) is the set of all countable models of \(T\).
Definition 4. By the descriptive complexity of a theory \(T\) we mean the descriptive complexity of \(\mathop{\mathrm{Mod}}(T)\subseteq 2^\omega\). For example, we say \(T\) is \(\mathbf{\Pi}^0_n\) if \(\mathop{\mathrm{Mod}}(T)\) is a \(\mathbf{\Pi}^0_n\) subset of \(2^\omega\). The same applies to a type (or a partial type) \(p(\overline{x})\) in language \(\mathcal{L}\), by viewing \(p(\overline{x})\) as the theory \(p(\overline{a})\) in language \(\mathcal{L}\cup\left\{\overline{a}\right\}\) where \(\overline{a}\) is a new set of constants (matching the length of \(\overline{x}\)).
3 Base Theory↩︎
We will start by defining a “base theory” \(T_0\), on top of which our final theory \(T\) will be defined. The models are basically trees, except that we name the levels explicitly and the predecessor relation on each level is considered a separate relation. Then we prove a few basic properties of \(T_0\).
Definition 5. Let \(\mathcal{L}_0=\left\{P_i\mid i\in\omega\right\}\cup\left\{<_i\mid i\in\omega\right\}\), where \(P_i\) are unary predicates and \(<_i\) are binary relations.
Notation 6. Let \(P\) denote \(\mathop{\mathrm{\bigvee\mkern-15mu\bigvee}}_{i\in\omega}P_i\), and \(<\) denote \(\mathop{\mathrm{\bigvee\mkern-15mu\bigvee}}_{i\in\omega}<_i\). These are not in general definable in our theories, but will be used as shorthands in our arguments.
Remark 7. The intended interpretations of the language and the base theory \(T_0\), to be defined below, are as follows: If an \(\mathcal{L}_0\)-structure \(\mathcal{M}\) is a model of \(T_0\), then \(<^{\mathcal{M}}\) defines a forest (disjoint union of trees) on domain \(P^{\mathcal{M}}\). \(P_i^{\mathcal{M}}\) are all the \(i\)-th level nodes, with the 0-th level being all the root nodes. \(<_i^{\mathcal{M}}\) is the restriction of \(<^{\mathcal{M}}\) to \(P_i^{\mathcal{M}}\times P_{i+1}^{\mathcal{M}}\).
Definition 8. Let \(T_0\) be the \(\mathcal{L}_0\)-theory that says (for every \(i,j\in\omega\) with \(i\ne j\)):
\(P_i\cap P_j=\varnothing\);
\(<_i\;\subseteq P_i\times P_{i+1}\);
(Existence of predecessors) \(\forall x\in P_{i+1}\,\exists y\in P_i\,(y<_ix)\);
(Uniqueness of predecessors) \(\forall x\forall x'\forall y\,((x<_iy\wedge x'<_iy)\to x=x')\);
Notice that \(\mathcal{L}_0\) is countable and relational, and \(T_0\) is \(\forall_2\)-axiomatizable.
Observation 9. \(T_0\) has \({\aleph_0}\) finite models (up to isomorphism). In fact, it has finitely many models of each finite cardinality \(n\).
Observation 10. Any (not necessarily finite) disjoint union of models of \(T_0\) remains a model of \(T_0\).
4 Constructing the Theory↩︎
Now that we have a base theory \(T_0\), we can start defining the theory \(T\) satisfying the conclusion of 43. The idea is as follows: We want a complete theory, so we will make models of \(T\) exhibit some “generic” behavior by requiring all finite models of \(T_0\) to be present (infinitely often). By adding new constants to represent those finite models, we preserve the low complexity of the theory itself, while also leaving room for types to behave wildly.
Construction: Since \(T_0\) has \({\aleph_0}\) finite models, list all of them as \(\left\{\mathcal{M}_i\right\}_{i<\omega}\). For each \(j<\omega\), let \(C_i^j\) be a set of new constants of size \(\left|M_i\right|\) (hence finite). Let \(C=\bigcup_{i,j\in\omega}C_i^j\).
Definition 11. Let \(\widetilde{\mathcal{L}}=\mathcal{L}_0\cup C\). Let \(T\) be the \(\widetilde{\mathcal{L}}\)-theory that says:
\(T_0\);
The constants in \(C\) are pairwise distinct;
The \(\mathcal{L}_0\)-substructure with domain \(C_i^j\) is isomorphic to \(\mathcal{M}_i\);
For each \(k\in\omega\): For all \(x,y\), if \(x\in C_i^j\) and \(x<_ky\vee y<_k x\), then \(y\in C_i^j\).
Notice that \(\widetilde{\mathcal{L}}\) is countable, \(T\) is \(\forall_2\)-axiomatizable, and \(T\) has only infinite models.
Next, we consider the “minimal” model of \(T\), one that has nothing other than the constants. (It will end up being the prime model.)
Proposition 12. There is a unique model \(\mathcal{C}\vDash T\) whose domain is equal to \(C^{\mathcal{C}}\), i.e. every element is (the interpretation of) a constant. In addition, \(\mathcal{C}\) embeds into every model of \(T\).
Proof. Straightforward from the axioms, where we completely specified the isomorphism types of the trees the constants are on. ◻
From now on, we refer to the substructure of all the constants of any \(\mathcal{M}\vDash T\) as the copy of \(\mathcal{C}\) inside \(\mathcal{M}\).
Definition 13. Let \(\mathcal{C}_i^j\) be the \(\mathcal{L}_0\)-substructure of \(\mathcal{C}\) with domain \(C_i^j\).
Notation 14. By \(\mathcal{M}^\omega\) we mean the countable disjoint union of the structure \(\mathcal{M}\) (in a relational language).
Observation 15. As \(\mathcal{L}_0\)-structures, \(\mathcal{C}\cong\bigsqcup_i\mathcal{M}_i^\omega.\)
Observation 16. For all \(\mathcal{M}\vDash T\), \(\mathcal{M}\cong\mathcal{C}\sqcup(\mathcal{M}\backslash\mathcal{C})\) over \(\mathcal{L}_0\) (where \(\mathcal{M}\backslash\mathcal{C}\) is the \(\mathcal{L}_0\)-substructure of \(\mathcal{M}\) with domain \(M\backslash C\)).
5 Completeness of the Theory↩︎
We move on to show the completeness of \(T\). The main tool we will use is the Ehrenfeucht-Fraïssé game \(EF^{\mathcal{L}}_k(\mathcal{M},\mathcal{N})\)1 (see [7]), which help characterize the theory (and types thereof) with invariants we introduce. The perfect-information game \(EF^{\mathcal{L}}_k(\mathcal{M}_0,\mathcal{M}_1)\) goes on for \(k\) steps, and in each step \(\forall\) chooses an element from \(M_0\) or \(M_1\), followed by \(\exists\) choosing an element from the other structure (trying to “match” \(\forall\)’s choice). In the end, collect all chosen elements \(\overline{m}_i\) from \(M_i\), and \(\exists\) wins the play if and only if there is an isomorphism \(f:\left\langle\overline{m}_0\right\rangle_{\mathcal{M}_0}\to\left\langle\overline{m}_1\right\rangle_{\mathcal{M}_1}\) identifying \(\forall\)’s choice at each step with \(\exists\)’s corresponding choice.
Notation 17. For two \(\mathcal{L}\)-structures \(\mathcal{M},\mathcal{N}\), write \(\mathcal{M}\equiv_{\mathcal{L},k}^{EF}\mathcal{N}\) if \(\exists\) has a winning strategy in \(EF^{\mathcal{L}}_k(\mathcal{M},\mathcal{N})\). And say \(\mathcal{M}\equiv^{EF}_{\mathcal{L}}\mathcal{N}\) if \(\mathcal{M}\equiv_{\mathcal{L}, k}^{EF}\mathcal{N}\) for every finite \(k\), i.e. \(\exists\) wins every \(EF^{\mathcal{L}}_k(\mathcal{M},\mathcal{N})\) of finite length.
The main reason we use \(EF^{\mathcal{L}}_k(\mathcal{M}_0,\mathcal{M}_1)\) is the theorem below, which follows from [7].
Theorem 18. If \(\mathcal{M}\equiv^{EF}_{\mathcal{L}}\mathcal{N}\) in a finite language \(\mathcal{L}\), then \(\mathcal{M}\equiv\mathcal{N}\) in the same language. As a result, if \(\mathcal{M}\equiv^{EF}_{\mathcal{L}'}\mathcal{N}\) in every finite \(\mathcal{L}'\subseteq\mathcal{L}\), then \(\mathcal{M}\equiv\mathcal{N}\) over \(\mathcal{L}\).
5.1 The Invariants↩︎
Going to finite sublanguages allows us to work with finite-height trees, where we can find invariants to use in the EF-games. We first define the finite sublanguage of \(\mathcal{L}_0\) that describes trees up to a finite height \(h\):
Definition 19. For \(0<h<\omega\), let \(\mathcal{L}_h\subseteq\mathcal{L}_0\) be the finite sublanguage consisting of \(P_i\) for \(i\le h\), and \(<_i\) for \(i<h\).
Notice that \(\mathcal{L}_0=\bigcup_{0<h<\omega}\mathcal{L}_h\), and \(\mathcal{L}_h\)-reducts of models of \(T_0\) are forests of height at most \(h\). In what follows we will be frequently using tree terminologies on models \(\mathcal{M}\vDash T_0\) (or their reducts), where the tree structure is understood to be \((P^{\mathcal{M}},<^{\mathcal{M}})\).
Definition 20. By an \(h\)-forest we mean an \(\mathcal{L}_h\)-reduct of a model of \(T_0\). We may also say \(h\)-tree when it has a single root. Its domain (as a forest) \(P_{\le h}\) is defined as \(\bigcup_{i\le h}P_i.\)
Definition 21. In a forest, the level of \(x\in P\) is the the unique \(l\) such that \(P_l(x)\).
To show the completeness of \(T\), one attempt is to show any \(\mathcal{M}\vDash T\) is elementarily equivalent to \(\mathcal{C}\) in any finite sublanguage of the form \(\mathcal{L}'=\mathcal{L}_h\cup C_0\) where \(C_0\subseteq C\) is finite. The major problem is that \(\mathcal{C}\) is a forest of finite trees while \(\mathcal{M}\) may contain infinite trees. But when viewed from \(\mathcal{L}'\), every tree will have finite height, and in this case we will show that infinite trees can be sufficiently well approximated by finite ones. For such purposes we introduce the following invariant, which summarizes the information of the tree above a node inductively using that of its children.
Fix \(0<h<\omega, k\in\omega.\)
Definition 22. The \(k\)-bounded coloring of an \(h\)-forest \(\mathcal{M}\) is the function \(\Lambda\) defined on \(M\) as follows: given \(x\in M\), \(\Lambda(x)=\left\langle\Lambda_l(x),\Lambda_{\sigma}(x)\right\rangle\) where
\(\Lambda_l(x)\) is the level of \(x\) (or \(-1\) if not in \(P_{\le h}\)).
\(\Lambda_{\sigma}(x)\) is a set of pairs \(\left\langle\lambda_i,n_i\right\rangle\). It is defined inductively, from the leaves down to the root, as follows:
Let \(\Lambda_{\sigma}(x)\) be the set of all pairs \(\left\langle\lambda,n\right\rangle\), where \(\lambda\) is the color of a successor \(y\) of \(x\) (i.e. \(\lambda=\Lambda(y)\)), and \(n=\min(k,m)\) where \(m\) is the number of successors of \(x\) with color \(\lambda\).
In particular, \(x\in P_{\le h}\) is a leaf if and only if \(\Lambda_{\sigma}(x)=\varnothing\).
Intuitively, \(\varnothing\) is the color of leaves, each \(\lambda_i\) is a (previously defined) color, and \(n_i\) is the number of successors of \(x\) with color \(\lambda_i\) (but capped at \(k\)).
Remark 23. By induction (noting that we are working with trees of a fixed finite height \(h\)), it’s clear that there are only finitely many possible colors, and thus the range of \(\Lambda\) (for all \(\mathcal{M}\)) lives in a finite set (depending only on \(h\) and \(k\)).
Definition 24. For fixed \(h,k\), a \((k,h)\)-color will mean one (among finitely many) that could be the color of some element in the \(k\)-bounded coloring of some \(h\)-forest.
For any element \(x\) (in a model of \(T\)), its \((k,h)\)-color is \(\Lambda(x)\) where \(\Lambda\) is the \(k\)-bounded coloring of its ambient model as an \(h\)-forest.
When \(k,h\) are understood from context, we will say color for \((k,h)\)-color.
Proposition 25. For every \((k,h)\)-color \(\lambda\), there is a finite \(h\)-tree \(\mathcal{Y}_\lambda\) whose root has color \(\lambda\).
Proof. From the definition of our coloring, we can build inductively a \((\le k)\)-branching \(h\)-tree \(\mathcal{Y}_\lambda\) with root color \(\lambda\). But such trees must be finite. ◻
5.2 Winning Strategies for \(\exists\)↩︎
Now we show the colors describe an \(h\)-forest \(\mathcal{M}\) sufficiently well, in the following sense.
Theorem 26. Fix \(0<h<\omega,n\in\omega\). Let \(k=n(h+1)\). Suppose that:
\(\mathcal{M}_0,\mathcal{M}_1\) are \(h\)-forests such that for each \((k,h)\) color \(c\), \(\mathcal{M}_0\) and \(\mathcal{M}_1\) have the same number of roots with color \(c\).
\(\overline{a}_0\in\mathcal{M}_0, \overline{a}_1\in\mathcal{M}_1\) are tuples of the same length and are closed under predecessor;
The map \(\overline{a}_0\mapsto\overline{a}_1\) is a \((k,h)\)-color-preserving isomorphism.
Then \((\mathcal{M}_0,\overline{a}_0)\equiv^{EF}_{\mathcal{L}_h,n}(\mathcal{M}_1,\overline{a}_1)\).
Proof. First, we modify the EF-game by extending the length from \(n\) to \(k=n(h+1)\), but requiring that \(\forall\) cannot choose an element unless its predecessor has been chosen before in the game (or the element has no predecessor). Winning this prolonged version of the game suffices because: whenever \(\forall\) plays an element \(x\) in the original length-\(n\) game, \(\exists\) can act as if \(\forall\) played all of the (at most \(h+1\)) ancestors of \(x\) in order (starting from the root) in the prolonged game, and winning the latter game clearly tells \(\exists\) how to win the former. Since each step in the original game takes up at most \(h+1\) steps in the prolonged game and \(k=n(h+1)\), we have ensured that \(\exists\) can win before using up all moves in the prolonged version.
Now we work in the prolonged game with length \(k\), and suppose \(\forall\) can only choose an element after its predecessor has shown up. This means that at every step, \(\forall\) only makes one of the following choices:
A previously chosen element (by \(\forall\) or \(\exists\));
An element of \(\overline{a}_0\cup\overline{a}_1\);
An element outside of \(P_{\le h}\) (from either structure);
An element of \(P_0\) (i.e. the root of a tree) (from either structure);
Or, an successor of a previously chosen element.
Correspondingly, we describe a winning strategy for \(\exists\) (which builds a \((k,h)\)-color-preserving partial isomorphism; since the language is relational, the substructure generated by any tuple is just itself, so the partial isomorphism is totally determined by \(\exists\)’s choices). At the same time, we verify inductively that at each step: (1) the element \(\exists\) chose has the same color as the one \(\forall\) chose at the same step (when this is not obvious); and (2) \(\exists\) successfully builds a partial isomorphism up to that step. Note that our assumption of \(\overline{a}_0\mapsto\overline{a}_1\) being a \((k,h)\)-color preserving isomorphism covers the base case.
If \(\forall\) chooses a previously chosen element (or one in \(\overline{a}_0\cup\overline{a}_1\)), then \(\exists\) makes the same choice as it did earlier.
If \(\forall\) chooses an element of \(\overline{a}_0\cup\overline{a}_1\), then \(\exists\) chooses the corresponding element according to the (by our third assumption) \((k,h)\)-color-preserving isomorphism \(\overline{a}_0\mapsto\overline{a}_1\).
If \(\forall\) chooses an element outside \(P_{\le h}\), then \(\exists\) chooses an element outside \(P_{\le h}\) in the other structure.
If \(\forall\) chooses a new root node \(x\), then \(\exists\) chooses a root \(y\) in the other structure with the same \((k,h)\)-color. This is always possible by our first assumption.
If \(\forall\) chooses a new successor \(x\) of a previously chosen element \(x_0\) (that has not been chosen previously): suppose \(\exists\) responded to \(x_0\) with \(y_0\) previously. By induction hypothesis, \(x_0\) and \(y_0\) have the same color. Now choose \(y\) to be a new successor of \(y_0\) having the same color \(c\) as \(x\) that have not been chosen before. The existence of such an element is verified as follows: Say \(x,x_0\in\mathcal{M}_i\) with \(i<2\). (1) If \(x_0\) has at least \(k\) successors of color \(c\) in \(\mathcal{M}_i\): then \(y_0\) has at least \(k\) successors of color \(c\) in \(\mathcal{M}_{1-i}\) (by definition of the color on \(x_0,y_0\) and that they have the same color). But at this stage we have chosen fewer than \(k\) elements in each structure as the game has length \(k\), so there is a new one available to \(\exists\). (2) If \(x_0\) has at most \(k\) successors of color \(c\) in \(\mathcal{M}_i\): then similarly \(y_0\) has the same number of successors of color \(c\) in \(\mathcal{M}_{1-i}\). By induction hypothesis, we built a partial \((k,h)\)-color-preserving isomorphism previously, so the number of successors with color \(c\) that have been chosen in both structures are the same. Since \(\forall\) can find a new element on one side, \(\exists\) must be able to do the same on the other side, so we are done.
◻
5.3 Finite-height Trees↩︎
A first consequence of 26 is that for every \(h\)-forest \(\mathcal{M}\) and every \(n\), there exists a \(k\) with \(\mathcal{M}\equiv_{\mathcal{L}_h,n}^{EF}\widetilde{\mathcal{M}}_{k,h}\). This allows us to show that finite-height trees are pseudofinite.
Proposition 27. Fix \(0<h<\omega,n\in\omega\) and let \(k=n(h+1)\). For every \(h\)-tree \(\mathcal{M}\), we have \(\mathcal{M}\equiv_{\mathcal{L}_h,n}^{EF}{\mathcal{Y}}_{\lambda}\) (from 25) where \(\lambda\) is the \((k,h)\)-color of the root of \(\mathcal{M}\).
Proof. Apply 26 to \(\mathcal{M}\) and \({\mathcal{Y}}_{\lambda}\) (with \(a_0=a_1=\varnothing\)), noting that the corresponding roots have the same color. ◻
Theorem 28. Finite-height trees (in the language \(\left\{\operatorname{Pred}\right\}\) with only the predecessor relation or, equivalently, in the language \(\left\{\operatorname{\le}\right\}\)) are pseudofinite.
Proof. First we work in the language \(\left\{\operatorname{Pred}\right\}\). Fix a tree \(\mathcal{M}\) with height \(h\) and a formula \(\varphi\) with \(\mathcal{M}\vDash\varphi\). Then \(\mathcal{M}\) is definitionally equivalent to an \(h\)-tree \(\mathcal{M}'\) (with all elements in \(P_{\le h}\)), by interpreting \(\operatorname{Pred}\) as \(\cup_{i<h}<_i\) in one direction; and interpreting \(P_i\) as the elements on the \(i\)-th level (expressible with \(\operatorname{Pred}\)), \(<_i\) as \(\operatorname{Pred}\restriction(P_i\times P_{i+1})\) in the other direction. Let \(\varphi'\) be the corresponding formula of \(\varphi\) under this interpretation, so that \(\mathcal{M}'\vDash\varphi'\). By writing \(\varphi'\) using game-normal formulas (see [7]), we see that there exists an \(n\) such that for all \(\mathcal{L}_h\) structures \(\mathcal{N}'\), \(\mathcal{M}'\equiv^{EF}_n\mathcal{N}'\) implies \(\mathcal{N}'\vDash\varphi'\). By 27, we can take \(\mathcal{N}'=\mathcal{Y}_{\lambda}\), with \(\lambda\) being the \((n(h+1),h)\)-color of the root of \(\mathcal{M}\), to guarantee \(\mathcal{N}'\vDash\varphi'\). Let \(\mathcal{N}\) be the tree obtained from \(\mathcal{N}'\) using the same definitional equivalence, so \(\mathcal{N}\vDash\varphi\). Now by 25, \(\mathcal{N}'\) is finite, so \(\mathcal{N}\) is finite as well.
The claim for the language \(\left\{\le\right\}\) follows from that for \(\left\{\operatorname{Pred}\right\}\), since we again have a definitional equivalence given a tree of fixed finite height \(n\). ◻
5.4 Completeness↩︎
The next application of 26 is to show the completeness of \(T\).
Corollary 29. Fix \(0<h<\omega,n\in\omega\). Let \(k=n(h+1)\). For \(\widetilde{\mathcal{L}}\)-structures \(\mathcal{M}, \mathcal{N}\) both satisfying \(T\), suppose \(\overline{a}\in\mathcal{M}, \overline{b}\in\mathcal{N}\) are tuples of the same length closed under predecessor with \(\overline{a}\mapsto\overline{b}\) being a \((k,h)\)-color-preserving isomorphism. Then \((\mathcal{M},\overline{a})\equiv^{EF}_{\mathcal{L}_h,n}(\mathcal{N},\overline{b})\).
Proof. Apply 26 to \((\mathcal{M},\overline{a})\) and \((\mathcal{N},\overline{b})\), The only assumption not given directly is that \(\mathcal{M}, \mathcal{N}\) have the same number of roots with a given color \(\lambda\), which holds because: Recall from 25 that the color of any root in any \(h\)-forest is a color of a root of a finite \(h\)-forest. But by our definition of \(T\) (which include all the constants in \(C\)), all such colors appear at least (thus exactly) \({\aleph_0}\) times in both \(\mathcal{M}\) and \(\mathcal{N}\), since both satisfy \(T\). So \(\mathcal{M},\mathcal{N}\) have the same number of roots with any given color \(\lambda\). ◻
Theorem 30. \(T\) is complete.
Proof. It amounts to proving all \(\mathcal{M},\mathcal{N}\vDash T\) are elementarily equivalent. In turn, by 18 it suffices to show \(\mathcal{M}\equiv_{\mathcal{L}',n}^{EF}\mathcal{N}\) for every finite sublanguage \(\mathcal{L}'\) of \(\widetilde{\mathcal{L}}\). We may assume \(\mathcal{L}'=\mathcal{L}_h\cup \overline{c}\) for some \(0<h<\omega\) and some finite \(\overline{c}\subseteq C\) closed under predecessor. Now the requirement becomes: \[(\mathcal{M},\overline{c}^{\mathcal{M}})\equiv_{\mathcal{L}_h,n}^{EF}(\mathcal{N},\overline{c}^{\mathcal{N}}).\]
To this end, we apply 29 to \((\mathcal{M},\overline{c}^{\mathcal{M}})\) and \((\mathcal{N},\overline{c}^{\mathcal{N}})\). We check the assumptions: \(\overline{c}^{\mathcal{M}}, \overline{c}^{\mathcal{N}}\) clearly have the same length, and are closed under predecessor by definition. In addition, the color and isomorphism type of \(\overline{c}\) (in either structure) are fully specified by the theory \(T\), so the corresponding map \(\overline{c}^{\mathcal{M}}\mapsto\overline{c}^{\mathcal{N}}\) is a \((k,h)\)-color-preserving isomorphism. Hence we are done. ◻
6 Analysis of Types↩︎
Before we discuss the existence of complicated types, we need to understand (and in particular count) types over \(T\). Fortunately, this follows from our previous analyses: the tree colorings (as in 22) play a role similar to an elimination set for the theory.
Proposition 31. For any \(0<h<\omega, k\in\omega\) and any \((k,h)\)-color \(c\), there is a first-order formula in free variable \(x\) expressing the fact that the \((k,h)\)-color of \(x\) is \(c\).
Proof. By inducting on the definition of the coloring. ◻
The description of types below follows directly from 29.
Proposition 32. Any \(n\)-type \(p(\overline{x})\) over \(T\) is completely determined by: (1) Whether or not each \(x_i\) is a constant; (2) For each \(i\), the unique \(n\) such that \(x_i\in P_n\) (or the nonexistence thereof); (3) For each \(k,h\), the \((k,h)\)-color of each \(x_i\) and ancestors; (4) For any \(x_i,x_j\in\overline{x}\), the unique \((u,v)\) such that the \(u\)-th predecessor of \(x_i\) is equal to the \(v\)-th predecessor of \(x_j\) (or the nonexistence of \((u,v)\), i.e. they are on different trees).
This characterization extends to types over a set \(S\): only item (4) needs to take \(S\) into additional consideration.
Corollary 33. \(T\) is strictly superstable.
Proof. By our characterization of types above, there can be at most \(\kappa+2^{\aleph_0}\) \(1\)-types \(p(x)\) over a set \(S\) of cardinality \(\kappa\), so \(T\) is superstable. (Note that item (4) is determined by the highest-level element in \(S\) that shares the same tree with \(x\).) On the other hand, for each \(X\in 2^\omega\), consider the partial type \(p_X(x)\) that says \(x\) is the root of a tree which has a leaf on level \(n\) if and only if \(n\in X\). Clearly these are continuum many partial 1-types over \(\varnothing\) and are pairwise incompatible, so \(T\) is not \(\omega\)-stable. ◻
7 Complicated Types↩︎
Now we start working on complicated (complete) types. The idea is that the theory allows us to put complicated trees in the model, and having access to the root reveals the complexity. To do this more formally, we define the following stronger notion of continuous reducibility.
Definition 34. For two structures \(\mathcal{M}\not\cong\mathcal{N}\) (in the same language), say \((\mathbf{\Sigma}^0_k,\mathbf{\Pi}^0_k)\le_c^*(\mathcal{M},\mathcal{N})\) if for any \(X\) and any \(\Sigma^0_k(X)\) set \(A\subseteq 2^\omega\), there exists an \(X\)-computable reduction \(f:2^\omega \to 2^\omega\) such that \(x\in A\iff f(x)\cong\mathcal{M}\) and \(x\notin A\iff f(x)\cong\mathcal{N}\), and the \(X\)-code for \(f\) is uniformly computable from a \(\Sigma^0_k(X)\)-code for \(A\).
Remark 35. If \((\mathbf{\Sigma}^0_k,\mathbf{\Pi}^0_k)\le_c^*(\mathcal{M},\mathcal{N})\), then \(\left\{X\in 2^\omega\mid X\cong\mathcal{M}\right\}\) is \(\mathbf{\Sigma}^0_k\)-hard and \(\left\{X\in 2^\omega\mid X\cong\mathcal{N}\right\}\) is \(\mathbf{\Pi}^0_k\)-hard.
To build an unbounded type, we first construct, for every \(k\), a tree \(\mathcal{M}_k\) whose root satisfies a \(\mathbf{\Pi}^0_k\)-hard 1-type. Then we combine all of them into a single tree, starting with a tree with countably many nodes \(G_k\) definable over the root and putting \(\mathcal{M}_k\) above each \(G_k\). To make sure \(\Pi^0_k\)-hardness transfers from \(\mathcal{M}_k\) to the combined tree, we need formulas whose truth values depend only on trees above the free variables. This leads us to the “local formulas” defined below:
Definition 36. The collection of local formulas is the smallest collection of \(\mathcal{L}_0\)-formulas that:
contains all atomic and negated atomic formulas; and
is closed under local quantifications, namely quantifiers of the form \({\forall y>_kx}\), \({\exists y>_kx}\), for any variable \(x\) and \(k\in\omega\).
Remark 37. As is common practice, we will also say a formula is local if it is logically equivalent to a local formula. Under this convention, the set of local formulas is closed under negation, conjunction, disjunction, and local quantification.
When we combine the \(\mathbf{\Pi}^0_k\)-hard trees into a single tree, each constituent’s root will never be on level 0. So we need the following definition of “upshift” for adapting local formulas to when the root is not necessarily on level 0.
Definition 38.
If \(\varphi\) is a local formula and \(k\in\omega\), then let \(\varphi^{+k}\), the \(k\)-th upshift of \(\varphi\), be the formula obtained from \(\varphi\) by replacing every \(P_i\) by \(P_{i+k}\), and \(<_i\) by \(<_{i+k}\).
Clearly, any upshift of a local formula remains local.
If \(\mathcal{M}\vDash T_0\) with \(m\in P^{\mathcal{M}}\), the tree above \(m\), denoted as \(\mathcal{M}_{\ge m}\), is the \(\mathcal{L}_0\)-structure obtained by setting \(m\) as the only root node and copying everything above \(m\). More formally: say \(m\in P_k^{\mathcal{M}}\).
\(M_{\ge m}=\left\{x\in M\mid x>^{\mathcal{M}}m\vee x=m\right\}\).
For \(x\in M_{\ge m}, x\in P_i^{\mathcal{M}_{\ge m}}\iff x\in P_{i+k}^{\mathcal{M}}\).
For \(x,y\in M_{\ge m}, x<^{\mathcal{M}_{\ge m}}_iy\iff x<_{i+k}^{\mathcal{M}}y\).
It follows that \(\mathcal{M}_{\ge m}\vDash T_0\) with its isomorphism type depending only on that of \((\mathcal{M},m)\).
Now we show that truth of local formulas is preserved “locally,” i.e. is determined by the tree above the free variables. The proposition generalizes to more than one variable, but the single-variable version suffices for us.
Proposition 39. Suppose \(\varphi(x)\) is a local formula in one variable \(x\), \(\mathcal{M}_i\) are \(\mathcal{L}_0\)-structures, \(m_i\in P_{k_i}^{\mathcal{M}_i}\) for \(k_i\in\omega, i<2\). Suppose in addition that \(\mathcal{M}_{0,\ge m_0}\cong \mathcal{M}_{1,\ge m_1}\), i.e. the trees above the two chosen elements are isomorphic. Then \[\mathcal{M}_0\vDash\varphi^{+k_0}(m_0)\iff\mathcal{M}_1\vDash\varphi^{+k_1}(m_1).\]
Proof. Note that the isomorphism \(\mathcal{M}_{0,\ge m_0}\cong \mathcal{M}_{1,\ge m_1}\) has to send \(m_0\) to \(m_1\) since it preserves the unique root. Hence, it suffices to show that (for \(i<2\)) \[\mathcal{M}_i\vDash\varphi^{+k_i}(m_i)\iff\mathcal{M}_{i,\ge m_i}\vDash\varphi(m_i).\] This follows by first relativizing (in the sense of Theorem 5.1.1 of [7]) \(\varphi^{+k_i}\) to the tree above \(m_i\) in \(\mathcal{M}_i\), noticing that \(\varphi^{+k_i}\) is invariant under this relativization (by locality); and then chasing through the definition of the tree above an element. ◻
Now we begin constructing the \(\mathbf{\Pi}^0_k\)-hard trees.
Proposition 40. Uniformly in \(k\in\omega, k\ge 1\), we can build computable trees \(\mathcal{M}_k, \mathcal{N}_k\vDash T_0\) and a local formula \(\varphi_k(x)\) such that \((\mathbf{\Sigma}^0_k,\mathbf{\Pi}^0_k)\le_c^*(\mathcal{M}_k,\mathcal{N}_k)\), and \(\mathcal{M}_k\vDash\varphi_k(*), \mathcal{N}_k\vDash\neg\varphi_k(*)\) where \(*\) is the unique (definable) root node (so \(\mathcal{M}_k\not\equiv\mathcal{N}_k\) witnessed by \(\varphi_k(*)\), in particular \(\mathcal{M}_k\not\cong\mathcal{N}_k\)).
Proof. We take \(\mathcal{M}_k, \mathcal{N}_k\) to be the back-and-forth trees \(\mathcal{E}_k, \mathcal{A}_k\) from [10], respectively, except that to work in \(\widetilde{\mathcal{L}}\) we must use \(<_n\) to replace the directed edges for appropriate values of \(n\). This is possible with all uniformity, since we know the level of each node during the construction: The idea there is to start with a single node as \(\mathcal{A}_1\) and a single root with infinitely leaf successors as \(\mathcal{E}_1\); Then inductively, let \(\mathcal{A}_{k+1}\) be a single root with infinitely many \(\mathcal{E}_k\)’s above, and \(\mathcal{E}_{k+1}\) be a single root with infinitely many \(\mathcal{A}_k\)’s and \(\mathcal{E}_k\)’s above.
That \((\mathbf{\Sigma}^0_k,\mathbf{\Pi}^0_k)\le_c^*(\mathcal{M}_k,\mathcal{N}_k)\) uniformly in \(k\) follows by relativizing [10] to any oracle \(X\). Again, the idea there is to build the reductions inductively.
The formulas \(\varphi_k(*)\) can be found by adapting [11] to our language \(\widetilde{\mathcal{L}}\), noting the resulting formulas can be made local since the quantifiers appearing in the proof there can be replaced by local ones (uniformly computably). Essentially, these formulas are obtained by writing down the (inductive) definitions of \(\mathcal{E}_k\) and \(\mathcal{A}_k\). ◻
Now we are finally ready to build an unbounded type.
Theorem 41. There is a complete type \(p(x)\in S_1(T)\) which is \(\mathbf{\Pi}^0_\omega\)-hard. In particular, it is not \(\forall_n\)-axiomatizable for any finite \(n\).
Proof. We combine the trees \(\mathcal{M}_i\) from 40 into a single tree with root \(x\), in a way that the root of each \(\mathcal{M}_i\) is definable from \(x\), and then take the complete type of \(x\). (We will see at the end why this suffices.)
The above can be done, for example, by the following: Let \(\mathcal{N}\vDash T_0\) be the tree defined by: (See Figure 1.)
There is a unique root, denoted by \(F_0\).
(Having defined all of \(F_j\) for \(j<i\):) There is a unique \(y\in P_{2i}\) which is a leaf and whose only common ancestor with \(F_j\) is \(F_0\), for all \(j<i\). (Call this \(y\) \(F_i\).)
For \(i>0\), there is a unique \(z\in P_{2i}\) that is not \(F_i\) but has the same predecessor as \(F_i\). (Call this \(z\) \(G_i\).)
The tree above \(G_i\) is \(\mathcal{M}_i\).
Let \(\mathcal{M}\) be the \(\widetilde{\mathcal{L}}\)-structure obtained from \(\mathcal{C}\sqcup\mathcal{N}\) (i.e. the \(\mathcal{L}_0\)-structure is \(\mathcal{C}\sqcup\mathcal{N}\) and the constants are from \(\mathcal{C}\)). Clearly, \(\mathcal{M}\vDash T\). Let \(p(x)\) be the 1-type of the root node of the \(\mathcal{N}\)-part in \(\mathcal{M}\).
We claim \(p(x)\) is \(\Pi^0_{\omega}\)-hard: Take any \(\mathbf{\Pi}^0_\omega\) set \(S\), which we may assume is \(\Pi^0_\omega(X)\) for some \(X\). Write it as \(\bigcap_{0<i<\omega}S_i\) where \(S_i\) is uniformly \(\Sigma^0_i(X)\). By 40, we can uniformly find \(X\)-computable functionals \(f_i\) witnessing \((S_i,\overline{S}_i)\le_c(\mathcal{M}_i,\mathcal{N}_i)\). Now our \(X\)-computable reduction \(f\) from \(S\) to \(\mathop{\mathrm{Mod}}(p(a))\) (where \(a\) is a new constant) does the following: Given input \(y\), \(f(y)\) is the following model:
Add a copy of \(\mathcal{C}\) (which can be done computably).
Disjoint from \(\mathcal{C}\), build a new tree with root \(a\) by following the instructions above for building \(\mathcal{N}\), except that build the tree above \(G_i\) using \(f_i(y)\) (instead of \(\mathcal{M}_i\)).
Clearly, if \(y\in S\) (i.e. \(y\) is in every \(S_i\)) then \(f(y)\cong\mathcal{N}\) (because each \(f_i(y)\) is actually \(\mathcal{M}_i\)). Otherwise, there is some \(i\) such that \(f_i(y)\) is \(\mathcal{N}_i\), in particular satisfies \(\neg\varphi_i(*)\). Using the definability of \(G_i\) from \(x\) (in the definition of \(\mathcal{N}\)), we see that \(f(y)\vDash\neg\varphi_i^{+2i}(G_i(a))\), while \(\varphi_i^{+2i}(G_i(x))\in p(x)\) (where \(G_i(x)\) is a formula defining \(G_i\) from \(x\)). Hence \(f(y)\not\vDash p(a)\), so we are done. ◻
Remark 42. \(p(x)\) is also unbounded over \(T\) since \(T\) is itself bounded.
Combining everything together, we finally obtain our main result.
Theorem 43. There is a complete theory \(T\) which is bounded but has unbounded types. In addition, it is strictly superstable.
Proof. The theory \(T\) we constructed has a \(\forall_2\) axiomatization by definition: see 11 and the comments immediately after. It has an unbounded type by 41, is complete by 30, and is strictly superstable by 33. ◻
Corollary 44. The theory above can be taken to be satisfy either of the following:
\(\forall_1\)-axiomatizable.
\(\forall_2\)-axiomatizable in a relational language.
Proof. For a \(\forall_1\) axiomatization, we can use function symbols \(\operatorname{Pred}_n\) for predecessors to replace \(<_n\), reformulating the theory correspondingly.
For a relational \(\forall_2\) axiomatization, we can similarly use unary predicates to replace all the constants.
In both cases we get theories bi-interpretable with the one given in 11, so boundedness and stability properties are preserved. ◻
8 Open Questions↩︎
There are several possible ways to strengthen the main result. First, one can examine the stability hierarchy. As mentioned in the introduction section, the existence of a bounded theory with unbounded types prevents one from showing the \(\omega\)-Vaught’s Conjecture for \(\omega\)-stable theories. However, if such behaviors cannot occur in \(\omega\)-stable theories, then the proof would go through.
Question 45. Is there a complete bounded \(\omega\)-stable theory with unbounded types?
Second, the model we construct has continuum many countable models (since there are continuum many types over \(\varnothing\)). In view of problems related to the Vaught’s Conjecture, we would like to know if such behaviors occur when there are countably many countable models as well.
Question 46. Is there a complete bounded theory with unbounded types having only countably many countable models?
In addition, while the theory we have is \(\forall_1\)-axiomatizable, to make it relational we would end up with a \(\forall_2\)-axiomatization, which we do not know is optimal or not for a relational theory. We can rule out \(\forall_1\) or \(\exists_1\) theories: All complete relational \(\forall_1\) theories have the empty set as a model (thus trivial); All complete relational \(\exists_1\) theories are too simple as well:
Proposition 47. Any complete relational \(\exists_1\) theory \(T\) can have no relations of arity at least 2 in the language. In particular, they cannot have unbounded types.
Proof. If \(R\) is a relation symbol with at least 2 variables, consider the formula \(\Phi=\exists x \forall y\;R(x,y,\ldots,y)\). Any \(\mathcal{M}\vDash T\) embeds in a superstructure satisfying \(\Phi\) and another satisfying \(\neg\Phi\), but both have the same complete theory \(T\) (since \(T\) is \(\exists_1\)), a contradiction.
Hence the language \(\mathcal{L}\) of such \(T\) has only unary relations, so \(T\) must be the theory of a structure where any finite combination of the predicates has infinitely many realizations (because any \(\mathcal{L}\)-structure embeds into such a structure). Such theories have QE, thus admit no unbounded types. ◻
But for \(\exists_2\), things remain unclear.
Question 48. Is there a \(\exists_2\)-axiomatizable complete theory with unbounded types?
Lastly, the theory we have is essentially still a theory of trees, and it is crucial that there are no meaningful relations between sibling nodes. While we attempted something similar for graphs, the lack of this “level-wise independence” makes it difficult to proceed. So can we still generalize this construction?
Question 49. Is there a similar construction for other structures, like graphs?
Acknowledgments↩︎
The author would like to thank Uri Andrews for his helpful suggestions and comments, and Steffen Lempp for proofreading this paper.
References↩︎
We add a superscript \(\mathcal{L}\) here to make explicit that \(\mathcal{M}, \mathcal{N}\) are considered as \(\mathcal{L}\)-structures here.↩︎