François G. Dorais

Topics
• Computability Theory
• Reverse Mathematics

Generalized separation principles

It is well-known that computability theory and reverse mathematics have very strong ties. Indeed, the base theory $\newcommand{\RCA}{\mathsf{RCA}_0}\RCA$ 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 $\RCA$ includes $\Delta^0_1$-comprehension, computable sets correspond to actual sets in reverse mathematics but, since $\Sigma^0_1$-comprehension is only available in $\newcommand{\ACA}{\mathsf{ACA}_0}\ACA$ and beyond, computably enumerable sets must always be accessed by indirect means such as $\Sigma^0_1$-formulas. The drawback of this translation is that $\Sigma^0_1$-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 $\Sigma^0_1$-separation scheme:

where $\phi$ and $\psi$ range over $\Sigma^0_1$ formulas. This principle is directly inspired by inseparable pairs in computability theory, i.e., a pair of disjoint computably enumerable sets $A$ and $B$ such that there is no computable set $C$ such that $A \subseteq C$ and $B \cap C = \varnothing.$ The existence of such pairs shows that some instances of $\Sigma^0_1$-separation fail in $\mathrm{REC}$ and hence are not provable in $\RCA.$

It turns out that the $\Sigma^0_1$-separation scheme is equivalent to $\newcommand{\WKL}{\mathsf{WKL}_0}\WKL$ over $\RCA.$ 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 $\Sigma^0_1$-separation instead. To avoid bringing in $\Sigma^0_1$-formulas, the scheme is often stated in the following alternate form:

If $f,g:\N\to\N$ are one-to-one functions with disjoint ranges, then there is a set $C$ such that $f(n) \in C$ and $g(n) \notin C$ for all $n.$

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 $A = \seq{a_s}_{s=0}^\infty$ of (coded) finite sets. Since the actual enumeration is usually irrelevant, I often use these as if they were actual sets. So I write $n \in A$ to mean

$A \subseteq B$ to mean

and even $A = B$ 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, $\Sigma^0_1$-separation can be stated as follows.

If $A$ and $B$ are disjoint enumerable sets, then there is a decidable set $C$ such that $A \subseteq C$ and $B \cap C = \varnothing.$

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 $F$ happens to be total, then $F(n) = m$ is a $\Delta^0_1$ predicate so $F$ is a total function whose graph is a set in $\RCA.$ If $A$ and $B$ are disjoint enumerable sets, then $F = A\times\set{0} \cup B \times\set{1}$ is a partial enumerable function and $C$ is a separating set for $A$ and $B$ precisely when $\bar{F} = C\times\set{0}\cup(\N-C)\times\set{1}$ is a total extension of $F.$ Thus we obtain yet another formulation of $\Sigma^0_1$-separation:

Every partial enumerable function $F:\N\to\set{0,1}$ can be extended to a total function $\bar{F}:\N\to\set{0,1}.$

It seems we just gained a new parameter. Instead of extending a partial enumerable function $\N\to\set{0,1}$ we could try to extend a partial enumerable function $\N\to\set{0,\dots,k-1}.$ Because of binary representation, there is no gain here: separating $k$ mutually disjoint enumerable sets is not harder than separating just two. However, the ability to extend any partial enumerable function $\N\to\N$ to a total one is equivalent to arithmetic comprehension.

This brings us to the most computably-theoretic reverse mathematics principle: $\newcommand{\DNR}{\mathsf{DNR}}\DNR.$ In computability theory, a function $F:\N\to\N$ is diagonally non-computable if $F(n) \neq \phi_n(n)$ where $\phi_n$ is the $n$-th partial computable function in the standard enumeration. This concept relativizes as usual, and $\DNR$ is the statement that there is an $A$-diagonally non-computable function for every set $A.$ While this is perhaps the most natural way to state $\DNR,$ we can avoid the reference to the standard enumeration of the partial computable functions by formulating it as follows:

For every partial enumerable function $F:\N\to\N$ there is a total function $G:\N\to\N$ such that $F(n) \neq G(n)$ for every $n \in \operatorname{dom}(F).$

This clearly implies the usual formulation of $\DNR$ and the universal properties of the standard enumeration show that this statement is equivalent. The reason why $\DNR$ is so handy is that it is a non-trivial consequence of $\WKL$ which is easily accessible to methods from computability theory. To see that $\DNR$ follows from $\WKL,$ consider the strengthened version $\DNR_2$:

