Kőnig's lemma
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. 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. Statement of the lemma. Let "G" be a connected, locally finite, infinite graph (this means: any two vertices can be connected by a path, the  graph has infinitely many vertices, and each vertex is adjacent to only finitely many other vertices). Then "G" contains a ray: a simple path (a path with no repeated vertices) that starts at one vertex and continues from it through infinitely many vertices. A common special case of this is that every infinite tree contains either a vertex of infinite degree or an infinite simple path. Proof. Start with any vertex "v". Every one of the infinitely many vertices of "G" can be reached from "v" with a simple path, and each such path must start with one of the  finitely many vertices adjacent to "v". There must be one of those adjacent vertices through which infinitely many vertices can be reached without going through "v". 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". Now infinitely many vertices of "G" can be reached from "v" with a simple path which does not include the vertex "v". Each such path must start with one of the finitely many vertices  adjacent to "v". 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". Continuing in this fashion, an infinite simple path can be constructed using mathematical induction and a weak version of the axiom of dependent choice. At each step, the induction hypothesis states that there are infinitely many nodes reachable by a simple path from a particular node "v" that does not go through one of a finite set of vertices. The induction argument is that one  of the vertices adjacent to "v" satisfies the induction hypothesis, even when "v" 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" 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. 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 formula_1 has an infinite path. Here formula_2 denotes the set of natural numbers (thought of as an ordinal number) and formula_1 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 formula_2 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 formula_1 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 formula_1 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 formula_1 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 formula_1 that has a path  has a path computable from Ext("T"). It is known that there are non-finitely branching computable subtrees of formula_1 that have no arithmetical path, and indeed no hyperarithmetical path. However, every computable subtree of formula_1 with a path must have a path computable from Kleene's O, the canonical formula_11 complete set. This is because the set Ext("T") is always formula_12 (see analytical hierarchy) when "T" is computable. A finer analysis has been conducted for computably bounded trees. A subtree of formula_1 is called computably bounded or recursively bounded if there is a computable function "f" from formula_2 to formula_2  such that for every sequence in the tree and every "n", the "n"th element of the sequence is at most "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 formula_16. 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 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, but is equivalent to the stronger subsystem ACA. Relationship to constructive mathematics and compactness. 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. 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 is, from a classical point of view, the contrapositive of a form of Kőnig's lemma. A subset "S" of formula_19 is called a "bar" if any function from formula_2 to the set formula_21 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 formula_2 to formula_21 has an initial segment in the bar of length no more than formula_24. 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 formula_25. 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 formula_26 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 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, that is to say, the axiom of countable choice for finite sets. 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.