Stephen G. Simpson
Department of Mathematics
Draft: May 8, 2000
Pennsylvania State University
This research was partially supported by NSF grant DMS-0070718. For helpful discussions and correspondence, I thank F. Ferreira, A. M. Fernandes, K. Tanaka, and T. Yamazaki.
AMS Subject Classifications: 03F35, 03D30, 03D80, 03B30.
This paper has been accepted for publication in Reverse
Mathematics 2001, to appear.
In this paper we apply recursion-theoretic methods to the study of
-models of subsystems of second order arithmetic.
Specifically, we present some results concerning
subsets of
, along with applications to countable
-models of
. These results and applications may be regarded as an
addendum or supplement to Simpson [30, §VIII.2]. We also
present generalizations to countable non-
-models of
.
These generalizations may be regarded as an addendum to Simpson
[30, §IX.2].
For background on subsystems of second order arithmetic, see Simpson
[30]. We recall here that
is the subsystem consisting
of
comprehension and
induction, and
is the subsystem consisting of
plus Weak König's
Lemma, i.e., the statement that every infinite tree of finite
sequences of
's and
's has a path. These two systems play an
important role in Reverse Mathematics [30]. Their
-models are easy to understand in recursion-theoretic terms.
An
-model of
is a set
such that
(i)
, (ii)
for all
, and
(iii) if
and
then
. An
-model of
has the additional property that if
and
is an
infinite tree of finite sequences of
's and
's, then
has a
path in
.
There is a large recursion-theoretic literature on
subsets
of
and degrees of elements of such sets. An important
paper in this area is Jockusch/Soare [16]. An extensive recent
survey is Cenzer/Remmel [3]. This topic is well known to be
closely related to
-models of
. The connection is as
follows:
is
if and only if there exists
a recursive tree
of finite sequences of
's and
's such that
is a path through
.
In the model-theoretic literature,
-models of
are
known as Scott systems, after Scott [25], who
proved that
is a countable
-model of
if and only if
is the set of sets representable in some
complete extension of Peano arithmetic. This idea is important in the
study of models of arithmetic. See also Kaye [17].
Here is an outline of the rest of this paper.
In §2 we discuss the significance of some of our results, in terms of foundations of mathematics.
In §3 we study and characterize the nonempty
subsets of
which are Medvedev complete. We prove that any
two such sets are recursively homeomorphic (Theorem 3.21).
This is related to a result of Pour-El/Kripke [22] concerning
effectively inseparable theories.
In §4 we relativize and iterate the result of
§3 to obtain a nonempty
set
of
codes for countable
-models of
, with a strong
homogeneity property: any two nonempty
subsets of
are recursively homeomorphic, via a homeomorphism which
preserves the
-models (Theorem 4.11).
In §5 we combine the results of
§§3,4 with Jockusch/Soare forcing, to
obtain a countable
-model of
in which all definable
elements are recursive (Theorem 5.11). This result is
originally due to Friedman [10, unpublished]. In
§6 we improve this result, to obtain a countable
-model of
satisfying
if
is definable from
then
(Theorem 6.9).
In §7 we generalize the results of
§§3,4,5,6 to
non-
-models. In this way we obtain a conservation result,
showing that
plus a strong relative non-definability scheme is
conservative over
-
(Corollary 7.9).
In §8 we prove a recursion-theoretic result of
Kucera [19]: There is a disjoint pair of recursively
inseparable, recursively enumerable sets, such that any two separating
sets which differ infinitely compute the complete recursively
enumerable set (Theorem 8.3). In §9 we
apply Kucera's result to the study of
-models of
.
It is well known that the intersection of all such models consists of
the recursive sets. We now show that the intersection of all such
models which are submodels of a given one may contain nonrecursive
sets (Theorem 9.1).
In §10 we generalize Kucera's result, and we apply
the generalization to the study of non-
-models of
. We
refute several plausible conjectures concerning the relationship
between
and
. See Remarks 10.4,
10.8, 10.9.
Throughout this paper, we use recursion-theoretic concepts and
notation from Rogers [24] and Soare [33]. We use
to denote the set of natural numbers. We
identify points
with functions
.
For
and
, we write
to mean that the Turing machine with Gödel number
and oracle
and input
halts in
steps with output
. For
and
, we write
to mean
that
. Furthermore,
means that
is defined,
i.e.,
, and
means that
is undefined, i.e.,
. For
,
means that
is
Turing reducible to
, i.e.,
. The Turing degree of
, written
, is the set of all
such that
, i.e.,
and
. A predicate
is said to be recursive if
if
, and
if
.
A set
is said to be
if there exists a
recursive predicate
such that
. For
sets
, we shall
consider recursive functionals
given by
for some
and all
,
.
In this section we explore the foundational significance of some of our results.
Foundations of mathematics is the study of the most basic concepts and logical structure of mathematics, with an eye to the unity of human knowledge. For general background in this area, the reader may turn to the van Heijenoort volume [37], where some of the most important modern papers have been carefully translated and reprinted. See also Gödel's collected works [12] and the Friedman volume [13].
As background for our work here, consider the well known foundational
program of computable analysis, i.e., the development of
mathematics in the computable world,
is recursive
.
See Aberth [1] and Pour-El/Richards [23]. This
program is obviously attractive from the viewpoint of Turing's
analysis of computability. However, it is also known that the
assumption ``all real numbers are computable'' conflicts with many
basic, well known theorems of real analysis. For example, it is in
conflict with the maximum principle for continuous real-valued
functions on a closed bounded interval.
Clearly it would be desirable to strike a balance between these
conflicting requirements. A fairly successful attempt in this
direction is Theorem 5.11, below. In non-technical terms,
the theorem asserts the existence of a world where the main theorems
of real analysis hold, and the natural numbers are standard, yet each
definable real number is computable. In technical terms, one obtains
an
-model
of
in which all definable reals are
recursive. The identification of the recursive reals with the
computable reals is an outcome of Turing's foundational work on
computable functions. Thus the computable reals play a large and
important role in
, forming so to speak the ``definable core'' of
. On the other hand, from recent foundational work in Reverse
Mathematics, we know that
is just strong enough to prove many
basic theorems of real analysis. See Simpson [30, Chapter
IV]. Thus
contains just enough non-computable reals in
order to satisfy the demands of real analysis.
Furthermore, in Theorem 6.9 below, we show that the same
-model
satisfies a more general scheme:
For all realsWe also show thatand
, if
is definable from
, then
is Turing reducible to
, i.e., computable using
as an oracle.
The above scheme is foundationally interesting, for the following
reason. Often in mathematics one has the situation that, under some
assumptions on a real parameter
, there exists a unique real
having some property which is stated in terms of
. In this kind of
situation, our scheme allows us to conclude that
is Turing
reducible to
.
In this section we exposit the lattice of Medvedev degrees of nonempty
subsets of
. We prove an important result
concerning nonempty
subsets of
which are Medvedev
complete.
For background on Medvedev degrees of subsets of the Baire space,
, see Rogers [24, §13.7] and Sorbi
[34]. For background on
subsets of the Cantor
space,
, and of the Baire space, see the survey by
Cenzer/Remmel [3].
Proof.In this proof and throughout this paper, we use the following
notation. For
we have
where
and
. We use
to denote the set of strings, i.e., finite
sequences of
's and
's. The length of
is denoted
. For
and
, we
have
and
. For
and
, we
have
given by
To prove our theorem, let
and
be nonempty
subsets
of
. The supremum or least upper bound of
and
is
where
and
. The infimum or greatest lower bound of
and
is
where
Proof.Let
be a standard, recursive enumeration of the
subsets of
. (See Remark 3.9 below.)
In particular, the predicate
is
.
By the Normal Form Theorem for
predicates, we have
where
is primitive recursive. As in
Simpson [30, Lemmas VIII.2.5 and VIII.2.9], put
We are going to show that any two Medvedev complete
subsets
of
are recursively homeomorphic (Theorem 3.21).
In order to prove this, we shall first consider the nature of Medvedev
reducibility in more detail.
Proof.By the Normal Form Theorem for
predicates, we have
Proof.To prove part 1, note that for all
we have
if and only if
and
.
By Lemma 3.5, this is
. For part 2 we have
and
and this is obviously
.![]()
Proof.The predicate
and
is
, so by the
Normal Form Theorem, let
be a primitive recursive
predicate such that
We now introduce a property of nonempty
subsets of
, called productiveness, which will turn out to be
equivalent to Medvedev completeness (Lemma 3.20).
Proof.Put
. Clearly
is nonempty and
. By Lemma 3.5, the predicate
Proof.Because
is productive,
is nowhere dense in
, so
given
we can effectively find
such
that
and
and
and
and
and
. Thus
. Now let
be a splitting function for
. By the Recursion Theorem, we can effectively find
such that
Proof.Let
and
be as in the hypothesis of our lemma. If
is a subalgebra of
and if
is a
monomorphism, let us call
good if, for all
,
if and only if
.
For part 1, to find a recursive functional
from
onto
,
it suffices to find a good recursive monomorphism
.
Assume inductively that we have already found a good finite
monomorphism
, where
is a finite subalgebra of
. (We start with
.) Let
be the
th element
of
with respect to some fixed recursive enumeration of
.
Let
be the finite subalgebra of
generated by
. We effectively extend
to a good finite
monomorphism
, as follows. For each atom
of
, if
or
put
, otherwise use Lemma 3.15 and a
splitting function for
to effectively find
such that
, and
if and only if
, and
if and only if
. Finally we
obtain a good recursive monomorphism
, and
part 1 is proved.
For part 2 we proceed as above, except that we use a back-and-forth
argument involving splitting functions for both
and
. The
inductive hypothesis is that we have a good finite isomorphism
, where
and
are
finite subalgebras of
. Let
be the
th element of
with respect to some fixed recursive enumeration of
. Let
be the finite subalgebra of
generated by
. Use Lemma 3.15 and a splitting
function for
to effectively extend
to a good finite
isomorphism
. Then let
be the finite subalgebra of
generated by
. Use Lemma 3.15 and a splitting
function for
to effectively extend
to a good finite
isomorphism
. Finally we obtain
a good recursive automorphism
, and part 2
is proved.![]()
Proof.Since
, there is a recursive functional
. By
Lemma 3.11, let
be recursive such that
for all
. Let
be a splitting function for
. The predicate
is
(see the proof of
part 1 of Lemma 3.6), so by the S-m-n Theorem, let
be primitive recursive such that
for all
. Now if
and
, we have
and
, hence
and
, hence
and
.
Thus
is a splitting function for
.![]()
Proof.By Lemma 3.19, Medvedev completeness implies
productiveness. By part 1 of Lemma 3.16, productiveness
implies Medvedev completeness.![]()
Proof.This is immediate from Lemmas 3.16 and 3.20.![]()
In this section we relativize and iterate the results of
§3. Our construction is inspired by the idea of
iterated forcing in set theory, as exposited in Jech [14, page
458] and Kunen [18, page 273]. We show that our
construction gives rise to a
set of countable
-models of
with a strong homogeneity property (Theorem
4.11).
Recall that for
and
we have
where
. (See the proofs of
Theorem 3.2 and Lemma 3.3.) For
put
.
Proof.This comes from a uniform relativization of the proof of Lemma
3.3. The predicate
is
, so by the Normal Form Theorem for
predicates,
let
be
primitive recursive such that
. Put
, where
Proof.This comes from a uniform relativization of Lemmas 3.14
and 3.19. Let
be such that, for all
,
. The argument for Lemma 3.14
gives a primitive recursive function
such that,
for all
,
is
-productive with splitting function
. Note also that
for all
. Let
be primitive recursive such
that, for all
and
,
if and
only if
. Let
be primitive
recursive such that, for all
and all
,
. As in the proof of Lemma
3.19 we have that, for all
,
is
-productive with splitting function
.![]()
Proof.If
then clearly
for an appropriate
, hence
. This gives
. The
converse inclusion follows from
.
To see that this is an
-model of
, use Lemma
4.2 plus the following characterization:
is an
-model of
if and only if
(i)
, (ii)
for all
, and
(iii) for all
and
, if
then
.![]()
Proof.This is a uniform relativization of part 2 of Lemma 3.16.![]()
Proof.By Lemma 4.3, the recursive functionals from
onto
given by
are uniformly productive. Hence their
restrictions, from
onto
and from
onto
, are uniformly productive. Begin with the trivial
recursive homeomorphism
. Repeatedly apply
Lemma 4.7 to obtain a recursive sequence of recursive
homeomorphisms
,
,
...,
, ..., such that
for all
. Finally
is given by
.![]()
Proof.Let
be as in Lemma 4.9. Let
and
be such that
. By Lemma 4.9 we have
, hence
for all
, hence
. By
Lemma 4.5 it follows that
.![]()
Proof.This follows from Lemmas 4.5 and 4.10 if we
let
, where
for all
. (Note:
is not the Turing jump of
.)![]()
In this section we combine the previous theorem with so-called
Jockusch/Soare forcing, to obtain an
-model of
in
which all definable elements are recursive (Theorem 5.11).
Proof.Let
,
be an enumeration of the dense arithmetical
subsets of
. Construct a sequence
in
as follows. Begin
with
. Given
, let
be such that
. Finally let
be the unique element of
. Clearly
and
meets each
, hence
is generic.![]()
Proof.For all
we have
if and only if
. For
, put
. We claim that
is dense in
. To see
this, let
be given. If
, then by Lemma 3.5
is
recursive, contrary to assumption. So we have
. Fix such an
and put
. Clearly
and
and
. This proves our claim. Now let
,
be an enumeration of the dense arithmetical subsets of
. As in the proof of Lemma 5.3, given
there exists
such that
meets
for all
, and
meets
for all
. This proves our lemma.![]()
Proof.We are assuming
, so let
be such that
. Put
either
is undefined
or
is defined
. We claim that
is dense in
. To see this, given
, we have
is undefined
, so fix such an
and put
is undefined
. Then clearly
and
. This proves our claim. Since
is dense
arithmetical, let
be such that
. It follows
that
is defined
, so we
have a recursive functional
given by
, and
. Hence by Lemma
3.11 and Remark 3.12,
is truth-table
reducible to
. To show that
is generic, let
be dense arithmetical. Put
or
. By Lemma
3.6,
is dense arithmetical. Let
be such that
. Then
, so
. This completes the
proof.![]()
Proof.Parts 1 and 2 are proved together by a straightforward induction on
the complexity of
. If
is atomic, then for
all
we have that
forces
if and only if
holds for all
, because
and
are elements of
. For
arbitrary
and
of
, we have that
forces
if and only if
if
then
and either
forces
or
forces
. For arbitrary
of
, we have that
forces
if and only if
if
then
and
forces
. For arbitrary
of
, we have that
forces
if and only
if
if
then
does not
force
.![]()
Proof.The proof is straightforward. Set quantifiers in
are
translated as number quantifiers in
.![]()
Proof.Suppose
and
satisfy
and
respectively. Then
and
hold. By
part 1 of Lemma 5.7, there exist
such that
and
and
forces
and
forces
. Since
,
we may safely assume that
. Let
be a recursive homeomorphism as in part 3 of Theorem
4.11. By Lemma 5.5 we have that
is generic. Since
forces
, it follows that
holds, i.e.,
. But, by part 3 of
Theorem 4.11, we have that
. This contradiction
proves our lemma.![]()
Proof.Parts 1 and 2 are immediate from Lemmas 5.7 and
5.9. For part 3, suppose that
and
is
definable without parameters over
. Let
be an
-formula with one free set variable,
, such that
is
the unique
such that
. Letting
be the
-sentence
unique
,
we have that
. By part 1 we have that
forces
. By Lemma
5.4, let
be generic such that
if
then
. Consider
the
-model
. Then
.
Since
and
is generic and
forces
, we have that
holds, i.e.,
. Let
be the unique
such
that
. We claim that
. This is clear from
Lemma 5.9, because for all
and
, we
have
if and only if
and
, if and only if
and
, if and only if
. Since
, it follows that
.![]()
Proof.This follows immediately from Theorem 4.11 and Lemma
5.3 and part 3 of Lemma 5.10.![]()
In this section we prove a key lemma concerning relativized
Jockusch/
[0]Soare genericity (Lemma 6.2). We
then use our lemma to obtain an improvement of Theorem
5.11, involving relative definability and relative
recursiveness, i.e., Turing reducibility (Theorem 6.9).
Proof.Let
be given such that
is dense in
and arithmetical in
. We need to show that
meets
. By Lemma 5.5, there are a
set
and a recursive functional
such that
. It suffices to show that
forces
if
is dense in
then
meets
. Equivalently, we shall show
if
and
forces
is
dense in
, then
and
forces
meets
. To see this, let
be given such that
and
forces
is dense in
. Put
.
Using
as our forcing language, we
have that
forces
is dense in
. In particular,
since
forces
, it follows that
forces
and
. Let
and
be such that
and
forces
and
. Put
and
. Then
,
, and
forces
and
, i.e.,
forces
meets
. This proves our lemma.![]()
Proof.This follows from a straightforward relativization to
of Lemma
5.5.![]()
Proof.A straightforward relativization to
of Lemma 4.5
shows that, for all
,
and this
is an
-model of
. Clearly
is
,
hence
for an appropriate
, hence
.![]()
Proof.The proof of Theorem 4.11 shows that
via a recursive homeomorphism
such that, for all
,
. In particular,
where
. Furthermore,
by Lemma 5.5,
is generic. Part 3 of Lemma
5.10 now gives the desired conclusion.![]()
Proof.This is a straightforward relativization to
of Lemma
6.6.![]()
Proof.As in the proof of Lemma 4.9, construct a recursive
sequence of
-recursive homeomorphisms
,
, such that
for all
. Define
. Then
is an
-recursive
homeomorphism. Furthermore, for
and
, we have
for all
. Hence
.
By Lemmas 4.5 and 6.5, it follows that
.![]()
Proof.Let
be generic, and put
. By Lemma 4.5,
is an
-model of
. Fix
. Fix
such that
. As in
Lemma 6.8, put
, and
let
be an
-recursive homeomorphism of
onto
. We have
. Put
.
By Lemma 6.8,
. By
Lemma 6.2,
is generic over
. Hence, by Lemma
6.3,
is generic over
. It follows by Lemma
6.7 that, for all
, if
is definable over
from
, then
. This completes the proof.![]()
In this section we generalize the results of
§§3,4,5,6 to
countable non-
-models of
.
As in [30, Remark I.7.6], let
-
be first
order Peano arithmetic with the induction scheme restricted to
formulas. The following theorem is well known.
Proof.This result is originally due to Harrington (1977, unpublished).
The proof is in Simpson [30, §IX.2].![]()
Thus any countable model of
-
is the first order part
of a countable model of
. It follows by the Gödel
Completeness Theorem that
-
is the first order part
of
. (See Simpson [30, §IX.2].) We shall strengthen
these results below (Theorems 7.6 and
7.8, Corollary 7.9).
Let
be a countable model of
-
. It is well known
that the familiar concepts and results of classical recursion theory
can be generalized to
-recursion theory. See for instance
Mytilinaios [21]. Let
-
be the set of all
such that
is
definable over
,
i.e., both
and
definable over
allowing
parameters from
. We describe sets
-
as
being
-recursive. It is known from Simpson [30, §
IX.1] that
-
is the smallest
such that
. Thus
-
in
-recursion theory plays the role of
in classical recursion
theory.
A set
is said to be
-finite if it is
-recursive and bounded in
, or equivalently, if there exists an
-canonical index of
. By an
-canonical index of
,
we mean an
such that
, where
is the usual
formula asserting that
occurs in
the binary expansion of
, i.e.,
. Compare Rogers [24, §5.6]. The
-finite sets play the role of finite sets in classical recursion
theory. A set
is said to be
-regular if
is
-finite for each
-finite
. By
Bounded
Comprehension [30, Theorem II.3.9], every
-recursively enumerable set is
-regular. In this paper we shall
have no use for sets which are not
-regular. If
is such that
, then every
is
necessarily
-regular.
We denote by
the set of all
-regular functions
. We denote by
the set of
-strings, i.e., (
-canonical indices of)
-finite
sequences of
's and
's. Clearly
and the
length function
are
-recursive. For
and
, we have an
-string
of length
. We denote
by
the set of nonempty sets of the form
where
is
-recursive. The sets
in
-recursion theory play the role of nonempty
subsets of
in classical recursion theory.
We say that
is complete if for every
there exists an
-recursive functional
. Generalizing
Theorem 3.21, we have:
Proof.This is a straightforward generalization of the arguments of
§3.![]()
Generalizing Theorem 4.11, we have:
Proof.This is a straightforward generalization of the arguments of
§4.![]()
For
the notion of Jockusch/Soare genericity
over
is defined in the obvious way, in terms of dense subsets
of
which are definable over
allowing parameters from
. This notion is equivalent to genericity over
-
in the sense of Simpson [30, §
IX.2]. Generalizing Lemma 5.3, we have:
Proof.See Simpson [30, §IX.2].![]()
Generalizing Lemma 5.4, we have:
Proof.Combine the proof of Lemma 7.4 with a straightforward
generalization of the proof of Lemma 5.4.![]()
Generalizing Theorem 5.11, we have:
Proof.This is a straightforward generalization of the arguments of
§5.![]()
Generalizing Theorem 6.9, we have:
Proof.This is a straightforward generalization of the arguments of
§6.![]()
Proof.This follows from Theorem 7.8 plus Gödel's
Completeness Theorem.![]()
In this section we present a simplified proof of a recursion-theoretic
result of Kucera [19]. Our proof is based on two easy,
well-known lemmas. We present the proof in detail now, because later
we shall need to generalize it to the context of
-recursion theory
where
is a model of
-
.
Proof.We use a movable marker argument, as in Rogers [24, pages
235-236]. We shall have
where
is
the position of marker
at stage
. Thus
Stage
. Begin by defining
for all
. In other
words,
.
Stage
. Let
be the least
such that
and
. If
is
undefined, let
. Thus
for all
.
If
is defined, let
. Thus
Finally put
. Clearly
is a recursively
enumerable set. Note that
takes on each possible value at
most once. Hence
as
, and it is clear
that the construction works.![]()
The following lemma is a strengthening due to K. Ohashi of the well-known Splitting Theorem of R. Friedberg. See Rogers [24, Exercise 12.21].
Proof.Let
be a one-to-one recursive function such that
is the range of
. Put
. Let
(
) be a standard, recursive enumeration of the
recursively enumerable sets. Let
be the finite set of
elements enumerated into
prior to stage
.
To construct
we use a no-injury priority argument. For
each
and
there is a requirement
to the effect that
``if possible''. The
ordering of the requirements is
.
Stage
. Put
.
Stage
. Let
be the least
such that
and either
or
. If
does not exist, or if
, put
into
, i.e.,
and
. Otherwise put
into
, i.e.,
and
.
Finally put
and
. Clearly
and
are recursively enumerable sets, and
. It is also clear that
takes on each possible value at
most twice, hence
as
.
We claim that
and
are recursively inseparable. Assume
for a contradiction that
is a recursive set which separates
and
, i.e.,
and
.
Let
and
be such that
and
. Then
and
. For all
sufficiently large
we have
, hence
. Thus there is a finite set
such that for all
there exists
such that
. On the other hand, we also have
that for all
there exists
such that
. It follows that
is
recursive, a contradiction.![]()
The following theorem and its corollaries are due to Kucera [19].
Proof.Let
be a recursively enumerable set as in Lemma 8.1.
Then clearly
for any infinite set
. By Lemma 8.2 let
be
a disjoint, recursively inseparable pair of recursively enumerable
sets such that
. Now let
and
be separating
sets. Then
and
.
Hence
and we have our result.![]()
The previous theorem is of interest with respect to
subsets
of
. An extensive survey of this part of recursion theory
is Cenzer/Remmel [3]. It is known that a nonempty
subset of
with no recursive elements necessarily has
elements of
distinct Turing degrees, among which are
infinitely many pairwise incomparable Turing degrees
.
We now get:
Proof.Let
be as in Theorem 8.3. Let
be the
set of (characteristic functions of) separating sets for
. If
and
are the Turing degrees
of
respectively, it follows from the conclusion of
Theorem 8.3 that either
or
.![]()
If
is a Turing degree, we write
to mean that every nonempty
subset of
contains at
least one element of Turing degree
. This is
equivalent to
being the degree of a complete extension of
Peano arithmetic. See also Jockusch/Soare [16] and Simpson
[27, §6]. It is known that there exist
and
such that
. We now get:
In this section we apply Kucera's result to the study of
-models of
. For background on this subject, see
Simpson [30, §VIII.2].
It is known that minimal
-models of
do not exist,
i.e., every
-model of
has a proper
-submodel
of
. It is also known that the intersection of all
-models of
is
, the set of recursive sets. We
now have:
Proof.Let
be as in Theorem 8.3. Since
proves
separation [30, Lemma IV.4.4], every
-model of
contains a separating set for
.
Let
be an
-model of
such that
, where
is the complete recursively enumerable set. Let
be a
separating set for
. Obviously
is not recursive. We
claim that
. Given
such that
, let
be a
separating set for
. Since
but
, the
conclusion of Theorem 8.3 implies that the symmetric
difference
is finite. Since
, it follows that
. This gives our result.![]()
The above theorem concerning
-models of
is in contrast
to the following theorem of Simpson [30, Corollary VIII.6.10]
concerning
-models of
. This is one instance where the
well-known analogy [30, pages 40 and 314] between
-models of
and
-models of
breaks down.
Actually Simpson [30, Corollary VIII.6.10] obtains not only
Theorem 9.3 for
-models of
, but also an
appropriate generalization for arbitrary models of
.
In this section we generalize Kucera's result and apply the
generalization to the study of non-
-models of
. For
background on non-
-models of
, see Simpson [30, §
VIII.2].
Proof.This follows from a straightforward formalization of our proof of
Theorem 8.3 via Lemmas 8.1 and 8.2
above, with
. The key point for the success of the priority argument for
Lemma 8.2 is that
as
. This
is provable in
because of Bounded
Comprehension
[30, Theorem II.3.9].![]()
Proof.That
satisfies 1, 2, 3 is immediate from Lemma
10.1. Let
be such that
.
Then
-
, but for every
such that
we have
. See also Theorem
9.1 and its proof.![]()
As in §7, let
-
be first order Peano
arithmetic with the induction scheme restricted to
formulas. For
we define
-
similarly, with
the induction scheme restricted to
formulas.
Proof.Let
be a countable model of
-
. By
[30, Exercise IX.2.8], there exists a countable
such that
is a model of
``
does not
exist''. Our result now follows from Theorem 10.3.![]()
Proof.Any model of
having
as its first order part is of the
form
where
. We claim that
necessarily satisfies ``
does not exist''. Otherwise, let
be such that
``
is the complete recursively
enumerable set''. Clearly any
formula without set
parameters is equivalent over
to a
formula with
parameter
. Since
includes induction for all
formulas with set parameters,
satisfies
induction for all
formulas with parameter
. Hence
satisfies induction for all
formulas without
set parameters. In other words,
-
, a
contradiction. This proves the claim. Our result now follows from
Theorem 10.3.![]()
Proof.Let
be the
formula of Lemma 10.1. Let
be a
sentence which is provable in
-
but not in
-
. (For instance, we
may take
to be the
sentence
expressing consistency of
-
.) We may assume that
is
. Let
be the
formula
Reasoning inif
then
, and
if
least element of
then
and
.
This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html -split 0 pizowkl
The translation was initiated by Stephen G Simpson on 2004-11-01