Forthcoming seminars
Seminar calendar
List of seminars
Archive by years
Register a seminar

Forthcoming seminars

You may need the following programs to see the files

Seminar of the Department of Mathematical Logic "Proof Theory"
April 24, 2017 18:45–20:15, Moscow

The reverse mathematics of decidability results for monadic second order logic

Leszek Kolodziejczyk

Number of views:
This page:26

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

SHARE: FaceBook Twitter Livejournal
Contact us:
 Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2018