**Carl Mummert ^{1}
Stephen G. Simpson^{2}
Department of Mathematics
Pennsylvania State University
State College, PA 16802, USA**

**March 23, 2004
Submitted for JSL December 16, 2003
Accepted February 13, 2004**

Let *n* be a positive integer. By a -model we mean an
-model which is elementary with respect to
formulas. We prove the following -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 -model of *S*, then there exists a
-model of *S*+``there is no countable -model of
*S*.'' We also prove a -model version of Löb's Theorem.
As a corollary, we obtain a -model which is not a
-model.

Let
denote the set of natural numbers
.
Let
denote the set of all subsets of .
An
*-model* is a nonempty set
,
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 *-model* is an -model which is an
elementary submodel of
with respect to
formulas of the language of second order arithmetic.

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

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

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

*
*

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
and intended to
range over ,
and second order (set) variables, denoted
and intended to range over .
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 .
For *M* an -model and an *L*_{2}-sentence with parameters from *M*, we define
to mean that *M* *satisfies* ,
i.e.,
is true in the
*L*_{2}-model
.
If *S* is a set
of *L*_{2}-sentences, we define
to mean that
for all .

An *L*_{2}-formula is said to be *arithmetical* if it contains no
set quantifiers. An *L*_{2}-formula is said to be
if it is
equivalent to a formula of the form

with

If *X* is a subset of ,
then *X* can be viewed as coding a
countable -model
,
where
.
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 -model* is then a countable coded
-model *X* such that
is a
-model.

We now present the main theorem of this paper. Our theorem is a -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].

Our -model version of Löb's Theorem [7] is as follows.

``every countable coded -model of *S* satisfies
''
,

then every -model of

In this section we draw corollaries concerning -models which are not -models. In order to do so, we need the following lemmas, which are well known.

We now present our corollaries.

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

**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.

This document was generated using the
**LaTeX**2`HTML` translator Version 98.1p1 release (March 2nd, 1998)

Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:

**latex2html** `-split 0 betan.tex`.

The translation was initiated by Stephen G Simpson on 2004-03-23

- ... Mummert
^{1} -
`http://www.math.psu.edu/mummert/`. Mummert's research was partially supported by a VIGRE graduate traineeship under NSF Grant DMS-9810759. - ... Simpson
^{2} -
`http://www.personal.psu.edu/t20/`. Simpson's research was partially supported by NSF Grant DMS-0070718.