Proof Of König's Lemma I am trying, carefully, to prove König's Lemma that an infinite binary tree $T$ has an infinite simple path. 
Let $R$ denote the root vertex of $T$. If I start at $v_1=R$, there must be a vertex adjacent to $R$, call it $v_2$, such that infinitely many vertices of $T$ are reachable by going up the tree from $v_2$. 
If not, the tree would be a finite tree (finite union of finite sets of vertices). 
I can repeat this process. Whenever I am at vertex $v_n$, I can find a vertex $v_{n+1}$ such that there are infinitely many vertices still available above $v_{n+1}$ in the tree. 
By induction, for any $n$ I can have that there exists a path of length $n$, in $T$. 
How do I get from this an infinite path? Surely mathematical induction gives me the existence of an arbitrarily long finite path, which is not the same thing?  

Edit: Ah, I think I've got it. I can order the vertices in each level of the tree from the left to the right, and at every step define $p(n)=$ the leftmost (resp. rightmost) vertex that has infinitely many vertices above it. Induction gives me the path $p(1)p(2)\ldots p(n)$ for every natural $n$ and then the infinite path is the set-theoretic union over $\Bbb N$ of these arbitrarily long finite paths?

 A: You can rearrange your argument a little bit. We recursively construct a set $\{ s_n \mid n \in \mathbb N \}$ of $0/1$ sequences such that $s_0 = ()$ is the root of your tree. Given $s_n$, we let $s_{n+1} = s_{n} \ ^\frown (0)$, if there are infinitely many points above $s_{n} \ ^\frown (0)$ and otherwise we let $s_{n+1} = s_{n} \ ^\frown (1)$. Note that in either case there are infinitely many points above $s_{n+1}$ - so this construction never breaks down.
Let $s$ be the unique infinite $0/1$ sequence such that the first $n-1$ entries of $s$ agree with $s_{n}$ - for every $n \in \mathbb N$. By construction $s$ is an infinite branch through our tree.
A: I shall summarise some of the further points discussed in the Comments in this Answer.
Proofs of Konig's Infinity Lemma (for Graphs and for Trees) (e.g. the Wikipedia proof) build the path vertex by vertex with two aspects which require discussion:


*

*The determination of which successor node(s) actually have an infinite path though them;

*The selection process whenever two (or more in general Trees) meet condition 1


For condition 1. In ZF Set theory the arguments of the proof are sufficient to establish that at least one such successor node exists without having to determine which one that is, for the purpose of the proof.
For condition 2. The selection process is a calculation if the Vertex set is well ordered: one simply uses $min\{V0,V1\}$ in the ordering when $\{V0,V1\}$ are the two successors meeting condition 1. However if the Vertex set is not well ordered the above calculation is not defined and so the Axiom of Dependent choice (or similar form of Weak Axiom of Choice) is required for the proof to go through.
In other words in ZFC Set Theory (which is the usual framework for Graph Theory and other parts of mathematics) Konig's Lemma holds unconditionally. In ZF Set theory Konig's Lemma is only valid with the additional condition that the Vertex Set is well ordered. This condition is met in the important special case in which the Vertex Set is (provably) countable. So for countable binary trees Konig's Lemma again holds unconditionally in ZF Set Theory.
This leaves open the question of actually calculating which successor node(s) meet condition 1. Although not required in the ZF proof, one can see that this would require an "infinite lookahead" to check that a given candidate Vertex actually led to an infinite path. This process is clearly not recursive and in Reverse Mathematics it was established that (for a binary tree) it is equivalent to a non-constructive axiom called Weak Konig's Lemma ($WKL_0$). For an arbitrary finitely branching tree it is equivalent to a stronger axiom called $ACA_0$. All trees in Reverse Mathematics are countable and so the ZF proof of Konig's Lemma applies.
