Talk:König's Tree Lemma

The following statement is superfluous and should be removed. --Ilan 05:03, 23 April 2012 (EDT)

• Each $t_n$ has infinitely many descendants.

I disagree. You need to suppose that $t_n$ has infinitely many descendants in order for the induction to work.

If there is a different proof which does not require this hypothesis, then that is a different proof and needs to be entered as such.

On the other hand, if you can see this proof working without that hypothesis, feel free to amend it accordingly. --prime mover 08:15, 23 April 2012 (EDT)

My point is that the first two conditions are necessary as a statement of the result, while the third is only used in the proof. I can modify the proof in order to clarify this distinction. --Ilan 16:50, 23 April 2012 (EDT)

Which would make it a separate proof, yeah? As it stands, the "infinite descendants" is part of the proof, not part of the statement of the result. --prime mover 17:03, 23 April 2012 (EDT)

Induction

Prime.mover, it is NOT a proof by induction. At each step, it makes an arbitrary choice. The minimal correction is to use the Axiom of Dependent Choice.

The minimal choice principle that can be used to prove the theorem is almost certainly the Axiom of Countable Choice for Finite Sets. --Dfeuer (talk) 22:15, 26 May 2013 (UTC)

Since when are we not allowed to fix mathematical errors? --Dfeuer (talk) 23:06, 26 May 2013 (UTC)

Strong induction. Given that it's true for all numbers up to $k$, and then it's true for $k+1$, that smells like induction to me. Whether during the course of the induction step it needs your AoCFS or ADC is another thing altogether. But it's using induction. --prime mover (talk) 06:32, 27 May 2013 (UTC)

Induction proves that there is a path of every finite length. It cannot, however, prove that there is an infinite path. For that, we can go with the strong medicine of dependent choice or the weak medicine of countable choice for finite sets. The only role for induction is in the latter approach, where induction proves that there are finitely many enumerations of any given finite set and then recursive definition produces the sequence once choice has already been applied (fill in those gaps at Dependent Choice for Finite Sets if you like). --Dfeuer (talk) 07:36, 27 May 2013 (UTC)

If you wish to understand more fully, try to apply the Principle of Recursive Definition more formally. You will hit a brick wall of not being able to formulate the mapping that is to be applied repeatedly. It simply doesn't help. --Dfeuer (talk) 07:48, 27 May 2013 (UTC)

go for it then --prime mover (talk) 10:20, 27 May 2013 (UTC)