Low basis theorem

<h2 id="statement-and-proof">Statement and proof</h2>
The low basis theorem states that every nonempty <a href="/facts/%25CE%25A001_class/spvSfILw">
 
 
 
 
 Π
 
 1
 
 
 0
 
 
 
 
 {\displaystyle \Pi _{1}^{0}}
 
 class</a> in 
 
 
 
 
 2
 
 ω
 
 
 
 
 {\displaystyle 2^{\omega }}
 
 (see <a href="/facts/Arithmetical_hierarchy/rQptcBFK">arithmetical hierarchy</a>) contains a set of <a href="/facts/Low_(computability)/cqkqcyrb">low degree</a> (Soare 1987:109). This is equivalent, by definition, to the statement that each infinite computable subtree of the binary tree 
 
 
 
 
 2
 
 <
 ω
 
 
 
 
 {\displaystyle 2^{<\omega }}
 
 has an infinite path of low degree.
The proof uses the method of forcing with 
 
 
 
 
 Π
 
 1
 
 
 0
 
 
 
 
 {\displaystyle \Pi _{1}^{0}}
 
 classes (Cooper 2004:330). Hájek and Kučera (1989) showed that the low basis is provable in the formal system of arithmetic known as 
 
 
 
 
 I-
 
 
 Σ
 
 1
 
 
 
 
 {\displaystyle {\text{I-}}\Sigma _{1}}
 
.
The forcing argument can also be formulated explicitly as follows. For a set X⊆ω, let f(X) = Σ{i}(X)↓2−i, where {i}(X)↓ means that Turing machine i halts on X (with the sum being over all such i). Then, for every nonempty (lightface) 
 
 
 
 
 Π
 
 1
 
 
 0
 
 
 
 
 {\displaystyle \Pi _{1}^{0}}
 
 S⊆2ω, the (unique) X∈S minimizing f(X) has a low Turing degree. This is because X satisfies {i}(X)↓ ⇔ ∀Y∈S ({i}(Y)↓ ∨ ∃j<i ({j}(Y)↓ ∧ ¬{j}(X)↓)), so the function i ↦ {i}(X)↓ can be computed from 
 
 
 
 
 ∅
 ′
 
 
 
 {\displaystyle \emptyset '}
 
 by induction on i; note that ∀Y∈S φ(Y) is 
 
 
 
 
 Σ
 
 1
 
 
 0
 
 
 
 
 {\displaystyle \Sigma _{1}^{0}}
 
 for any 
 
 
 
 
 Σ
 
 1
 
 
 0
 
 
 
 
 {\displaystyle \Sigma _{1}^{0}}
 
 set φ. In other words, whether a machine halts on X is forced by a finite condition, which allows for X′ = 
 
 
 
 
 ∅
 ′
 
 
 
 {\displaystyle \emptyset '}
 
.

<h2 id="application">Application</h2>
One application of the low basis theorem is to construct completions of effective theories so that the completions have low Turing degree. For example, the low basis theorem implies the existence of <a href="/facts/PA_degree/uTM36Y1l">PA degrees</a> strictly below 
 
 
 
 
 ∅
 ′
 
 
 
 {\displaystyle \emptyset '}
 
.

<ul><li>Cenzer, Douglas (1999). <a href="https://books.google.com/books?id=KqeXZ4pPd5QC&pg=PA54">"
 
 
 
 
 Π
 
 1
 
 
 0
 
 
 
 
 {\displaystyle \Pi _{1}^{0}}
 
 classes in computability theory"</a>. In Griffor, Edward R. (ed.). <a href="https://archive.org/details/handbookofcomput0140unse/page/37">Handbook of computability theory</a>. Stud. Logic Found. Math. Vol. 140. North-Holland. pp. <a href="https://archive.org/details/handbookofcomput0140unse/page/37">37–85</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 0-444-89882-4. <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1720779">1720779</a>. <a href="/facts/Zbl_(identifier)/P6rFxKKx">Zbl</a> <a href="https://zbmath.org/?format=complete&q=an:0939.03047">0939.03047</a>.</li>
<li><a href="/facts/S._Barry_Cooper/5cm2x9tR">Cooper, S. Barry</a> (2004). Computability Theory. Chapman and Hall/CRC. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 1-58488-237-9..</li>
<li>Hájek, Petr; Kučera, Antonín (1989). "On Recursion Theory in IΣ1". Journal of Symbolic Logic. 54 (2): 576–589. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.2307%2F2274871">10.2307/2274871</a>. <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/2274871">2274871</a>. <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:118808365">118808365</a>.</li>
<li>Jockusch, Carl G. Jr.; Soare, Robert I. (1972). <a href="https://doi.org/10.1090%2Fs0002-9947-1972-0316227-0">"Π(0, 1) Classes and Degrees of Theories"</a>. Transactions of the American Mathematical Society. 173: 33–56. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1090%2Fs0002-9947-1972-0316227-0">10.1090/s0002-9947-1972-0316227-0</a>. <a href="/facts/ISSN_(identifier)/DPAflDvU">ISSN</a> <a href="https://search.worldcat.org/issn/0002-9947">0002-9947</a>. <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/1996261">1996261</a>. <a href="/facts/Zbl_(identifier)/P6rFxKKx">Zbl</a> <a href="https://zbmath.org/?format=complete&q=an:0262.02041">0262.02041</a>. The original publication, including additional clarifying prose.</li>
<li>Nies, André (2009). Computability and randomness. Oxford Logic Guides. Vol. 51. Oxford: Oxford University Press. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-0-19-923076-1. <a href="/facts/Zbl_(identifier)/P6rFxKKx">Zbl</a> <a href="https://zbmath.org/?format=complete&q=an:1169.03034">1169.03034</a>. Theorem 1.8.37.</li>
<li>Soare, Robert I. (1987). Recursively enumerable sets and degrees. A study of computable functions and computably generated sets. Perspectives in Mathematical Logic. Berlin: <a href="/facts/Springer-Verlag/nAesf6nT">Springer-Verlag</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 3-540-15299-7. <a href="/facts/Zbl_(identifier)/P6rFxKKx">Zbl</a> <a href="https://zbmath.org/?format=complete&q=an:0667.03030">0667.03030</a>.</li></ul>

Low basis theorem open-in-new

Low basis theorem