I read the following on Wikipedia's page on [Monadic Second-Order Logic of Two Successors (MS2S)](https://en.wikipedia.org/wiki/S2S_(mathematics)):



> 
> Weak S2S (WS2S) requires all sets to be finite (note that finiteness
> is expressible in S2S using Kőnig's lemma).
> 
> 
> 


Is this statement an error? I would think that only [Weak Kőnig's Lemma(WKL)](https://en.wikipedia.org/wiki/Reverse_mathematics#Weak_K%C5%91nig%27s_lemma_WKL0) would be expressible in MS2S since it is restricted to binary trees whereas [Kőnig's Lemma](https://en.wikipedia.org/wiki/K%C5%91nig%27s_lemma) is not limited to finite tree width. If it is possible to express the full Kőnig's Lemma, how would one do so? If not, how would one express WKL in MS2S? I looked at the [axiomatization of S2S](https://mathoverflow.net/questions/434659/axiomatization-of-s2s) but wasn't sure how to go about expressing WKL using it or another representation such as an infinite tree automata.



How can Kőnig's Lemma be expressed in Monadic Second-Order Logic of 2 Successors?

> 
> I would think that only Weak Kőnig's Lemma(WKL) would be expressible in MS2S
> 
> 
> 


You're slightly misreading the passage - the point is that Konig's Lemma can be used to show that finiteness is definable in MS2S. (That said, you are right that even WKL would be enough.)


Here's the idea. First, note that in MS2S we can define the ordering on $2^{<\omega}$: we have $\sigma\preccurlyeq\tau$ iff every predecessor-closed set containing $\tau$ also contains $\sigma$. From this **and (weak) Konig's Lemma** we can define infiniteness: $X$ is infinite iff every downwards-closed set $Y\supseteq X$ contains a chain with no greatest element.


The point is not that KL, or WKL, is somehow being expressed in MS2S; rather, we are using (W)KL in the metatheory so to speak in order to prove something about the strength of MS2S. This is in fact nontrivial: over general structures, monadic second-order logic is *incomparable* with weak monadic second-order logic despite the name of the latter. (To see why this is plausible, consider an equivalence relation with infinitely many infinite classes *and* infinitely many classes of each finite cardinality.)


