An Incompleteness Theorem for β_{n}-Models

Carl Mummert^{∗} Stephen G. Simpson^{†}

Department of Mathematics Pennsylvania State University State College, PA 16802, USA

February 13, 2004

Submitted for JSL December 16, 2003 Accepted February 13, 2004

Abstract Let n be a positive integer. By a β_{n}-model we mean an ω-model which is elementary with respect to Σ_{n}^{1} formulas. We prove the following β_{n}-model version of Gödel’s Second Incompleteness Theorem. For any recursively axiomatized theory S in the language of second order arithmetic, if there exists a β_{n}-model of S, then there exists a β_{n}-model of S + “there is no countable β_{n}-model of S.” We also prove a β_{n}-model version of Löb’s Theorem. As a corollary, we obtain a β_{n}-model which is not a β_{n+1}-model.

1 Introduction

Let ω denote the set of natural numbers {0, 1, 2, …}. Let P (ω) denote the set of all subsets of ω. An ω-model is a nonempty set M ⊆ P (ω), viewed as a model for the language of second order arithmetic. Here the number variables range over ω, the set variables range over M, and the arithmetical operations are standard. For n a positive integer, a β_{n}-model is an ω-model which is an elementary submodel of P (ω) with respect to Σ_{n}^{1} formulas of the language of second order arithmetic.

Recently Engström [3] posed the following question: Does there exist a β_{n}- model which is not a β_{n+1}-model? To our amazement, there seems to be no answer to this question in the literature.

∗http://www.math.psu.edu/mummert/. Mummert’s research was partially supported by a VIGRE graduate traineeship under NSF Grant DMS-9810759.

†http://www.math.psu.edu/simpson/. Simpson’s research was partially supported by NSF Grant DMS-0070718.

Previous research has focused on minimum β_{n}-models. A minimum β_{n}- model is a β_{n}-model which is included in all β_{n}-models. If a minimum β_{n}- model exists, then obviously it is unique, and it is not a β_{n+1}-model. However, the existence of minimum β_{n}-models is problematic, to say the least. Simpson [10, Corollary VIII.6.9] proves that there is no minimum β_{1}-model. Shilleto [8] proves the existence of a minimum β_{2}-model. Enderton and Friedman [2] prove the existence of minimum β_{n}-models, n ≥ 3, assuming a basis property which follows from V = L but which is not provable in ZFC. We conjecture that the existence of a minimum β_{n}-model is not provable in ZFC, for n ≥ 3. We have verified this conjecture for n ≥ 4. Simpson’s book [10, Sections VII.1–VII.7 and VIII.6] contains further results concerning minimum β_{1}- and β_{2}-models of specific subsystems of second order arithmetic, as well as β_{n}-models for n ≥ 3. See also Remark 3.6 below.

In this paper we answer Engström’s question affirmatively. We prove that, for each n ≥ 1, there exists a β_{n}-model which is not a β_{n+1}-model (Corollary 3.7). Our proof is based on a β_{n}-model version of Gödel’s Second Incompleteness Theorem (Theorem 2.1). We draw corollaries concerning β_{n}-models of specific true theories (Corollary 3.3, Remark 3.5). We also obtain a β_{n}-model version of Löb’s Theorem (Theorem 2.3).

Preliminaries

Our results are formulated in terms of L_{2}, the language of second order arithmetic. L_{2} has variables of two sorts: first order (number) variables, denoted i, j, k, m, n, … and intended to range over ω, and second order (set) variables, denoted X, Y, Z, … and intended to range over P (ω). The variables of both sorts are quantified. We also have addition, multiplication, equality, and order for numbers, denoted +, ·, =, <, as well as set membership, denoted ∈. Recall that an ω-model is a nonempty subset of P (ω). For M an ω-model and Φ an L_{2}-sentence with parameters from M, we define M ⊧ Φ to mean that M satisfies Φ, i.e., Φ is true in the L_{2}-model (ω, M, +, ·, =, <, ∈). If S is a set of L_{2}-sentences, we define M ⊧ S to mean that M ⊧ Φ for all Φ ∈ S.

