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

Question

I read the following on Wikipedia's page on Monadic Second-Order Logic of Two Successors (MS2S):

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) would be expressible in MS2S since it is restricted to binary trees whereas Kőnig's 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 but wasn't sure how to go about expressing WKL using it or another representation such as an infinite tree automata.

Answer 1

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.)