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 reals and , if is definable from , then is Turing reducible to , i.e., computable using as an oracle.We also show that plus the above scheme has the same first order part as alone. See Corollary 7.9, below.
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
if then , andReasoning in , suppose is such that holds. If then we have , hence . Now suppose . Then where holds and is the least such that . Since fails, - fails. Hence by Corollary 10.6 we have is finite. This implies is finite. The rest follows easily from Theorem 10.3.
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