For every partial enumerable function $F:\N\to\set{0,1}$ there is a total function $G:\N\to\set{0,1}$ such that $F(n) \neq G(n)$ for every $n \in \operatorname{dom}(F).$

The function $G:\N\to\set{0,1}$ is as required exactly when $\bar{F}(n) = 1-G(n)$ is a total extension of $F.$

Once again, we have gained an extra parameter. Could the sequence of principles

form a strictly descending chain from $\WKL$ to $\DNR$? It turns out that these principles are all equivalent to $\WKL$ but before we see why that is, let’s consider yet another way to formulate these principles. It is easy to see that $\DNR_k$ is equivalent to:

If $A_0,\dots,A_{k-1}$ are mutually disjoint enumerable sets, then there is a total function $G:\N\to\set{0,\dots,k-1}$ such that $n \notin A_{G(n)}$ for every $n.$

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 $A_0 \cap \cdots \cap A_{k-1} = \varnothing.$ This fact was observed by Cenzer and Hinman (2008), who introduced yet another parameter to formulate the generalized separation principles $\newcommand{\Sep}{\mathsf{S}}\Sep^\ell_k$:

If $A_0,\dots,A_{k-1}$ are enumerable sets such that the intersection of any $\ell+1$ of them is empty, then there is a total function $G:\N\to\set{0,\dots,k-1}$ such that $n \notin A_{G(n)}$ for every $n.$

Cenzer and Hinman looked at these from the perspective of Medvedev degrees of $\Pi^0_1$-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 $\WKL.$ 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 $\WKL,$ 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 $\ell=1$).

Lemma ($\RCA$). For all positive integers $k$ and $\ell,$ $\Sep^{\ell^2}_{k^2}$ implies $\Sep^\ell_{k}$. In particular, $\DNR_{k^2}$ implies $\DNR_k.$

Proof. Let $A_0,\dots,A_{k-1}$ be enumerable sets such that the intersection of any $\ell+1$ of them is empty. Our goal is to find a function $F:\N\to\set{0,\dots,k-1}$ such that $n \notin A_{F(n)}$ for every $n.$

Consider the enumerable sets $B_0,\dots,B_{k^2-1}$ defined by

for $i,j \lt k.$ These sets have the property that the intersection of any $\ell^2+1$ of them is empty. It follows from $\Sep^{\ell^2}_{k^2}$ that there is a function $H:\N\to\set{0,\dots,k^2-1}$ such that $B_\ell \cap H^{-1}(\ell) = \varnothing$ for every $\ell \lt k^2.$ Define $G_0,G_1:\N^2\to\set{0,\dots,k-1}$ by the equation

Note that if $m \in A_i$ and $n \in A_j$ then either $G_0(m,n) \neq i$ or $G_1(m,n) \neq j.$ We now consider two cases.

If for every $m$ there is a $n$ such that $n \in A_{G_1(m,n)},$ then let $N:\N\to\N$ be such that $N(m) \in A_{G_1(m,N(m))}$ for every $m.$ Note that we must then have $m \notin A_{G_0(m,N(m))}$ for every $m,$ which means that $F(m) = G_0(m,N(m))$ is as required.

Otherwise, there is an $m_0$ such that $n \notin A_{G_1(m_0,n)}$ for every $n.$ In that case, $F(n) = G_1(m_0,n)$ is as required. QED

This collapses the entire array of generalized separation principles, but the final alternative in the proof requires to decide a $\Sigma^0_2$ 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 ($\RCA + \mathsf{I}\Sigma^0_2$). For all positive integers $k,$ $\ell$ and $m,$ $\Sep^{\ell^m}_{k^m}$ implies $\Sep^\ell_{k}.$ In particular, $\DNR_{k^m}$ implies $\DNR_k$.

Proof. We proceed as in the previous proof, except that the sets $B_0,\dots,B_{k^m-1}$ are now defined by

for all $i_0,i_1,\dots,i_{m-1} \lt k.$ These enumerable sets again have the property that the intersection of any $\ell^m+1$ of them is empty, so it follows from $\Sep^{\ell^m}_{k^m}$ that there is a function $H:\N\to\set{0,\dots,k^m-1}$ such that $n \notin B_{H(n)}$ for every $n.$ Again, define $G_0,\dots,G_{m-1}:\N^m\to\N$ by

