Who first proved there's an $\omega$-model of $\mathsf{WKL}_0$ in which all sets are low?

Question

I am trying to pin down: who first proved that $\mathsf{WKL}_0$ has an $\omega$-model in which every set is of low degree? As shown in Simpson's Subsystems of Second Order Arithmetic (Theorem IX.2.17), one doesn't have to travel too far to get to this result when starting from the low basis theorem of Jockusch and Soare. But Simpson's typically extensive bibliographic remarks on the section in which this result is proved offer no indication of when this fact about $\mathsf{WKL}_0$ was first noted. Thanks.

Answer 1

The general issue here is that there are some results in Reverse Mathematics that are very little besides rephrased computability theory results. In such cases, it is common for nobody to take credit for the Reverse Mathematics result.

Another example of this is the theorem that $\mathsf{RT}^3_2$ implies $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$. Jockusch's paper on Ramsey theory (from 1972) is phrased only in terms of computability and predates the definitions of Reverse Mathematics. So there is no canonical source for the Reverse Mathematics result about $\mathsf{RT}^3_2$, although it would have been obvious to anyone who knew the definitions and Josckush's paper.

Friedman's theorem 1.3 from his 1974 paper "Some Systems of Second Order Arithmetic and Their Use" is certainly enough, with the common knowledge about Scott systems at the time, for someone from that era to prove the existence of a low $\omega$-model of $\mathsf{WKL}_0$. The low basis theorem was published by Jockusch and Soare in 1972. But Friedman seems to have had something else in mind, because in his comments after the theorem he refers to a "$\Delta^0_2$-complete" completion of PA rather than a low completion of PA.

The existence of low $\omega$-models of $\mathsf{WKL}_0$ is also closely related (in my mind at least) to the density of the PA-over relation. Recall $C \ll B$ ("$B$ is PA over $C$") if $B$ computes a path through each infinite subtree of $2^{<\omega}$ that is computable from $C$ (this is equivalent to: $B$ computes a completion of PA with $C$ as an additional predicate). Simpson states in his article in the Handbook of Mathematical Logic (1978) that if $C \ll B$ there is a $D$ with $C \ll D \ll B$. This also immediately gives an $\omega$-model of $\mathsf{WKL}_0$ where every set is low: let $0 \ll B$ where $B$ is low, make a sequence $0 \ll C_1 \ll C_2 \ll \cdots \ll B$, and let $M = \{ X : (\exists i)[X \leq_T C_i]\}$. I have no idea exactly when in the 1970s Simpson proved that density result.