Editing Kőnig's lemma (section)

==Computability aspects==
The computability aspects of Kőnig's lemma have been thoroughly investigated. For this purpose it is convenient to state Kőnig's lemma in the form that any infinite finitely branching subtree of <math>\omega^{<\omega}</math> has an infinite path. Here <math>\omega</math> denotes the set of natural numbers (thought of as an [[ordinal number]]) and <math>\omega^{<\omega}</math> the tree whose nodes are all finite sequences of natural numbers, where the parent of a node is obtained by removing the last element from a sequence. Each finite sequence can be identified with a partial function from <math>\omega</math> to itself, and each infinite path can be identified with a total function. This allows for an analysis using the techniques of computability theory.

A subtree of <math>\omega^{<\omega}</math> in which each sequence has only finitely many immediate extensions (that is, the tree has finite degree when viewed as a graph) is called '''finitely branching'''. Not every infinite subtree of <math>\omega^{<\omega}</math> has an infinite path, but Kőnig's lemma shows that any finitely branching infinite subtree must have such a path.

For any subtree <math>T</math> of <math>\omega^{<\omega}</math> the notation <math>\operatorname{Ext}(T)</math> denotes the set of nodes of <math>T</math> through which there is an infinite path. Even when <math>T</math> is computable the set <math>\operatorname{Ext}(T)</math> may not be computable. Whenever a subtree <math>T</math> of
<math>\omega^{<\omega}</math> has an infinite path, the path is computable from <math>\operatorname{Ext}(T)</math>, step by step, greedily choosing a successor in <math>\operatorname{Ext}(T)</math> at each step. The restriction to <math>\operatorname{Ext}(T)</math> ensures that this greedy process cannot get stuck.

There exist non-finitely branching computable subtrees of <math>\omega^{<\omega}</math> that have no [[arithmetical hierarchy|arithmetical]] path, and indeed no [[analytical hierarchy|hyperarithmetical]] path.<ref>{{harvtxt|Rogers|1967}}, p.&nbsp;418ff.</ref> However, every computable subtree of <math>\omega^{<\omega}</math> with a path must have a path computable from [[Kleene's O]], the canonical <math>\Pi^1_1</math> complete set. This is because the set <math>\operatorname{Ext}(T)</math> is always <math>\Sigma^1_1</math> (for the meaning of this notation, see [[analytical hierarchy]]) when <math>T</math> is computable.

A finer analysis has been conducted for computably bounded trees. A subtree of <math>\omega^{<\omega}</math> is called '''computably bounded''' or '''recursively bounded''' if there is a computable function <math>f</math> from <math>\omega</math> to <math>\omega</math> such that for every sequence in the tree and every natural number <math>n</math>, the <math>n</math>th element of the sequence is at most <math>f(n)</math>. Thus <math>f</math> gives a bound for how "wide" the tree is. The following [[basis theorem (computability)|basis theorem]]s apply to infinite, computably bounded, computable subtrees of <math>\omega^{< \omega}</math>.
* Any such tree has a path computable from <math>0'</math>, the canonical Turing complete set that can decide the [[halting problem]].
* Any such tree has a path that is [[Low (computability)|low]]. This is known as the [[low basis theorem]].
* Any such tree has a path that is ''hyperimmune free''. This means that any function computable from the path is dominated by a computable function.
* For any noncomputable subset <math>X</math> of <math>\omega</math> the tree has a path that does not compute&nbsp;<math>X</math>.

A weak form of Kőnig's lemma which states that every infinite binary tree has an infinite branch is used to define the subsystem WKL<sub>0</sub> of [[second-order arithmetic]]. This subsystem has an important role in [[reverse mathematics]]. Here a binary tree is one in which every term of every sequence in the tree is 0 or 1, which is to say the tree is computably bounded via the constant function 2. The full form of Kőnig's lemma is not provable in WKL<sub>0</sub>, but is equivalent to the stronger subsystem ACA<sub>0</sub>.