(Note that since $m$ could be non-standard, all $m$-tuples are understood to be coded $m$-tuples but we will not be too fussy about proper notation.)

By $\mathsf{I}\Sigma^0_2,$ we can find the largest index $j \lt m$ for which there is some sequence $\seq{n_0,\dots,n_{j-1}}$ such that

holds for all choices of $n_j,\dots,n_{m-1}.$ It follows that for every choice of $n$ we can find some sequence $\seq{n_{j+1},\dots,n_{m-1}}$ such that

Thus, the function $F:\N\to\set{0,\dots,k-1}$ defined by

for the first sequence $\seq{n_{j+1},\dots,n_{m-1}}$ as above is necessarily such that $n \notin A_{F(n)}$ for all $n.$ QED

So, assuming $\mathsf{I}\Sigma^0_2,$ we can walk backwards along the bottom row of the array even by a non-standard number of steps. Now $\Sep^1_k$ (or $\DNR_k$) does not make sense as a stand-alone principle when $k$ is nonstandard, but the limiting principle $(\exists k)\Sep^1_k$ (equivalently $(\exists k)\DNR_k$) does make sense and it does allow for the witness $k$ to be non-standard.

Proposition ($\RCA + \mathsf{I}\Sigma^0_2$). $(\exists k)\DNR_k$ is equivalent to the weak König lemma.

While $\mathsf{I}\Sigma^0_2$ 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 $\mathsf{I}\Sigma^0_2$ necessary for the last proposition?

Perhaps there is another argument that only uses $\mathsf{I}\Sigma^0_1$ or $\mathsf{B}\Sigma^0_2$? 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…

References

1. D. Cenzer, P. G. Hinman, 2008: Degrees of difficulty of generalized r.e. separating classes, Arch. Math. Logic 46, no. 7–8, 629–647.

   • mr: 2395562

   • zbl: 1151.03020

   • doi: 10.1007/s00153-007-0058-y

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

   • mr: 1034562

   • zbl: 0694.03027

   • isbn: 9780444705204

   • doi: 10.1016/S0049-237X(08)70045-4

3. I. Neeman, 2011: Necessary use of $\Sigma^1_1$ induction in a reversal, J. Symbolic Logic 76, no. 2, 561–574.

   • mr: 2830416

   • zbl: 1218.03005

   • doi: 10.2178/jsl/1305810764

Originally posted on February 26, 2012, by François G. Dorais. To the extent possible under law, François G. Dorais has waived all copyright and neigboring rights to this work.

Comments

• François G. Dorais wrote on February 26, 2012, at 20:05

  Paul Shafer kindly pointed out that Steve Simpson had already asked in 2001 whether $(\exists k)\mathsf{DNR}_k$ is equivalent to the weak König lemma over $\mathsf{RCA}_0$. (See these slides.)

  ---

• Carl Mummert wrote on March 1, 2012, at 13:31

  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 $\Sigma^0_1$). 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 on March 1, 2012, at 13:44

  Another classic example of necessary induction in a reversal is that $\mathsf{ACA}_0$ is equivalent to $\mathsf{ACA}_0'$ in the real world and also equivalent over $\mathsf{RCA}_0$ plus $\Sigma^1_1$ induction, but not over $\mathsf{RCA}_0$ 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.

  ---

• François G. Dorais replied to Carl Mummert on March 2, 2012, at 02:04

  All the ones I’m aware of are for $\Sigma^1_1$ induction. Are you aware of any for something like $\Sigma^0_2$ induction?

  ---

• Carl Mummert replied to François G. Dorais on March 2, 2012, at 14:49

  There is an example in “The Atomic Model Theorem and Type Omitting” by Hirschfeldt, Shore, and Slaman. They showed that the two principles $\Pi^0_1-G$ and AMT are not equivalent over $\mathsf{RCA}_0$ but they are equivalent over $\mathsf{RCA}_0$ plus $\Sigma^0_2$ induction. This is described in their paper in the prose below Corollary 4.5.

  ---

• François G. Dorais wrote on February 23, 2013, at 17:15

  Edits: Fixed small typos. Reformatted references.

  ---