Edit: Maybe this is not the best title, so few free to change it.

So I'm trying to prove the following statement:

A finitely branching tree $T$ with infinitely many vertices must have an infinite path.

My proof is loosely like this:

  1. $P = \emptyset$

  2. Start at the root $v_0$

  3. Since there are infinitely many vertices, there must be some vertice with infinitely successors.

    Order the successors of $v_0$ (there is a finite number of them), with the vertices with infinite successors to the left.

    $P = P \cup \{v_0\}$

    Select $v_1$ as the new root and repeat (3).

What bothers me the most is that I didn't manage to find a deterministic way to do step (3), at first I though BFS would work, since it's complete it would eventually visit all vertices at height $n$ and I could use this to construct an arbitrarily long path $P_n$, however arbitrarily long and infinite are two different things.

  • $\begingroup$ This is indeed not the best title, change it to what you want to proove, it will be clearer $\endgroup$ Commented Dec 10, 2016 at 2:24

1 Answer 1


You will not find an algorithm to do what you want. As you indirectly suggest, an algorithm can only check a finite prefix of any path. You can't even use the process of elimination as there may be multiple infinite paths. (If there was only one, you could eventually rule out all the other finite paths.)

As you are probably aware, this is (a corollary of) König's lemma. What you are asking for is essentially a constructive proof of it which doesn't exist. The typical (classical) proof repeatedly uses double negation elimination in the form: if no child has an infinite (simple) path then the subtree has a finite number of vertices, this is a contradiction thus there must be some vertex that has an infinite number of descendants. There is not, in general, a computable function to pick out this vertex though. Knowing that it must "exist" doesn't mean we have any way of calculating it.

  • $\begingroup$ Thanks! I wasn't aware about König's lemma, at first I though this was just some silly theorem and wouldn't imagine that it's related to the Axiom of choice. $\endgroup$
    – Aristu
    Commented Dec 10, 2016 at 15:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.