An L_{2}-formula is said to be arithmetical if it contains no set quantifiers. An L_{2}-formula is said to be Σ_{n}^{1} if it is equivalent to a formula of the form

∃X_{1}∀X_{2}∃X_{3} ⋯ X_{n} Θ

with n alternating set quantifiers, where Θ is arithmetical. An L_{2}-formula is said to be Π_{n}^{1} if its negation is Σ_{n}^{1}. A β_{n}-model is an ω-model M such that, for all Σ_{n}^{1} formulas Φ(X_{1}, …, X_{k}) with exactly the free variables displayed, and for all A_{1}, …, A_{k} ∈ M,

P (ω) ⊧ Φ(A_{1}, …, A_{k}) ⇔ M ⊧ Φ(A_{1}, …, A_{k}).

If X is a subset of ω, then X can be viewed as coding a countable ω-model {(X)_{i} : i ∈ ω}, where (X)_{i} = {j : 2^{i}3^{j} ∈ X}. Moreover, every countable ωmodel can be coded in this way. Therefore we define a countable coded ω-model to be simply a subset of ω. A countable coded β_{n}-model is then a countable coded ω-model X such that {(X)_{i} : i ∈ ω} is a β_{n}-model.

2 A β_{n}-model version of Gödel’s Theorem

We now present the main theorem of this paper. Our theorem is a β_{n}-model version of Gödel’s Second Incompleteness Theorem [6]. It was inspired by the ω-model version, due to Friedman [4, Chapter II], as expounded in Simpson [10, Theorem VIII.5.6]. See also Steel [11] and Friedman [5].

Theorem 2.1. Let S be a recursively axiomatized theory in the language of second order arithmetic. For each n ≥ 1, if there exists a β_{n}-model of S, then there exists a β_{n}-model of S + “there is no countable coded β_{n}-model of S.”

Proof. We use the subsystem ACA_{0}^{+} of second order arithmetic. The axioms of ACA_{0}^{+} consist of the basic axioms, induction, arithmetical comprehension, and “for every set X, the ωth Turing jump of X exists.” See Blass/Hirst/Simpson [1] and Simpson [10, Definition X.3.2]. Note that every β_{n}-model automatically satisfies ACA_{0}^{+}. Furthermore, ACA_{0}^{+} proves that for every countable coded ω-model there exists a full satisfaction predicate. This allows us to write L_{2}-formulas which assert certain properties of countable coded ω-models. Let B_{n}(X) be the L_{2}-formula asserting that X is a countable coded β_{n}-model. Let Sat(X, S) be the L_{2}-formula asserting that X ⊧ S, i.e., the countable ω-model {(X)_{i} : i ∈ ω} satisfies Φ for all Φ ∈ S. For brevity we introduce the L_{2}-formula

B_{n}(X, S) ≡ B_{n}(X) ∧ Sat(X, S)

asserting that X is a countable coded β_{n}-model of S.

Consider the L_{2}-theory T consisting of ACA_{0}^{+} + Φ_{1} + Φ_{2}, where

\begin{aligned}Φ_{1} & ≡ & ∃X B_{n}(X, S) , \\ Φ_{2} & ≡ & ∀Y (B_{n}(Y, S) ⇒ Y ⊧ ∃Z B_{n}(Z, S)) . \end{aligned}

We claim that T proves Con(T), the standard L_{2}-sentence asserting consistency of T. To see this, we reason within T. By Φ_{1} there exists X such that B_{n}(X, S) holds. We claim that X satisfies T. Being a β_{n}-model, X satisfies ACA_{0}^{+}. Furthermore, in light of Φ_{2}, X satisfies Φ_{1}. It remains to show that X satisfies Φ_{2}. For this, let Y = (X)_{i} be such that X satisfies B_{n}(Y, S). Then B_{n}(Y, S) is true, because a β_{n}-submodel of a β_{n}-model is a β_{n}-model. Hence by Φ_{2} we have Y ⊧ ∃Z B_{n}(Z, S). We conclude that X ⊧ Φ_{2}. We have now shown that X is a model of T. Thus T is consistent. Our claim is proved.

