WS1S is Non-elementary: A Summary of Meyer's Proof

Abstract:Weakly monadic second order logic with one successor is not elementary recursive.
PDF (168 K)