View source for Phillips curve

{{Other uses|König's theorem (disambiguation)}}

'''König's lemma''' or '''König's infinity lemma''' is a [[theorem]] in [[graph theory]] due to {{harvs|first=Dénes|last=Kőnig|authorlink=Dénes Kőnig|year=1936|txt}}.<ref>Note that, although Kőnig's name is properly spelled with a [[double acute accent]], the lemma named after him is customarily spelled with an umlaut.</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==
If ''G'' is a [[connected graph]] with [[Infinity|infinitely]] many vertices such that every vertex has finite degree (that is, each vertex is adjacent to only finitely many other vertices) then ''G'' contains an infinitely long [[path (graph theory)|simple path]], that is, a path with no repeated vertices.

A common special case of this is that every [[tree (graph theory)|tree]] that contains infinitely many vertices, each having finite degree, has at least one infinite simple path.

Note that the vertex degrees must be finite, but need not be uniformly bounded: it is possible to have one vertex of degree 10, another of degree 100, a third of degree 1000, and so on.

===Proof===

For the proof, assume that the graph consists of infinitely many vertices <math>v_i</math> and is connected.

Start with any vertex ''v''<sub>1</sub>. Every one of the infinitely many vertices of ''G'' can be reached from ''v''<sub>1</sub> with a simple path,  and each such path must start with one of the finitely many vertices adjacent to ''v''<sub>1</sub>. There must be one of those adjacent vertices through which infinitely many vertices can be reached without going through ''v''<sub>1</sub>.   If there were not, then the entire graph would be the union of finitely many finite sets, and thus finite, contradicting the assumption that the graph is infinite. We may thus pick one of these vertices and call it ''v''<sub>2</sub>.

Now infinitely many vertices of ''G'' can be reached from ''v''<sub>2</sub> with a simple path which doesn't use the vertex ''v''<sub>1</sub>. Each such path must start with one of the finitely many vertices adjacent to ''v''<sub>2</sub>. So an argument similar to the one above shows that there must be one of those adjacent vertices through which infinitely many vertices can be reached; pick one and call it ''v''<sub>3</sub>.

Continuing in this fashion, an infinite simple path can be constructed by [[mathematical induction]].  At each step, the induction hypothesis states that there are infinitely many nodes reachable by a simple path from a particular node <math>v_i</math> that does not go through one of a finite set of vertices.  The induction argument is that one of the vertices adjacent to <math>v_i</math> satisfies the induction hypothesis, even when <math>v_i</math> is added to the finite set.

The result of this induction argument is that for all ''n'' it is possible to choose a vertex ''v''<sub>''n''</sub> as the construction describes. The set of vertices chosen in the construction is then a chain in the graph, because each one was chosen to be adjacent to the previous one, and the construction guarantees that the same vertex is never chosen twice.

This proof 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.  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]].

==Computability aspects==
The computability aspects of König's lemma have been thoroughly investigated.  The form of König's lemma most convenient for this purpose is the one which states 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 and <math>\omega^{<\omega}\,</math> the canonical tree of all finite sequences of natural numbers, ordered by extension.  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 subtree must have such a path.

For any subtree ''T'' of <math>\omega^{<\omega}\,</math> the notation Ext(''T'') denotes the set of nodes of ''T'' through which there is an infinite path.  Even when ''T'' is computable the set Ext(''T'') may not be computable.  Every subtree ''T'' of
<math>\omega^{<\omega}\,</math> that has a path has a path computable from Ext(''T'').

It is known that there are 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 Ext(''T'') is always <math>\Sigma^1_1</math> (see [[analytical hierarchy]]) when ''T'' 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 ''f'' from <math>\omega</math> to <math>\omega</math> such that for all ''n'' there is no sequence in the tree whose ''n''th element is larger than ''f(n)''.  Thus ''f'' 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 ''X'' of <math>\omega</math> the tree has a path that does not compute&nbsp;''X''.

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 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 ''N'' 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.

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 ''R'' such that for each ''x'' there are only finitely many ''z'' such that ''xRz''.  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.<ref>{{harvtxt|Truss|1976}}, p. 273; 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.

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

==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 = 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 = 37–85
 | publisher = Elsevier
 | title = Handbook of Computability Theory
 | year = 1999}}.
*{{citation
 | last = König | first = D. | authorlink = 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}}.
*{{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 = 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 = 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. | authorlink = 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}}.
*{{citation
 | last = Truss | first = J.
 | 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
 | year = 1976}}.

==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]]
[[Category:Articles containing proofs]]
[[Category:Computability theory]]
[[Category:Wellfoundedness]]
[[Category:Axiom of choice]]
[[Category:Graph theory]]
[[Category:Infinite graphs]]
[[Category:Constructivism (mathematics)]]