Generalized separation principles
It is well-known that computability theory and reverse mathematics have very strong ties. Indeed, the base theory used in reverse mathematics was designed as the minimal theory that can adequately formulate and prove the basic results of computability theory. Based on the Church–Turing thesis, this is a very reasonable way to capture the proof method known as direct computation in everyday mathematics. Although the ties run very deep, there are always frictions when translating results between computability theory and reverse mathematics. The aim of this post is to talk about different ways of doing this translation but I will do so by talking about a family of generalized separation principles that I recently realized were (non-trivially) equivalent, a fact that had been well known in computability theory for several decades.
Three central notions in computability theory are computable sets and functions, computably enumerable sets, and partial computable functions. The better known way to translate these into reverse mathematics is to use the correspondences
Since includes -comprehension, computable sets correspond to actual sets in reverse mathematics but, since -comprehension is only available in and beyond, computably enumerable sets must always be accessed by indirect means such as -formulas. The drawback of this translation is that -formulas are not part of the everyday language of mathematics so the principles that arise in this way, no matter how useful, do not fit well with the goals of reverse mathematics.
A poignant example is the very handy -separation scheme:
where and range over formulas. This principle is directly inspired by inseparable pairs in computability theory, i.e., a pair of disjoint computably enumerable sets and such that there is no computable set such that and The existence of such pairs shows that some instances of -separation fail in and hence are not provable in
It turns out that the -separation scheme is equivalent to over Since the weak König lemma is widely used in combinatorics, this is a well justified object of study for reverse mathematics. In practice, though, many reversals involving the weak König lemma go through -separation instead. To avoid bringing in -formulas, the scheme is often stated in the following alternate form:
If are one-to-one functions with disjoint ranges, then there is a set such that and for all
This translation uses the fact that infinite computably enumerable sets are precisely the ranges of one-to-one computable functions. Separating sets always exist when one of the two computably enumerable sets is finite so it is harmless to exclude that case.
While using enumerations as above makes a lot of sense, excluding finite sets is sometimes harmful; even if repetitions are allowed, excluding the empty set is also sometimes harmful. This issue pops up in computability theory too and, fortunately, computability theorists have found a nice solution. Every computably enumerable can be represented as the union of a computable sequence of finite sets, in fact, a nondecreasing sequence of finite sets. In other words, every computably enumerable set can be enumerated by a process that outputs a finite (possibly zero) number of elements into the set at every stage. This idea is interesting since it is not too far removed from mathematical practice. It is unusual to enumerate things in such a general manner, but this extra generality is there to fix a genuine problem; standard enumerations can be substituted when this is harmless.
Recently, I’ve taken the habit of using the term enumerable set for a nondecreasing sequence of (coded) finite sets. Since the actual enumeration is usually irrelevant, I often use these as if they were actual sets. So I write to mean
and even to mean
The term enumerable set is a slightly dangerous abuse since enumerable sets are not necessarily sets in the context reverse mathematics. Nevertheless, I find the translation
very compelling. I sometimes use decidable set instead of plain set for emphasis. With this convention, -separation can be stated as follows.
If and are disjoint enumerable sets, then there is a decidable set such that and
This is almost identical to the negation of the existence of an inseparable pair.
Since partial computable functions are precisely the partial functions with computably enumerable graphs, it seems appropriate to use partial enumerable function to mean a partial function whose graph is an enumerable set. Note that if a partial enumerable function happens to be total, then is a predicate so is a total function whose graph is a set in If and are disjoint enumerable sets, then is a partial enumerable function and is a separating set for and precisely when is a total extension of Thus we obtain yet another formulation of -separation:
Every partial enumerable function can be extended to a total function
It seems we just gained a new parameter. Instead of extending a partial enumerable function we could try to extend a partial enumerable function Because of binary representation, there is no gain here: separating mutually disjoint enumerable sets is not harder than separating just two. However, the ability to extend any partial enumerable function to a total one is equivalent to arithmetic comprehension.
This brings us to the most computably-theoretic reverse mathematics principle: In computability theory, a function is diagonally non-computable if where is the -th partial computable function in the standard enumeration. This concept relativizes as usual, and is the statement that there is an -diagonally non-computable function for every set While this is perhaps the most natural way to state we can avoid the reference to the standard enumeration of the partial computable functions by formulating it as follows:
For every partial enumerable function there is a total function such that for every
This clearly implies the usual formulation of and the universal properties of the standard enumeration show that this statement is equivalent. The reason why is so handy is that it is a non-trivial consequence of which is easily accessible to methods from computability theory. To see that follows from consider the strengthened version :
For every partial enumerable function there is a total function such that for every
The function is as required exactly when is a total extension of
Once again, we have gained an extra parameter. Could the sequence of principles
form a strictly descending chain from to ? It turns out that these principles are all equivalent to but before we see why that is, let’s consider yet another way to formulate these principles. It is easy to see that is equivalent to:
If are mutually disjoint enumerable sets, then there is a total function such that for every
In this light, we see that the assumption that the enumerable sets are mutually disjoint is unnecessarily strong: the minimal requirement for the conclusion to hold is that This fact was observed by Cenzer and Hinman (2008), who introduced yet another parameter to formulate the generalized separation principles :
If are enumerable sets such that the intersection of any of them is empty, then there is a total function such that for every
Cenzer and Hinman looked at these from the perspective of Medvedev degrees of -classes. They found that the Medvedev degrees associated to these generalized separation principles have a rich structure, but that this structure trivializes when considering Muchnik degrees instead. From the perspective of reverse mathematics, this suggests that all of these principles are equivalent to This pretty much the case but we will soon see that there is a little twist to this story…
At this point, we have a doubly indexed array of generalized separation principles and the following implications:
Note that all of these are easy consequences of so the question is whether any of them are strictly weaker. The following lemma allows us to walk backwards in this array. The argument is due to Richard Friedberg, but it was first published by Jockusch Jr. (1989) (for ).
Lemma (). For all positive integers and implies . In particular, implies
Proof. Let be enumerable sets such that the intersection of any of them is empty. Our goal is to find a function such that for every
Consider the enumerable sets defined by
for These sets have the property that the intersection of any of them is empty. It follows from that there is a function such that for every Define by the equation
Note that if and then either or We now consider two cases.
If for every there is a such that then let be such that for every Note that we must then have for every which means that is as required.
Otherwise, there is an such that for every In that case, is as required. QED
This collapses the entire array of generalized separation principles, but the final alternative in the proof requires to decide a statement. This is why the Medvedev degrees associated to these principles have such a rich structure, but the associated Muchnik degrees do not. Reverse mathematics also shows little sensitivity to such complex decisions, but it is not completely insensitive since the ability to compound such decisions requires some induction.
Lemma (). For all positive integers and implies In particular, implies .
Proof. We proceed as in the previous proof, except that the sets are now defined by
for all These enumerable sets again have the property that the intersection of any of them is empty, so it follows from that there is a function such that for every Again, define by
(Note that since could be non-standard, all -tuples are understood to be coded -tuples but we will not be too fussy about proper notation.)
By we can find the largest index for which there is some sequence such that
holds for all choices of It follows that for every choice of we can find some sequence such that
Thus, the function defined by
for the first sequence as above is necessarily such that for all QED
So, assuming we can walk backwards along the bottom row of the array even by a non-standard number of steps. Now (or ) does not make sense as a stand-alone principle when is nonstandard, but the limiting principle (equivalently ) does make sense and it does allow for the witness to be non-standard.
Proposition (). is equivalent to the weak König lemma.
While is the precise amount of induction needed to carry out the above proof, that does not mean that so much induction is necessary for the reversal.
Is the assumption necessary for the last proposition?
Perhaps there is another argument that only uses or ? Such necessary uses of induction are rare, but an example of this was recently found by Neeman (2011). It would be interesting to see if this happens again in this case…
D. Cenzer, P. G. Hinman, 2008: Degrees of difficulty of generalized r.e. separating classes, Arch. Math. Logic 46, no. 7–8, 629–647.
C. G. Jockusch Jr., 1989: Degrees of functions with no fixed points, Logic, Methodology and Philosophy of Science VIII, Studies in Logic and the Foundations of Mathematics 126, 191–201.
I. Neeman, 2011: Necessary use of $\Sigma^1_1$ induction in a reversal, J. Symbolic Logic 76, no. 2, 561–574.
François G. Dorais wrote
Paul Shafer kindly pointed out that Steve Simpson had already asked in 2001 whether is equivalent to the weak König lemma over . (See these slides.)
Carl Mummert wrote
For those comparing this with classic reverse math literature, they would have talked about the range of a function instead of an enumerable set in the sense given here (mostly to camouflage the terminology ). Thus the classic “Every function has a range” would translate to “Every enumerable set is decidable”. The terminology “decidable set” is also nice because it brings out the relationship with constructive systems, where “set” does not mean “decidable set”.
Carl Mummert wrote
Another classic example of necessary induction in a reversal is that is equivalent to in the real world and also equivalent over plus induction, but not over alone. I believe there are several other examples of this in Simpson’s book, for example Theorem VII.6.9(2), although they are not emphasized as having this property.
All the ones I’m aware of are for induction. Are you aware of any for something like induction?
Carl Mummert replied to François G. Dorais
There is an example in “The Atomic Model Theorem and Type Omitting” by Hirschfeldt, Shore, and Slaman. They showed that the two principles and AMT are not equivalent over but they are equivalent over plus induction. This is described in their paper in the prose below Corollary 4.5.
François G. Dorais wrote
Edits: Fixed small typos. Reformatted references.