We have shown that T proves Con(T). From this plus Gödel’s Second Incompleteness Theorem [6], it follows that T is inconsistent. In other words, Φ_{1} ⇒ ¬ Φ_{2} is provable in ACA_{0}^{+}. Since ACA_{0}^{+} is true, Φ_{1} ⇒ ¬ Φ_{2} is true.

To prove Theorem 2.1, assume the existence of a β_{n}-model of S. By the Löwenheim/Skolem Theorem, there exists a countable coded β_{n}-model of S. In other words, Φ_{1} holds. Therefore, ¬ Φ_{2} holds, i.e., there exists a β_{n}-model of S which does not contain a countable coded β_{n}-model of S. This completes the proof of Theorem 2.1.

Remark 2.2. In proving Theorem 2.1, we have actually proved more. Namely, we have proved that Theorem 2.1 is provable in ACA_{0}^{+}. Actually we could replace ACA_{0}^{+} throughout this paper by the weaker theory ACA_{0}^{∗} = ACA_{0} + ∀n ∀X (the nth Turing jump of X exists).

Our β_{n}-model version of Löb’s Theorem [7] is as follows.

Theorem 2.3. Let S be a recursively axiomatized L_{2}-theory. Let Φ be an L_{2}- sentence. For each n ≥ 1, if every β_{n}-model of S satisfies

“every countable coded β_{n}-model of S satisfies Φ” ⇒ Φ,

then every β_{n}-model of S satisfies Φ.

Proof. This is a reformulation of Theorem 2.1 with S replaced by S + ¬ Φ.

3 Some corollaries of Theorem 2.1

In this section we draw corollaries concerning β_{n}-models which are not β_{n+1}- models. In order to do so, we need the following lemmas, which are well known.

Lemma 3.1. For each n ≥ 1, the formula B_{n}(X, S) is equivalent to a Π_{n}^{1} formula. The equivalence is provable in ACA_{0}^{+}.

Proof. Note that an ω-model M is a β_{n}-model if and only if

∀e ∀ Y, Z ∈ M (Ψ_{n}(e, Y, Z) ⇒ M ⊧ Ψ_{n}(e, Y, Z)),

where Ψ_{n}(e, X, Y) is a universal Σ_{n}^{1} formula. (The existence of such a formula is provable in ACA_{0}^{+}, or actually in ACA_{0}. See Simpson [10, Lemma V.1.4 and pages 252, 306, 333].) Applying this observation to the countable ω-model M = {(X)_{i} : i ∈ ω} coded by X, we have in ACA_{0}^{+} that B_{n}(X) holds if and only if

∀e ∀i ∀j (Ψ_{n}(e, (X)_{i}, (X)_{j}) ⇒ X ⊧ Ψ_{n}(e, (X)_{i}, (X)_{j})).

Thus B_{n}(X) is Π_{n}^{1}. Furthermore, ACA_{0}^{+} proves the existence of a full satisfaction predicate for X which is implicitly defined by an arithmetical formula. Thus Sat(X, S) is both Σ_{1}^{1} and Π_{1}^{1}. We now see that B_{n}(X, S) is Π_{n}^{1}.

Lemma 3.2. Let S be a recursively axiomatized L_{2}-theory. Assume the existence of a β_{n}-model of S. Let M be an ω-model of ACA_{0}^{+}+“there is no countable coded β_{n}-model of S.” Then M is not a β_{n+1}-model.

Proof. Lemma 3.1 implies that the sentence ∃X B_{n}(X, S) is Σ_{n+1}^{1}. Our hypotheses imply that this sentence holds in P (ω) but not in M. Thus M is not a β_{n+1}-model.

