(Long) Detailed Proof of Kőnig's Lemma (Explicit, Down to Axiom of Choice)
Solution 1:
Dependent Choice is quite significantly stronger than what is necessary to prove Kőnig's lemma. And although the "obvious proof" uses Dependent Choice, we can do with much less. Indeed, Kőnig's lemma is equivalent to the statement "Every countable family of finite sets admits a choice function".
This principle is very weak. It follows from "the countable union of finite sets is countable", which follows from "the countable union of countable sets is countable", which follows from "every countable family of sets admits a choice function", which follows from Dependent Choice. None of these implications is reversible, either.
In fact, Kőnig's lemma follows even from "every set can be linearly ordered", or "every infinite set contains a countably infinite subset".
Suppose that $G$ is a locally finite graph. We may assume that it is cycle-free, otherwise pick any cycle, and loop through it infinitely many times. Now that the graph is cycle-free, we may also assume it is connected, otherwise we can restrict to a connected component.
Fix a node, $g_0\in G$. Then we have a tree with $g_0$ being the root. Define $T_n$ to be the set of vertices for which the unique path from $g_0$ has exactly $n$ nodes. Because $G$ is cycle-free and connected, these paths are indeed unique, and every node in $G$ lies in some $T_n$.
Claim 1. For each $n$, $T_n$ is finite.
Proof. $T_0=\{g_0\}$. Suppose that $T_n$ is finite, then elements of $T_{n+1}$ are all neighbours of elements of $T_n$. But as $G$ is locally finite, $T_{n+1}$ is a subset of a finite union of finite sets, which means it is finite. $\square$
Say that a vertex $g$ in $G$ is terminal if there is some $\ell_g$ such that all paths going from $g_0$ through $g$ are at most of length $\ell_g$.
Claim 2. For each $n$, $T_n$ contains at least one node which is not terminal.
Proof. If all the nodes in $T_n$ are terminal, let $\ell = \max\{\ell_g\mid g\in T_n\}$, then $G=\bigcup_{k\leq \ell}T_k$, and so $G$ is finite. But we assumed that $G$ is infinite. $\square$
Claim 3. If $g\in T_n$ and $g$ is not terminal, then there is some $g'\in T_{n+1}$ such that $g'$ is a neighbour of $g$, and $g'$ is also not terminal.
Proof. If $g$ is connected only to terminal nodes in $T_{n+1}$, let $\ell$ be $\max\{\ell_{g'}\mid g'\in T_{n+1}\text{ and it is a neighbour of }g\}$. That means that every path from $g_0$ going through $g$ must have at most $\ell$ vertices, and so $g$ is terminal as well. $\square$
Let $T'_n$ denote the subset of $T_n$ of those nodes which are not terminal. Since $T'_n$ is finite, say with $k_n$ elements, the set $S_n=\{f\colon\{0,\dots,k_n-1\}\to T'_n\mid f\text{ is a bijection}\}$ is also finite, and non-empty. Let $F$ be a choice function from $\{S_n\mid n\in\Bbb N\}$.
Finally, define $f$ on the graph as follows: $$f(g)=\begin{cases} F(n+1)(i) & g\in T_n, i=\min\{j<k_{n+1}\mid F(j)\text{ is a neighbour of }g\},\\ g & \text{otherwise}.\end{cases}$$ That is, $f$ either "stops" if there are only terminal nodes, or picks the neighbour with the least index in the enumeration of $T'_{n+1}$, if such neighbour exists.
And now I claim that applying the recursion theorem on $f$, with $g_0$ as a starting point, will produce a ray. That is, a sequence $s$ such that $s_0 = g_0$ and $s_{n+1} = f(s_n)$.
Claim 4. The sequence $s$ is a ray.
Proof. It is enough to claim that for all $n$, $s_n$ is not a terminal node. For $n=0$ we already know that $g_0$ is not terminal. But by Claim 3, if $s_n$ is not terminal, then there is some neighbour in $T_{n+1}$ which is also not terminal, so $s_{n+1}=f(s_n)$ must be such neighbour, and in particular it is not terminal. $\square$
You can see from this proof how the various choice principles I've pointed out allow us to prove the existence of the choice function $F$.
If the countable union of finite sets is countable, then we take the union of all the $T'_n$, it is countable, so we may enumerate it, and use this enumeration to define $F$.
If every set can be linearly ordered, we may linearly order the union of the $T'_n$s, which again provides us with a uniform enumeration, as a linear ordering of a finite set is a well-ordering.
If every infinite set has a countably infinite subset, then the union of the $T'_n$s has a countably infinite subset, it follows that it must meet infinitely many $T'_n$s, but by the uniqueness of the paths, we can then create a countable subtree, and use the enumeration, again.
Finally, to obtain the countable choice for families of finite sets axiom, let $\{A_n\mid n\in\Bbb N\}$ be a family of non-empty finite sets. We define $G_n$ to be the set of choice functions from $A_k$ for $k<n$, i.e. $\prod_{k<n}A_k$, and let $G=\bigcup_{n\in\Bbb N}G_n$, with the edge relation defined as follows: $\{f,g\}$ is an edge if and only if there is some $n$ such that $\operatorname{dom} g=\{0,\dots,n\}$ and $f=g\restriction\{0,\dots,n-1\}$, or vice versa.
That is, an edge is between two functions such that the one extends the other by a single new choice. It is easy to see this is locally finite, as each $A_n$ is finite. So there is a ray, from which we define a choice function from the entire family $\{A_n\mid n\in\Bbb N\}$.
Solution 2:
The idea behind this is to work in sets and show that there is an iterative scheme (and thus, an infinite sequence) which successively generates an infinite path of $G$ that is consistent from iteration to iteration. So we'll construct a system directly and use König's Lemma to show that there is such an iterative scheme. Then we invoke DC to say that this generates an infinite sequence. I apologize in advance for not providing diagrams, but it's already enough writing this as it is - try to draw along if you can!
Let's get started. We'll restate the theorem:
In an infinite, locally finite, connected graph $G$, there exists an infinite one-way path.
Proof
Letting $G = (V,E)$ satisfy the specified conditions, we may assume without loss of generality that $G$ is simple, as multiple edges and loops have no effect on whether or not a graph is connected, and will have no effect on our approach to the problem at hand.
Showing $G$ is Countable
Pick an arbitrary vertex $v_0$ in $V$. Since $G$ is connected, there is a finite path (paths are finite by definition) from $v_0$ to every other vertex in $G$. For each vertex $w$ in $G$, let $L(w)$ be the length of the shortest path from $v_0$ to $w$ ($n = 0$ if $w = v_0$). We define $T_n = \{w \in V : L(w) = n\}$ to be the $n^{th}$ tier of $G$ with respect to $v_0$ ($n \in \mathbb{N} \cup \{0\}$), that is, $T_n$ is the set of vertices which can be reached from $v_0$ via a path of minimum length $n$. In this construction, every vertex of $G$ is assigned to a unique tier $T_n$. So the union over all $T_n$ must give us every vertex in $G$.
Since $G$ is locally finite, $T_n$ is always finite, as one can only transit to finitely many vertices from any other given vertex. Since $G$ is connected, all $T_n$ must be non-empty: if $T_n$ was empty for some $n$, then all $T_{m>n}$ would have to be empty as well, as you can't have a path of length longer than $n$ without a path of length $n$ to begin with. This would imply that there are finitely many $T_n$, and since $T_n$ is always finite, the union over all $T_n$ (which represents all vertices in $G$) yields a finite set of vertices, contradictory to our assumption that $G$ is infinite. Therefore, all tiers $T_n$ are non-empty, and there are countably many finite tiers. Since each vertex in $G$ is an element of some tier $T_n$, the countable union over all tiers gives the vertex set $V$, which must in turn be countable.
Since $G$ is locally finite, each vertex has finite degree, and so the number of edges between and within tiers $T_{n-1}$ and $T_{n}$ must be finite. We will denote $E_n$ as the set of edges in G linking two vertices in $T_{n-1} \cup T_{n}$ (taking $T_{-1}$ to be $\varnothing$). It's important to note that for each vertex in $T_n$, there is some vertex in $T_{n-1}$ joining it, since a path of length $n$ is built on a path of length $n-1$. Then by a similar argument to the one for $T_n$, we find there are countably many $E_n$, each of which are finite and non-empty (otherwise there would be no paths to the vertices in $T_{m>n}$). The uncountable union over all $E_n$ yields the edge set $E$, which then must be countable.
Since the vertex and edge sets of $G$ are both countable, $G$ is countable. $\blacksquare$
Constructing a System with an Iterative Scheme for König's Lemma
Since $G$ is countable, its vertices may be enumerated as $v_0, v_1, v_2, ...$ and we will do so, letting $v_0$ be the same vertex we arbitrarily selected above. By definition $v_0 \in T_0$, but the other vertices may be in a different tier than their vertex number (otherwise $G$ would be an infinite one-way path and the theorem is proven). However, every vertex does belong to a unique tier by construction, which we can also use further characterize the vertex. So from now on let us denote vertices by $v_k^n$, where $k$ is the vertex's index number with respect to the vertex enumeration and superscript $n$ is the tier $T_n$ it belongs to with respect to $v_0^0$ (which I will continue to call $v_0$ as an exception).
Let $G_n = \bigcup_{i=0}^n (T_i \cup E_i$) be the subgraph of $G$ induced by the vertices of tiers $1$ through $n$. Since all $T_i$ and $E_i$ are non-empty, we have $G_n \subset G_{n+1}$ for all $n$. The idea here is that we have an iteration scheme $G_0 \cup G_1 \cup\space...\space\cup G_n$ that successively iterates out G based on "minimal path distance with respect to $v_0$", i.e., the scheme iterates out all minimal paths of up to length $n$ in $G$ starting from $v_0$.
There are two important facts. The first is that to be minimal, each successive vertex in a given path must be in a successive tier, unless the path terminates before $n$ iterations (for example, if there is a vertex adjacent to $v_0$ only). Think about it: by definition, you can get to any vertex in $T_n$ from some vertex in $T_{n-1}$, so if the path has two vertices in the same tier, it violates minimality.
The second is that for all $n$, there is a finite number $\pi_n$ of minimal paths of length $n$. This follows from $G$ being locally finite, but I will construct this number in an appendix at the end of this proof, as it's already long enough. But just remember that $\pi_n$ represents the (finite) number of minimal paths of length $n$. From here on, I'll just refer to the minimal paths as "paths" for ease of reading; the "minimal" aspect will be implied.
We now define a set $p_i^n$ to represent a particular path of length $n$, where $i \leq \pi_n$ indexes the path and tells us which of those $\pi_n$ paths it is. Further, we define the path space $P_n = \bigcup_{i=1}^{\pi_n} \{p_i^n\}$ as the set of all paths of length $n$. The path space is non-empty for all $n$. We need to construct the paths though. We do this as follows:
Recall that we define the tiers by $T_n = \{w \in V : L(w) = n\}$, where $L(w)$ is the minimum path length from vertex $v_0$ to vertex $w$. It would be handy right now to be able to pick out vertices from a given tier, and we've since enumerated the vertices. Let's tweak the function $L$. Define a function $L'$ such that $L'(v_j) = v_j^n$ (a translation from our old vertex notation to our current one) if $v_j$ is in tier $T_n$.
With this, we define the tier index sets by $I_n = \{j \in \mathbb{N} \cup \{0\} : L'(v_j) = v_j^n\}$. This will let us identify which vertex is in a particular position in a particular path. To do this, we formally define the paths in $G$ as:
$p_i^n = \bigcup_{k=1}^n \{\#_{x_{ik}^n}\}$
... where $x_{ik}^n \in I_k$ is the $k^{th}$ vertex ($k \leq n$) in the $i^{th}$ path of length $n$ ($i \leq \pi_n$), and;
$\#_{x_{ik}^n} = 2^{x_{ik}^n}3^k$ is a unique number (since $2$ and $3$ are prime) given to vertex $x_{ik}^n$, which encodes the the vertex's natural index in powers of two and its tier in powers of three. So every vertex in $G$ gets a unique number based on its index and tier, and thus all paths are unique (and valid of course, by assumption). So we've got an explicit expression for paths now, and all the definitions we need to set up König's Lemma.
Identifying the Iteration Scheme
The key part of this section is using the fact that a path of length $n$ builds on top of a path of length $n-1$, which builds on a path of length $n-2$, and so on down to $v_0$, for any path. Let's take a look at $p_i^{n+1}$:
$p_i^{n+1} = \bigcup_{k=1}^{n+1} \{\#_{x_{ik}^{n+1}}\}$
If we isolate the $(n+1)^{th}$ vertex from this union, we get:
$p_i^{n+1} = \bigcup_{k=1}^{n} \{\#_{x_{ik}^{n+1}}\} \cup \{\#_{x_{i(n+1)}^{n+1}}\}$
Clearly the first term must represent a valid path of length $n$, and thus $\bigcup_{k=1}^{n} \{\#_{x_{ik}^{n+1}}\} = p_l^n \subset p_i^{n+1}$ for some $l \in \pi_n$. Since $i$ was arbitrary, we have that for any element $p_{n+1} \in P_{n+1}$ there exists an induced subpath $p_n \in P_n$ such that $p_n \subset p_{n+1}$. Here, we see that the construction represents paths as sets and subpaths as subsets of paths. This is the path iteration scheme we are looking for - iterating out a path vertex by vertex - and we are ready to use König's Lemma.
Using König's Lemma
Just a quick reminder that "minimal" is still implied when I'm talking about paths!
The condition of the lemma in this graph theoretical context is fulfilled as follows:
We have a countable set of finite path spaces (sets) $P_n$, each of which are non-empty and disjoint (since their members $p_n$ are sets of cardinality $n$). By construction, the proper subset relation $\subset$ on $\bigcup P_n$ represents "previous iteration stage" subpaths of $p_n$, and we have that for every $p_{n+1} \in P_{n+1}$ there exists an induced subpath $p_n \in P_n$ such that $p_n \subset p_{n+1}$. The iterative scheme here is "backwards", in that we are making a statement about the iteration stage prior to the current one.
König's Lemma tells us that since there are countably many non-empty $P_n$, the backward iterative scheme on $P_n$ implies that there must be an infinite forward iterative scheme (i.e. there's at least one iterable path that doesn't terminate). That is, there is some countable subset $\Pi = \bigcup \rho_n$ of $\bigcup P_n$ such that $\rho_n \in P_n$ and $\rho_n \subset \rho_{n+1}$ for all $n$. As proof, the contrary is that all iterable paths terminate at some finite iteration stage, which is to say that there is some finite terminal stage $t$ such that $P_{n \geq t} = \varnothing$, at which all iterations stop. But this contradicts our construction whereby the iteration tiers $T_n$, and hence $P_n$, are countable in number and all non-empty.
Therefore, we have a countable set of paths $\Pi = \bigcup \rho_n$ such that $\rho_n \subset \rho_{n+1}$ for all $n$. $\blacksquare$
Yet, this tells us that a countable path iteration scheme exists - but it does not tell us that there is an infinite one-way path. Here one might reasonably say, "Why not?", or, "Of course it does!". At this point we're at an impasse reminiscent of Zeno's paradox, whereby Zeno says something along the lines of "if you want to touch the wall up ahead, you can't, because first you have to travel half the distance, then half the remaining distance, and so on indefinitely". In our context, the philosophical question is: does this iterate out an infinite path, contrary to what Zeno says, or does it just indefinitely iterate out finite paths? That's where DC comes in.
Invoking the Axiom of Dependent Choice
Specifically speaking, the subset relation $\subset$ over $\Pi$ is what's called an entire relation, whereby we have for any $a \in \Pi$ there is some $b \in \Pi$ such that $a \subset b$. From the Wikipedia entry on the Axiom of Dependent Choice:
The axiom of dependent choice can be stated as follows:
For every nonempty set $X$ and every entire binary relation $R$ on $X$, there exists a sequence $(x_n)_{n \in \mathbb{N}}$ in $X$ such that
$x_{n}Rx_{n+1}$ for all $n \in \mathbb{N}$.
Thus, by the axiom of choice, there is a sequence $(\rho_n)_{n \in \mathbb{N}}$ such that $\rho_{n}R\rho_{n+1}$ for all $n \in \mathbb{N}$. This is our infinite one-way path -- we simply reject Zeno's paradox.
Thus, $G$ contains an infinite one-way path; our proof is complete. $\blacksquare$
Afterthought
We appear to have implicitly invoked DC when we asserted that $\bigcup G_n = G$. From what I've seen, the fact seems to be asserted right away in proofs of similar things like colouring infinite graphs, without any explanation. I'm not 100% if this is DC at work here, but it seems to be the case.
As we can see this took a bit of effort to set up, but we needed to establish the vertex and edge tiers in order to set up an iterative scheme for $G$ to be used throughout the proof, rather than in the case of vertex colouring or planarity where the graph can be iterated out one vertex at a time. But in both of these cases similar constructions can be made: instead of $\pi_n$, the number of minimal paths of length $n$, we use the chromatic polynomial $P_G(k)$ or a parameter that represents the number of topologically distinct configurations of $G$, and instead of a "vertex locator" like $x_{ik}^n$ we might have a colour or configuration identifier.
Anyhow, if you've made it this far, thanks for going down the rabbit hole with me! Below is the construction of $\pi_n$, as promised.
Appendix: Constructing $\pi_n$
Here we need to return to the tiers of $G$ with respect to $v_0$. just to reiterate, we're still implying "minimal" when we talk about paths, and as a quick recap, we defined the $n^{th}$ tier of $G$ as $T_n = \{w \in V : L(w) = n\}$, the set of vertices which can be reached from $v_0$ via a path of minimum length $n$. The question of defining $\pi_n$, restated, would be: how many paths lead to $T_n$? There are two main parameters involved: given two vertices $v \in T_{n-1}$ and $w \in T_n$, we need to know how many paths lead into $v$, and how many edges join $v$ and $w$. To represent these, we define for all vertices $v$ and $w$:
$Q(v) =$ the number of paths leading into $v$ (we will explicitly define shortly)
$B(v,w) =$ the number of edges joining $v$ and $w$ (there may be more than one)
If we again take $v \in T_{n-1}$ and $w \in T_n$, the product $Q(v)B(v,w)$ gives us the number of paths leading into $w$ from $v$: each of the $Q(v)$ paths leading into $w$ may continue along any one of $B(v,w)$ edges to get there. We can see that this contributes towards $Q(w)$, but there may be other vertices in $T_{n-1}$ that also contribute. But if we add up all the contributions, we get $Q(w)$ as a whole. So we recursively define, for $w \in T_n$:
$Q(w) = \Sigma_{v \in T_{n-1}} Q(v)B(v,w)$ with $Q(v_0) = 1$ (there's only one minimal path from $v_0$ to $v_0$)
Adding up $Q(w)$ for all $w \in T_n$ then gives us the number of paths, $\pi_n$, leading into $T_n$:
$\pi_n = \Sigma_{w \in T_n} Q(w) = \Sigma_{w \in T_n} \Sigma_{v \in T_{n-1}} Q(w)B(v,w)$
$B(v,w)$ is always finite since $G$ is locally finite, thus $Q(w)$ is always finite (since it starts from $Q(v_0)=1$). Therefore, $\pi_n$ is always finite, as indicated in the proof.
And that about wraps it up. Thanks again for reading - I'm gonna go to bed now.