I will talk about a result obtained a few years ago jointly with Henryk Michalewski, Pierre Pradic and Michał Skrzypczak. Our aim was to describe the strength of axioms needed to prove Büchi's theorem, which says that the monadic second order theory of the natural number order is decidable.

The axiomatic requirements of theorems involving second-order quantification over the naturals, like Büchi's theorem, are commonly studied within a research programme known as reverse mathematics, and often characterized in terms of an equivalence between the theorem and some fragment of so-called second order arithmetic. I plan to give a (brief) introduction to second order arithmetic and to monadic second order logic. Then I will discuss our main result, which says that Büchi's theorem (suitably formulated) is, over the usual base theory considered in reverse mathematics, equivalent to the induction scheme for Sigma^0_2 formulas. Various automata-theoretic statements related to Büchi... more

The axiomatic requirements of theorems involving second-order quantification over the naturals, like Büchi's theorem, are commonly studied within a research programme known as reverse mathematics, and often characterized in terms of an equivalence between the theorem and some fragment of so-called second order arithmetic. I plan to give a (brief) introduction to second order arithmetic and to monadic second order logic. Then I will discuss our main result, which says that Büchi's theorem (suitably formulated) is, over the usual base theory considered in reverse mathematics, equivalent to the induction scheme for Sigma^0_2 formulas. Various automata-theoretic statements related to Büchi... more