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.
Gratuit
Disciplines