The low basis theorem is one of several
basis theorems in computability theory, each of which showing that, given an infinite subtree of the binary tree
, it is possible to find an infinite path through the tree with particular computability properties. The low basis theorem, in particular, shows that there must be a path which is
low; that is, the
Turing jump
In computability theory, the Turing jump or Turing jump operator, named for Alan Turing, is an operation that assigns to each decision problem a successively harder decision problem with the property that is not decidable by an oracle machine w ...
of the path is Turing equivalent to the
halting problem
In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a ...
.
Statement and proof
The low basis theorem states that every nonempty
class in
(see
arithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
) contains a set of
low degree (Soare 1987:109). This is equivalent, by definition, to the statement that each infinite computable subtree of the binary tree
has an infinite path of low degree.
The proof uses the method of forcing with
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
.
The forcing argument can also be formulated explicitly as follows. For a set ''X''⊆ω, let ''f''(''X'') = Σ
(''X'')↓2
−''i'', where (''X'')↓ means that Turing machine ''i'' halts on ''X'' (with the sum being over all such ''i''). Then, for every nonempty (lightface)
''S''⊆2
ω, the (unique) ''X''∈''S'' minimizing ''f''(''X'') has a low Turing degree. To see this, (''X'')↓ ⇔ ∀''Y''∈''S'' ((''Y'')↓ ∨ ∃''j''<''i'' ((''Y'')↓ ∧ ¬(''X'')↓)), which can be computed from 0′ by induction on ''i''; note that ∀''Y''∈''S'' φ(''Y'') is
for
φ. In other words, whether a machine halts on ''X'' is ''forced'' by a finite condition, with allows for ''X''′ = 0′.
Application
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
PA degrees strictly below
.
References
*
* .
*
* The original publication, including additional clarifying prose.
* Theorem 1.8.37.
*
Computability theory
{{Mathlogic-stub