Seminars
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
Calendar
Search
Add a seminar

RSS
Forthcoming seminars




Seminars "Proof Theory" and "Logic Online Seminar"
April 24, 2017 18:45–20:15, Moscow, Steklov Mathematical Institute (8 Gubkina), room 313 + Zoom
 


The reverse mathematics of decidability results for monadic second order logic

Leszek Kolodziejczyk

Number of views:
This page:117

Abstract: I will talk about the results of a reverse mathematics-style study of the axiomatic strength needed to prove two classical results on the decidability of monadic second order theories: Büchi's Theorem, which concerns the monadic theory of the natural numbers with successor, and Rabin's Theorem, which concerns the monadic theory of the full infinite binary tree with the left- and right-successor relations.
Unlike most typical decidability theorems for first order theories, the proofs of Büchi's and Rabin's Theorems seem to require the use of some nontrivial set-theoretic principles: either Ramsey's Theorem or Kőnig's Lemma in the case of Büchi, and a restricted version of Borel determinacy in the case of Rabin. We show that in fact, the Ramsey-theoretic principle needed to prove Büchi's Theorem is quite tame, and the decidability theorem itself holds in the recursive reals, though it is not provable in RCA_0. On the other hand, the determinacy principle used in the proof of Rabin's Theorem turns out to be equivalent to a crucial automata-theoretic fact used in the inductive proof of the theorem, and in some contexts to the decidability theorem itself. It follows that Rabin's Theorem is unprovable in relatively strong fragments of second order arithmetic.
The talk will be based on joint work with Henryk Michalewski, Pierre Pradic and Michał Skrzypczak.

Language: English
 
  Contact us:
 Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024