Logic seminar
The logical strength of Büchi's decidability theorem
Leszek Kolodziejczyk
University of Warsaw
Monday, 25. May 2020 - 13:30 to 15:00
https://us02web.zoom.us/j/472648284 - meeting ID: 472 648 284
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's theorem also turn out to be either equivalent to, or provable from, Sigma^0_2 induction.
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's theorem also turn out to be either equivalent to, or provable from, Sigma^0_2 induction.