We now present our corollaries.

Corollary 3.3. Let S be a recursively axiomatized L_{2}-theory. For each n ≥ 1, if there exists a β_{n}-model of S, then there exists a β_{n}-model of S + “there is no countable coded β_{n}-model of S.” Such a β_{n}-model is not a β_{n+1}-model.

Proof. This is immediate from Theorem 2.1 and Lemma 3.2, noting that any β_{n}-model satisfies ACA_{0}^{+}.

Corollary 3.4. Let S be a recursively axiomatized L_{2}-theory which is true, i.e., which holds in P (ω). Then for each n ≥ 1 there exists a β_{n}-model of S + “there is no countable coded β_{n}-model of S.” Such a β_{n}-model is not a β_{n+1}-model.

Proof. This is immediate from Corollary 3.3, since P (ω) is a β_{n}-model.

Remark 3.5. In Corollary 3.4, S can be any true recursively axiomatized L_{2}- theory. For example, we may take S to be any of the following specific L_{2}- theories, which have been discussed in Simpson [10]: Π_{m}^{1} comprehension, Π_{m}^{1} transfinite recursion, Σ_{m}^{1} choice, Σ_{m}^{1} dependent choice, strong Σ_{m}^{1} dependent choice, m ≥ 1, or any union of these, e.g., Π_{∞}^{1} comprehension, Σ_{∞}^{1} choice, Σ_{∞}^{1} dependent choice. Note that Π_{∞}^{1} comprehension is full second order arithmetic, called Z_{2} in [10].

Remark 3.6. Let S be any of the specific L_{2}-theories mentioned in Remark 3.5, except Σ_{1}^{1} choice and Σ_{1}^{1} dependent choice. By a minimum β_{n}-model of S we mean a β_{n}-model of S which is included in all β_{n}-models of S. For n = 1, 2 a minimum β_{n}-model of S can be obtained by methods of Simpson [10, Chapter VII] and Shilleto [8] respectively. For n ≥ 3 a minimum β_{n}-model of S can be obtained by methods of Simpson [10, Chapter VII] and Enderton/Friedman [2] assuming V = L.

We answer Engström’s question [3] affirmatively as follows.

Corollary 3.7. For each n ≥ 1 there exists a β_{n}-model which is not a β_{n+1}- model.

Proof. In Corollary 3.4 let S be the trivial L_{2}-theory with no axioms.

Remark 3.8. Corollary 3.7 follows from the results of Enderton/Friedman [2] assuming V = L. We do not know of any proof of Corollary 3.7 in ZFC, other than the proof which we have given here.

References

[1] Andreas R. Blass, Jeffry L. Hirst, and Stephen G. Simpson. Logical analysis of some theorems of combinatorics and topological dynamics. In [9], pages 125–156, 1987.

[2] Herbert B. Enderton and Harvey Friedman. Approximating the standard model of analysis. Fundamenta Mathematicae, 72(2):175–188, 1971.

[3] Fredrik Engström, October 2003. Private communication.

[4] Harvey Friedman. Subsystems of Set Theory and Analysis. PhD thesis, Massachusetts Institute of Technology, 1967. 83 pages.

[5] Harvey Friedman. Uniformly defined descending sequences of degrees. Journal of Symbolic Logic, 41:363–367, 1976.

[6] Kurt Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik, 38:173–198, 1931.

[7] M. H. Löb. Solution of a problem of Leon Henkin. Journal of Symbolic Logic, 20:115–118, 1955.

[8] J. R. Shilleto. Minimum models of analysis. Journal of Symbolic Logic, 37:48–54, 1972.

[9] S. G. Simpson, editor. Logic and Combinatorics. Contemporary Mathematics. American Mathematical Society, 1987. XI + 394 pages.

[10] Stephen G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, 1999. XIV + 445 pages.

[11] John R. Steel. Descending sequences of degrees. Journal of Symbolic Logic, 40:59–61, 1975.