König's Lemma
Lemma
Let $G$ be an infinite graph which is connected and is locally finite.
Then every vertex lies on a path of infinite length.
Proof 1
Let $G$ be an infinite graph which is connected and is locally finite.
From Vertices in Locally Finite Graph, $G$ has an infinite number of vertices $v_1, v_2, \ldots, v_k, \ldots$, each of finite degree.
Let $\VV_k$ be the set of all vertices adjacent to $v_k$.
As $G$ is a connected graph, between $v_k$ and every other vertex of $G$ there exists at least one open path from $v_k$ to every other vertex of $G$.
Take any vertex of $G$ and call it $v_1$.
Let $\PP_1$ be the set of all paths from $v_1$.
Each element of $\PP_1$ must start with an edge joining $v_1$ to some element of $\VV_1$.
This entire paragraph is bogus. If this argument worked, then the theorem would be all but proven by the end of it. My view is that this proof probably cannot be salvaged, and it should be deleted. Proof 2 can probably be fixed up (not sure), and I'm working on a Proof 3.
You can help ProofWiki by reviewing it, and either correcting it or adding some explanatory material as to why you believe it is actually correct after all.
To discuss this point in more detail, feel free to use the talk page.
If you are able to resolve this, then when you have done so you can remove this instance of {{Mistake}} from the code.
If you would welcome a second opinion as to whether your explanation is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
There must be some $v_r \in \VV_1$ such that there is an infinite path from $v_r$ in $G$ which does not pass through $v_1$. Otherwise, every path from $v_1$ would be finite, and since there is a path from $v_1$ to each other vertex of the graph, all vertices are contained within one of these finite paths. There are a finite number of paths from $v_1$, so all vertices of $G$ are contained within a finite set of finite sets, contradicting the assumption that $G$ is infinite.
The statement: "There are a finite number of paths from $v_1$" has been described as "not generally true in its context"
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by resolving the issues.
To discuss this proof in more detail, feel free to use the talk page.
If you are able to fix this page, then when you have done so you can remove this instance of {{Questionable}} from the code.
If you would welcome a second opinion as to whether your correction is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
By the axiom of dependent choice, we may pick one of the vertices of $V_1$ such that there exists an infinite path through it that does not include $v_1$, and call this $v_2$.
Each such infinite path must start with one of the elements of $\VV_2$.
Repeating the above argument shows that there is some $v_s \in \VV_2$ such that there is an infinite path from $v_s$ in $G$ which does not pass through $v_2$.
Thus we can construct by induction an infinite path.
The induction hypothesis states that there are infinitely many vertices which can be reached by a path from a particular vertex $v_i$ that does not go through one of a finite set of vertices.
The induction argument is that one of the vertices adjacent to $v_i$ satisfies the induction hypothesis, even when $v_i$ is added to the finite set.
The result of this induction argument is that for all $n$ we can choose a vertex $v_n$ as per the construction.
The set of vertices chosen in the construction is then a path, because each one was chosen to be adjacent to the previous one, and the construction guarantees that the same vertex is never chosen twice.
$\blacksquare$
Proof 2
Let $G$ be an infinite graph which is both connected and locally finite.
From Vertices in Locally Finite Graph, $G$ has an infinite number of vertices each of finite degree.
Let $v$ be a vertex of $G$.
Let $T$ be the set of all finite open paths that start at $v$.
This defines an ordering, but we don't want an ordering—we want an edge set. This is easily fixed by limiting the relation to pairs of paths that differ only by one arc.
You can help ProofWiki by reviewing it, and either correcting it or adding some explanatory material as to why you believe it is actually correct after all.
To discuss this point in more detail, feel free to use the talk page.
If you are able to resolve this, then when you have done so you can remove this instance of {{Mistake}} from the code.
If you would welcome a second opinion as to whether your explanation is correct, add a call to {{Proofread}} the page (see the proofread template for usage).
Define the ordering $\preccurlyeq$ on $T$ as follows:
Let $\tuple {v_0, e_0, v_1, e_1, \ldots, v_m} \preccurlyeq \tuple {v'_0, e'_0, v'_1, e'_1, \ldots, v'_n}$ if and only if:
- $m \le n$
and:
- $\forall i < m: \tuple {v'_i, e'_i, v'_{i + 1} } = \tuple {v_i, e_i, v_{i + 1} }$
Observe that $T$ is a tree.
Why is $T$ a tree? // $T$ will be a tree because there is only one way to build any given path up from the $0$-length path.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
For each vertex $x$, let $\map E x$ be the set of all edges incident on $x$.
$\map E x$ is finite because $G$ is locally finite by definition.
For every $\tuple {v_0, e_0, v_1, e_1, \ldots, v_{n + 1} } \in T$ we have that $e_n \in \map E {v_n}$.
It follows that $T$ is finitely branching.
By definition of connectedness, to every vertex $x$ there is a walk $w$ from $v$.
A walk between any two vertices can be trimmed down to form a path.
Until this has been finished, please leave {{refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
Suppose $w = \tuple {v_0, e_0, v_1, e_1, \ldots, v_n}$ contains a cycle $\tuple {v_i, e_i, v_{i + 1}, \ldots, v_j}$ where $v_i = v_j$.
Then we can delete $\tuple {e_i, v_{i + 1}, \ldots, v_j}$ from $w$ to get a shorter walk from $v$ to $x$.
Repeatedly deleting cycles until none remain, we obtain an open path from $v$ to $x$.
What if there were an infinite number of cycles? Can we be justified in performing the above step an infinite number of times? Even worse, what if this number were uncountable?? // A walk from one vertex to another must be finite, so it can have only finitely many cycles.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
There exist an infinite number of points in $G$, as, by definition of locally finite, $G$ is itself infinite.
We have just demonstrated that for each $x \in G$ there exists an open path from $v$ to $x$.
Hence $T$, the set of finite paths that start at $v$, is infinite.
By Kőnig's tree lemma, $T$ has an infinite branch $B$.
The union $\bigcup B$ is then an infinite path in $G$ that contains $v$.
That last statement: what does the "union of a branch" mean? // Each vertex of $B$ is an open path in $G$. Each vertex of $B$ extends the path of the previous vertex, so you can take a sort of union along it. Yes, that will certainly have to be described in detail.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
$\blacksquare$
Proof 3
By Locally Finite Connected Graph is Countable, $G$ has countably many vertices.
Thus the result holds by König's Lemma: Countable.
$\blacksquare$
Axiom:Axiom of Countable Choice for Finite Sets
This theorem depends on Axiom:Axiom of Countable Choice for Finite Sets.
Although not as strong as the Axiom of Choice, Axiom:Axiom of Countable Choice for Finite Sets is similarly independent of the Zermelo-Fraenkel axioms.
As such, mathematicians are generally convinced of its truth and believe that it should be generally accepted.
Note
Extract this note into its own page.
Until this has been finished, please leave {{refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
If the graph $G$ is assumed to be countably infinite, then the result will hold in pure Zermelo-Fraenkel set theory without any choice.
Source of Name
This entry was named for Dénes Kőnig.
Linguistic Note
In the conventional naming of König's Lemma, the diacritics on the ö in the König of König's Lemma and on the ő of Dénes Kőnig do not match.
While this is irritatingly confusing, unfortunately, it is how it is.