(Long) Detailed Proof of Kőnig's Lemma (Explicit, Down to Axiom of Choice) Kőnig's Lemma states that in an infinite, locally finite, connected graph $G$, there exists an infinite one-way path (a ray). The proof of it in my graph theory book (Introduction to Graph Theory, 4th ed., Wilson) had a sour taste to it, like it was covering something up. So I checked out proofs from other sources, which also seemed to cover up something which felt very close to the foundation (i.e. using the axioms). After looking it up I found out that this is indeed the case, as it results directly from the axiom of dependent choice (DC).
This wasn't a question on an assignment for me or anything, but I wanted to try to give a more detailed, albeit lengthy proof of the lemma with more explicit constructions and play-by-play, highlighting some of the key points and bare bones math going on here (including the general statement of the lemma and the use of DC), to the best of my understanding. I was hoping that anyone with time to spare hands could review or give comment, make sure everything I'm stating things correctly! And of course, I would be happy if this helps anyone in a similar predicament that comes to read this in the future, or helps anyone to appreciate the deeper levels of a simple theorem. 
I've enabled the "answer your own question" box so I can post my proof separately, but I encourage/challenge others to do the same and make a detailed construction as an exercise, especially during these times of isolation!
Below I'll prove a similar theorem which uses Kőnig's Lemma in a more general form (but sweeps DC under the rug). It's a good reference because it's easier to understand without a super explicit construction:

Let $G$ be a countable graph such that every finite subgraph of $G$ is $k$-colourable. Then $G$ is $k$-colourable.

Proof 
Since $G$ is countable, its vertices are enumerable as $v_1$, $v_2$, $v_3$, etc. Let $G_n$ be the (finite) subgraph induced by vertices $v_0$ through $v_n$. Since each vertex $v_n$ corresponds to a finite induced subgraph $G_n$, there are countably many $G_n$. Since $G_n \subset G_{n+1}$ for all $n$ by construction, the union over all $G_n$ yields $G$. Since each $G_n$ is finite, there are countably many corresponding sets $C_n$ of valid $k$-colourings of $G_n$, each non-empty with a finite number of elements given by the chromatic polynomial of $G_n$, $P_{G_n}(k)$. If we consider a colouring of $G_{n+1}$ and remove vertex $v_{n+1}$, we are left with a valid colouring of $G_n$: removing vertices does not invalidate a colouring. And so this valid colouring of $G_n$ must be an element of $C_n$. In general, for every colouring $c_{n+1} \in C_{n+1}$ of $G_{n+1}$ there is some colouring $c_{ind} \in C_{n}$ such that $c_{ind} \prec c_{n+1}$ (i.e. $c_{ind}$ is induced on $G_n$ by $c_{n+1}$). Kőnig's Lemma states that since there are countably many non-empty $C_n$ that follow these conditions, we must have a countable set of $c_n \in C_n$ such that $c_n \prec c_{n+1}$ for all $n$. If there were not, then all inductive sequences of colourings would terminate at some finite point $t$. If we take $\tau$ to be the maximum such $t$ over all sequences, then $C_{\tau + 1}$ must be empty, contradictory to our assumption that all $G_n$ are $k$-colourable (and in turn that all $C_n$ are non-empty). Therefore there is a countable set of inductive valid $k$-colourings $c_n$, and their union gives us a valid $k$-colouring of $G$. 
Thus, $G$ is $k$-colourable. $\blacksquare$ 
The general form of Kőnig's Lemma can be stated as follows (paraphrasing Infinite Graphs - A Survey, by Nash-Williams, 1967):

Given a countable sequence of finite, non-empty, disjoint sets $S_n$ and a relation $\prec$ on $\bigcup S_n$, if for each element $s_{n+1} \in S_{n+1}$ there exists an $s_n \in S_n$ such that $s_n \prec s_{n+1}$, then there exists a countable sequence of elements $(s_n)$ such that $s_n \prec s_{n+1}$ for all $n$. 

The end of the $k$-colouring proof I gave is basically the proof of this theorem. In this general form, the $S_n$ can be thought of as "configuration spaces" (finite sets of valid configurations), and the relation $\prec$ can be thought of as an inductive consistency relation. In the $k$-colouring proof, our configuration spaces are the $C_n$ and they are finite due to the chromatic polynomial of $G_n$, though I didn't explicitly construct them so we can't show that they are disjoint. But as I mentioned, this is still easier to understand without explicit construction. This is because we iterate out $G$ vertex by vertex, and as a result, we get a natural correspondence between the iterated subgraphs and their colourings. In proving the graph theoretic result about the existence of an infinite one-way path, the iteration scheme is not vertex by vertex, and so more explicit construction is needed to make the simple argument as above. That will be in my proof below, and similar methods can be used to construct a more explicit proof of this $k$-colourability result, and one for planarity as well! 
 A: 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\}$.
A: 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.  
