Kőnig's lemma

This theorem also has important roles in constructive mathematics and proof theory.

be a connected, locally finite, infinite graph.

To begin this process, start with any single vertex

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.

The union of all of these paths is the ray whose existence was promised by the lemma.

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

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

to itself, and each infinite path can be identified with a total function.

There exist non-finitely branching computable subtrees of

A finer analysis has been conducted for computably bounded trees.

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.

The full form of Kőnig's lemma is not provable in WKL0, but is equivalent to the stronger subsystem ACA0.

The proof given above is not generally considered to be 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, and because of the reliance on a weak form of the axiom of choice.

The fan theorem of L. E. J. Brouwer (1927) is, from a classical point of view, the contrapositive of a form of Kőnig's lemma.

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.

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

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.

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

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.

[3] This form of the axiom of choice (and hence of Kőnig's lemma) is not provable in ZF set theory.

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.