Editing Kőnig's lemma

{{Short description|Mathematical result on infinite trees}}
{{Other uses|König's theorem (disambiguation)}}
{{more footnotes|date=February 2021}}
[[File:Denes König - Über eine Schlussweise aus dem Endlichen ins Unendliche.png|thumb|Kőnig's 1927 publication]]
'''Kőnig's lemma''' or '''Kőnig's infinity lemma''' is a [[theorem]] in [[graph theory]] due to the Hungarian mathematician [[Dénes Kőnig]] who published it in 1927.<ref>{{harvtxt|Kőnig|1927}} as explained in {{harvtxt|Franchella|1997}}</ref> It gives a sufficient condition for an infinite graph to have an infinitely long path. The computability aspects of this theorem have been thoroughly investigated by researchers in [[mathematical logic]], especially in [[recursion theory|computability theory]]. This theorem also has important roles in [[constructive mathematics]] and [[proof theory]].

==Statement of the lemma==
Let <math>G</math> be a [[connected graph|connected]], [[Glossary of graph theory terms#finite|locally finite]], [[Glossary of graph theory terms#finite|infinite graph]]. This means that every two vertices can be connected by a finite path, each vertex is adjacent to only finitely many other vertices, and the graph has infinitely many vertices. Then <math>G</math> contains a [[Ray (graph theory)|ray]]: a [[path (graph theory)|simple path]] (a path with no repeated vertices) that starts at one vertex and continues from it through infinitely many vertices. Another way of stating the theorem is: "If the human race never dies out, somebody now living has a line of descendants that will never die out".<ref>{{harvtxt|Knuth|1968}}, p.&nbsp;382</ref>

A useful special case of the lemma is that every infinite [[tree (graph theory)|tree]] contains either a vertex of infinite [[degree (graph theory)|degree]] or an infinite simple path. If it is locally finite, it meets the conditions of the lemma and has a ray, and if it is not locally finite then it has an infinite-degree vertex.

===Construction===
The construction of a ray, in a graph <math>G</math> that meets the conditions of the lemma, can be performed step by step, maintaining at each step a finite path that can be extended to reach infinitely many vertices (not necessarily all along the same path as each other). To begin this process, start with any single vertex <math>v_1</math>. This vertex can be thought of as a path of length zero, consisting of one vertex and no edges. By the assumptions of the lemma, each of the infinitely many vertices of <math>G</math> can be reached by a simple path that starts from <math>v_1</math>.

Next, as long as the current path ends at some vertex <math>v_i</math>, consider the infinitely many vertices that can be reached by simple paths that extend the current path, and for each of these vertices construct a simple path to it that extends the current path. There are infinitely many of these extended paths, each of which connects from <math>v_i</math> to one of its neighbors, but <math>v_i</math> has only finitely many neighbors. Therefore, it follows by a form of the [[pigeonhole principle]] that at least one of these neighbors is used as the next step on infinitely many of these extended paths. Let <math>v_{i+1}</math> be such a neighbor, and extend the current path by one edge, the edge from <math>v_i</math> to <math>v_{i+1}</math>. This extension preserves the property that infinitely many vertices can be reached by simple paths that extend the current path.

Repeating this process for extending the path produces an infinite sequence of finite simple paths, each extending the previous path in the sequence by one more edge. The union of all of these paths is the ray whose existence was promised by the lemma.

==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>.

==Relationship to constructive mathematics and compactness==
The proof given above is not generally considered to be [[mathematical constructivism|constructive]], because at each step it uses a [[Reductio ad absurdum|proof by contradiction]] to establish that there exists an adjacent vertex from which infinitely many other vertices can be reached, and because of the reliance on a weak form of the [[axiom of choice]]. Facts about the computational aspects of the lemma suggest that no proof can be given that would be considered constructive by the main schools of [[constructive mathematics]].

The fan theorem of {{harvs|first=L. E. J.|last=Brouwer|authorlink=Luitzen Egbertus Jan Brouwer|year=1927|txt}} is, from a classical point of view, the [[contrapositive]] of a form of Kőnig's lemma. A subset ''S'' of <math>\{0,1\}^{<\omega}</math> is called a ''bar'' if any function from <math>\omega</math> to the set <math>\{0,1\}</math> has some initial segment in ''S''. A bar is ''detachable'' if every sequence is either in the bar or not in the bar (this assumption is required because the theorem is ordinarily considered in situations where the [[law of the excluded middle]] is not assumed). A bar is ''uniform'' if there is some number <math>N</math> so that any function from <math>\omega</math> to <math>\{0,1\}</math> has an initial segment in the bar of length no more than <math>N</math>. Brouwer's fan theorem says that any detachable bar is uniform.

This can be proven in a classical setting by considering the bar as an open covering of the [[Compact space|compact]] topological space <math>\{0,1\}^\omega</math>. Each sequence in the bar represents a basic open set of this space, and these basic open sets cover the space by assumption. By compactness, this cover has a finite subcover. The ''N'' of the fan theorem can be taken to be the length of the longest sequence whose basic open set is in the finite subcover. This topological proof can be used in classical mathematics to show that the following form of Kőnig's lemma holds: for any natural number ''k'', any infinite subtree of the tree <math>\{0,\ldots,k\}^{<\omega}</math> has an infinite path.

==Relationship with the axiom of choice==
Kőnig's lemma may be considered to be a choice principle; the first proof above illustrates the relationship between the lemma and the [[axiom of dependent choice]]. At each step of the induction, a vertex with a particular property must be selected. Although it is proved that at least one appropriate vertex exists, if there is more than one suitable vertex there may be no canonical choice. In fact, the full strength of the axiom of dependent choice is not needed; as described below, the [[axiom of countable choice]] suffices.

If the graph is countable, the vertices are well-ordered and one can canonically choose the smallest suitable vertex. In this case, Kőnig's lemma is provable in second-order arithmetic with [[arithmetical comprehension]], and, a fortiori, in [[Zermelo–Fraenkel set theory|ZF set theory]] (without choice).

Kőnig's lemma is essentially the restriction of the axiom of dependent choice to entire relations <math>R</math> such that for each <math>x</math> there are only finitely many <math>z</math> such that <math>xRz</math>. Although the axiom of choice is, in general, stronger than the principle of dependent choice, this restriction of dependent choice is equivalent to a restriction of the axiom of choice.
In particular, when the branching at each node is done on a finite subset of an arbitrary set not assumed to be countable, the form of Kőnig's lemma that says "Every infinite finitely branching tree has an infinite path" is equivalent to the principle that every countable set of finite sets has a choice function, that is to say, the axiom of countable choice for finite sets.<ref>{{harvtxt|Truss|1976}}, p.&nbsp;273; {{harvtxt|Howard|Rubin|1998}}, pp. 20, 243; compare {{harvtxt|Lévy|1979}}, Exercise IX.2.18.</ref> This form of the axiom of choice (and hence of Kőnig's lemma) is not provable in ZF set theory.

== Generalization ==
In the [[category of sets]], the [[inverse limit]] of any inverse system of non-empty finite sets is non-empty. This may be seen as a generalization of Kőnig's lemma and can be proved with [[Tychonoff's theorem]], viewing the finite sets as compact discrete spaces, and then using the [[finite intersection property]] characterization of compactness.

==See also==
* [[Aronszajn tree]], for the possible existence of counterexamples when generalizing the lemma to higher cardinalities.
* [[PA degree]]

==Notes==
{{reflist}}

==References==
*{{citation
 | last = Brouwer | first = L. E. J. | author-link = Luitzen Egbertus Jan Brouwer
 | title = On the Domains of Definition of Functions
 | year = 1927}}. published in {{citation
 | editor-last = van Heijenoort | editor-first = Jean
 | title = From Frege to Gödel
 | year = 1967}}
*{{citation
 | last = Franchella | first = Miriam
 | issue = 51(1)3:2-3
 | journal = Archive for History of Exact Sciences
 | pages = 3–27
 | title = On the origins of Dénes König's infinity lemma
 | year = 1997
 | volume = 51
 | doi=10.1007/BF00376449| s2cid = 117198918
 }}
*{{citation
 | last1 = Howard | first1 = Paul 
 | last2 = Rubin | first2 = Jean | author-link2 = Jean E. Rubin
 | title = Consequences of the Axiom of Choice
 | year = 1998
 | publisher = American Mathematical Society
 | place = Providence, RI
 | series = Mathematical Surveys and Monographs
 | volume = 59
}}
*{{citation
 | last = Kőnig
 | first = D.
 | author-link = Dénes Kőnig
 | issue = 2–3
 | journal = Acta Sci. Math. (Szeged)
 | language = German
 | pages = 121–130
 | title = Über eine Schlussweise aus dem Endlichen ins Unendliche
 | url = http://acta.fyx.hu/acta/showCustomerArticle.action?id=5131&dataObjectType=article&returnAction=showCustomerVolume&sessionDataSetId=2b29ea26fa2c9ba&style=
 | year = 1927
 | access-date = 2014-12-23
 | archive-url = https://archive.today/20141223141608/http://acta.fyx.hu/acta/showCustomerArticle.action?id=5131&dataObjectType=article&returnAction=showCustomerVolume&sessionDataSetId=2b29ea26fa2c9ba&style=
 | archive-date = 2014-12-23
 | volume = 3
 }}
*{{citation
 | last = Lévy | first = Azriel | author-link = Azriel Lévy
 | isbn = 3-540-08417-7
 | mr = 0533962
 | publisher = Springer
 | title = Basic Set Theory
 | year = 1979}}; reprint, Dover, 2002, {{isbn|0-486-42079-5}}.
*{{citation
 | last = Rogers | first = Hartley Jr. | author-link = Hartley Rogers, Jr.
 | mr = 0224462
 | publisher = McGraw-Hill
 | title = Theory of Recursive Functions and Effective Computability
 | year = 1967}}
*{{citation
 | last = Truss | first = J. | author-link = John Truss
 | editor1-last = Marek | editor1-first = V. Wiktor
 | editor2-last = Srebrny | editor2-first = Marian
 | editor3-last = Zarach | editor3-first = Andrzej
 | contribution = Some cases of König's lemma
 | doi = 10.1007/BFb0096907
 | mr = 0429557
 | pages = 273–284
 | publisher = Springer
 | series = Lecture Notes in Mathematics
 | title = Set Theory and Hierarchy Theory a Memorial Tribute to Andrzej Mostowski
 | volume = 537
 | isbn = 978-3-540-07856-2 | year = 1976}}
*{{citation|last=Knuth |first=Donald |title=Art of Computer Programming, Volume 1: Fundamental Algorithms |page=382 |year=1968 |isbn=978-0-201-03801-9 |author-link=Donald Knuth}}

==Further reading==
*{{citation
 | last = Cenzer
 | first = Douglas
 | contribution = <math>\Pi^0_1</math> classes in computability theory
 | doi = 10.1016/S0049-237X(99)80018-4
 | isbn = 0-444-89882-4
 | mr = 1720779
 | pages = [https://archive.org/details/handbookofcomput0140unse/page/37 37–85]
 | publisher = Elsevier
 | title = Handbook of Computability Theory
 | year = 1999
 | url = https://archive.org/details/handbookofcomput0140unse/page/37
 }}
*{{citation
 | last = Kőnig | first = D. | author-link = Dénes Kőnig
 | issue = 8
 | journal = Fundamenta Mathematicae
 | language = French
 | pages = 114–134
 | title = Sur les correspondances multivoques des ensembles
 | url = http://matwbn.icm.edu.pl/ksiazki/fm/fm8/fm815.pdf
 | year = 1926| volume = 8 | doi = 10.4064/fm-8-1-114-134 }}
*{{citation
 | last = Kőnig | first = D. | author-link = Dénes Kőnig
 | language = German
 | location = Leipzig
 | publisher = Akad. Verlag
 | title = Theorie der Endlichen und Unendlichen Graphen: Kombinatorische Topologie der Streckenkomplexe
 | year = 1936}}
*{{citation
 | last = Simpson | first = Stephen G.
 | isbn = 3-540-64882-8
 | mr = 1723993
 | publisher = Springer
 | series = Perspectives in Mathematical Logic
 | title = Subsystems of Second Order Arithmetic
 | year = 1999}}
*{{citation
 | last = Soare | first = Robert I. | author-link = Robert I. Soare
 | isbn = 3-540-15299-7
 | mr = 0882921
 | publisher = Springer
 | series = Perspectives in Mathematical Logic
 | title = Recursively Enumerable Sets and Degrees: A study of computable functions and computably generated sets
 | year = 1987}}

==External links==
* [http://plato.stanford.edu/entries/mathematics-constructive/ Stanford Encyclopedia of Philosophy: Constructive Mathematics]
* The [[Mizar system|Mizar project]] has completely formalized and automatically checked the proof of a version of Kőnig's lemma in the file [http://mizar.org/JFM/Vol3/trees_2.html TREES_2].

{{DEFAULTSORT:Koenigs Lemma}}
[[Category:Lemmas in graph theory]]
[[Category:Articles containing proofs]]
[[Category:Computability theory]]
[[Category:Wellfoundedness]]
[[Category:Axiom of choice]]
[[Category:Infinite graphs]]
[[Category:Constructivism (mathematics)]]