Low basis theorem
The low basis theorem is one of several basis theorems in computability theory, each of which show 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 of the path is Turing equivalent to the halting problem.
Statement and proof
The low basis theorem states that every nonempty class in contains a set of low degree. 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. Hájek and Kučera 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 = Σ↓2−i, where ↓ means that Turing machine i halts on X. Then, for every nonempty S⊆2ω, the X∈''S minimizing f'' has a low Turing degree. This is because X satisfies ↓ ⇔ ∀Y∈''S ↓ ∨ ∃j''<i ↓ ∧ ¬), so the function i ↦ ↓ can be computed from by induction on i; note that ∀Y∈''S φ is for any set φ. In other words, whether a machine halts on X'' is forced by a finite condition, which allows for X′ =.