Quelques liens entre logique Monadique du Second Ordre et théorie de la démonstration
Pradic, Pierre · HAL (Le Centre pour la Communication Scientifique Directe) · 2020
This thesis studies certain aspects of Monadic Second-Order logic over infinitewords (MSO) through the lens of proof-theory. It is split into two independentparts.The first parts studies intuitionistic variants of MSO with strong witnessing properties allowing the extraction of synchronous functions from formal proof derivations.A constructive system with a suitable witnessing property is defined and proven correct and complete with respect to Church’s synthesis. To this end, the usual correspondence between MSO formulas and automata is refined to give a semantics of the constructive subsystem where proofs are correspond to simulations between non-deterministic automata. This notion is extended toalternating automata. This leads to a finer-grained system based on linear logicand MSO, which is then approached similarly. A stronger completeness theoremis shown for this latter system; the proof requires the determination of ω-regular games and an interpretation of linear formulas reminiscent of Gödel’sDialectica.The second part of this thesis is concerned with the axiomatic strength of the decidability theorem for MSO over infinite words and related results on infinite word automata. We proveamong other things an equivalence between the decidability of MSO, the additive version ofRamsey’s theorem for pairs and the principle of Σ⁰₂-induction over the weak artithmetical theoryRCA₀. We conclude this part by collecting a few results concerning the decidability of MSO overrationals, showing that axioms beyond Σ⁰₂-induction are necessary in that case.