Some proof-theoretical approaches to Monadic Second-Order logic

Autor: Pradic, Pierre
Přispěvatelé: Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Preuves et Langages (PLUME), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Faculty of Mathematics, Informatics, and Mechanics [Warsaw] (MIMUW), University of Warsaw (UW), Université de Lyon, Uniwersytet Warszawski. Wydział Matematyki, Informatyki i Mechanik, Colin Riba, Henryk Michalewski, STAR, ABES, École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Jazyk: angličtina
Rok vydání: 2020
Předmět:
Zdroj: Logic in Computer Science [cs.LO]. Université de Lyon; Uniwersytet Warszawski. Wydział Matematyki, Informatyki i Mechanik, 2020. English. ⟨NNT : 2020LYSEN028⟩
Popis: 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.
Cette thèse traite de certains aspects de la logique Monadique du Second Ordre sur les mots infinis (MSO) à travers le prisme de la théorie de la démonstration.Elle contient deux parties distinctes.La première étudie des variantes intuitionistes de MSO avec de fortes propriétés du témoin qui permettent d’extraire des fonctions synchrones à partir de dérivations formelles.Un sous-système constructif avec la propriété du témoin est défini et est prouvé correct et complet pour la synthèse de Church. Pour ce faire, la correspondance entre formules de MSO et automates est raffinée pour donner une sémantique du système constructif où les preuves correspondent à une notion de simulation entre automates non-déterministes. Cette notion est étendue aux automates alternants. Cela mène à un sous-système de MSO plus fin basé sur la logique linéaire. Un théorème de complétude plus fort est montré pour ce dernier reposant sur la détermination des jeux ω-réguliers et une interprétation des formules similaire à la traduction Dialectica de Gödel.La seconde partie s’intéresse à la force axiomatique du théorème de décidabilité de MSO sur les mots infinis et autres résultats afférents de théorie des automates sur les mots infinis dans le cadre des mathématiques à rebours.On montre entre autres une équivalence entre la décidabilité de MSO, la version additive du théorème de Ramsey pour les paires et le principe de récurrence pour les formules Σ⁰₂ dans la théorie RCA₀. On conclut cette partie avec quelques résultats préliminaires concernant la décidabilité de MSO sur les rationnels, qui établissent que des axiomes strictement plus forts sont nécessaires dans ce cas.
Databáze: OpenAIRE
Externí odkaz: