König's lemma
Encyclopedia
König's lemma or König's infinity lemma is a theorem
in graph theory
due to Dénes Kőnig
(1936). 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 computability theory
. This theorem also has important roles in constructive mathematics and proof theory
.
, that is, a path with no repeated vertices.
A common special case of this is that every 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 bounded: it is possible to have one vertex of degree 10, another of degree 100, a third of degree 1000, and so on.
and is connected.
Start with any vertex v1. Every one of the infinitely many vertices of G can be reached from v1 with a simple path, and each such path must start with one of the finitely many vertices adjacent to v1. There must be one of those adjacent vertices through which infinitely many vertices can be reached without going through v1. 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 v2.
Now infinitely many vertices of G can be reached from v2 with a simple path which doesn't use the vertex v1. Each such path must start with one of the finitely many vertices adjacent to v2. 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 v3.
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
that does not go through one of a finite set of vertices. The induction argument is that one of the vertices adjacent to 
satisfies the induction hypothesis, even when 
is added to the finite set.
The result of this induction argument is that for all n it is possible to choose a vertex vn 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 may not be considered constructive, because at each step it uses a 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.
has an infinite path. Here 
denotes the set of natural numbers and 
the canonical tree of all finite sequences of natural numbers, ordered by extension. Each finite sequence can be identified with a partial function from 
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
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 
has an infinite path, but König's lemma shows that any finitely branching subtree must have a path.
For any subtree T of
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
that has a path has a path computable from Ext(T).
It is known that there are non-finitely branching computable subtrees of
that have no arithmetical
path, and indeed no hyperarithmetical
path (Rogers 1967, p. 418ff). However, every computable subtree of
with a path must have a path computable from Kleene's O, the canonical 
complete set. This is because the set Ext(T) is always 
(see analytical hierarchy
) when T is computable.
A finer analysis has been conducted for computably bounded trees. A subtree of
is called computably bounded or recursively bounded if there is a computable function f from 
to 
such that for all n there is no sequence in the tree whose nth element is larger than f(n). Thus f gives a bound for how “wide” the tree is. The following basis theorems apply to infinite, computably bounded, computable subtrees of 
.
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 WKL0 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 WKL0, but is equivalent to the stronger subsystem ACA0.
is, from a classical point of view, the contrapositive of a form of König's lemma. A subset S of
is called a bar if any function from 
to the set 
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 
to 
has an initial segment in the bar of length no more than 
. 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
topological space
. 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 
has an infinite path.
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 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 (Truss (1976:273); compare Levy (1979, Exercise IX.2.18)). This form of the axiom of choice (and hence of König's lemma) is not provable in ZF set theory.
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
in graph theory
Graph theory
In mathematics and computer science, graph theory is the study of graphs, mathematical structures used to model pairwise relations between objects from a certain collection. A "graph" in this context refers to a collection of vertices or 'nodes' and a collection of edges that connect pairs of...
due to Dénes Kőnig
Dénes König
Dénes Kőnig was a Jewish Hungarian mathematician who worked in and wrote the first textbook on the field of graph theory....
(1936). 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
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, especially in computability theory
Recursion theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
. This theorem also has important roles in constructive mathematics and proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
.
Statement of the lemma
If G is a connected graph with 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 simple pathPath (graph theory)
In graph theory, a path in a graph is a sequence of vertices such that from each of its vertices there is an edge to the next vertex in the sequence. A path may be infinite, but a finite path always has a first vertex, called its start vertex, and a last vertex, called its end vertex. Both of them...
, that is, a path with no repeated vertices.
A common special case of this is that every tree
Tree (graph theory)
In mathematics, more specifically graph theory, a tree is an undirected graph in which any two vertices are connected by exactly one simple path. In other words, any connected graph without cycles is a 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 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 and is connected.Start with any vertex v1. Every one of the infinitely many vertices of G can be reached from v1 with a simple path, and each such path must start with one of the finitely many vertices adjacent to v1. There must be one of those adjacent vertices through which infinitely many vertices can be reached without going through v1. 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 v2.
Now infinitely many vertices of G can be reached from v2 with a simple path which doesn't use the vertex v1. Each such path must start with one of the finitely many vertices adjacent to v2. 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 v3.
Continuing in this fashion, an infinite simple path can be constructed by mathematical induction
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
. At each step, the induction hypothesis states that there are infinitely many nodes reachable by a simple path from a particular node
that does not go through one of a finite set of vertices. The induction argument is that one of the vertices adjacent to satisfies the induction hypothesis, even when is added to the finite set.The result of this induction argument is that for all n it is possible to choose a vertex vn 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 may not be considered constructive, because at each step it uses a proof by contradiction
Reductio ad absurdum
In logic, proof by contradiction is a form of proof that establishes the truth or validity of a proposition by showing that the proposition's being false would imply a 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 has an infinite path. Here denotes the set of natural numbers and the canonical tree of all finite sequences of natural numbers, ordered by extension. Each finite sequence can be identified with a partial function from 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
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 has an infinite path, but König's lemma shows that any finitely branching subtree must have a path.For any subtree T of
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 that has a path has a path computable from Ext(T). It is known that there are non-finitely branching computable subtrees of
that have no arithmeticalArithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...
path, and indeed no hyperarithmetical
Analytical hierarchy
In mathematical logic and descriptive set theory, the analytical hierarchy is a higher type analogue of the arithmetical hierarchy. It thus continues the classification of sets by the formulas that define them.-The analytical hierarchy of formulas:...
path (Rogers 1967, p. 418ff). However, every computable subtree of
with a path must have a path computable from Kleene's O, the canonical complete set. This is because the set Ext(T) is always (see analytical hierarchyAnalytical hierarchy
In mathematical logic and descriptive set theory, the analytical hierarchy is a higher type analogue of the arithmetical hierarchy. It thus continues the classification of sets by the formulas that define them.-The analytical hierarchy of formulas:...
) when T is computable.
A finer analysis has been conducted for computably bounded trees. A subtree of
is called computably bounded or recursively bounded if there is a computable function f from to such that for all n there is no sequence in the tree whose nth element is larger than f(n). Thus f gives a bound for how “wide” the tree is. The following basis theorems apply to infinite, computably bounded, computable subtrees of .
- Any such tree has a path computable from
, the canonical Turing complete set that can decide the halting problemHalting problemIn computability theory, the halting problem can be stated as follows: Given a description of a computer program, decide whether the program finishes running or continues to run forever...
. - Any such tree has a path that is lowLow (computability)In computability theory, a Turing degree [X] is low if the Turing jump [X′] is 0′, which is the least possible degree in terms of Turing reducibility for the jump of a set. Since every set is computable from its jump, any low set is computable in 0′...
. This is known as the low basis theoremLow basis theoremThe low basis theorem in computability theory states that every nonempty \Pi^0_1 class of 2^\omega contains a set of low degree. It was first proved by Carl Jockusch and Robert I. Soare in 1972.- References :...
. - 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
the tree has a path that does not compute 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 WKL0 of second-order arithmetic
Second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. It was introduced by David Hilbert and Paul Bernays in their...
. This subsystem has an important role in reverse mathematics
Reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of...
. 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 WKL0, but is equivalent to the stronger subsystem ACA0.
Relationship to constructive mathematics and compactness
The fan theorem of BrouwerLuitzen Egbertus Jan Brouwer
Luitzen Egbertus Jan Brouwer FRS , usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, a graduate of the University of Amsterdam, who worked in topology, set theory, measure theory and complex analysis.-Biography:Early in his career,...
is, from a classical point of view, the contrapositive of a form of König's lemma. A subset S of
is called a bar if any function from to the set 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 to has an initial segment in the bar of length no more than . 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
Compact space
In mathematics, specifically general topology and metric topology, a compact space is an abstract mathematical space whose topology has the compactness property, which has many important implications not valid in general spaces...
topological space
. 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 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 ZF set theory
Zermelo–Fraenkel set theory
In mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...
(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 (Truss (1976:273); compare Levy (1979, Exercise IX.2.18)). This form of the axiom of choice (and hence of König's lemma) is not provable in ZF set theory.
See also
- Aronszajn treeAronszajn treeIn set theory, an Aronszajn tree is an uncountable tree with no uncountable branches and no uncountable levels. For example, every Suslin tree is an Aronszajn tree...
, for the possible existence of counterexamples when generalizing the lemma to higher cardinalities.
External links
- Stanford Encyclopedia of Philosophy: Constructive Mathematics
- The Mizar projectMizar systemThe Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referenced and used in new articles. Mizar has goals...
has completely formalized and automatically checked the proof of a version of König's lemma in the file TREES_2.