Quantification du second-ordre et points-fixes en logique
8 ECTS, semestre 2, 12 semaines
| Prérequis | suivre le cours preuves-programmes : outils classiques en parallèle de ce cours constituera un complément judicieux. |
| Validation | CC+examen |
| Enseignant | Alexis Saurin et Thomas Colcombet |
| Horaires hebdomadaires | 48 h CM |
| Années |
Syllabus
Ce cours étudiera sous différents aspects la notion de second-ordre en logique et étudiera les logiques à points-fixes. On abordera notamment différentes applications informatiques de ces formalismes logiques à l'étude des langages formels sur les mots et les arbres et à l'étude des langages de programmation.
Sommaire
Partie 1: Logique et arithmétique du second-ordre, système F
Syntaxe de la logique du second-ordre, déduction naturelle du second-ordre, théories et fragments particuliers (PA2, HA2, MSO, F, ...).
Modèles du second-ordre: modèles pleins et modèles de Henkin, complétude au second-ordre.
Preuves et programmes: extension de la correspondance de Curry-Howard (second-ordre et polymorphisme) et étude du système F (définition, représentation des types de données, théorèmes de normalisation (candidats de réductibilité de Girard, réalisabilité), fonctions représentables dans F).
Partie 2: Logique du second-ordre monadique
Définitions, rappels et compléments sur la théorie des automates.
Décidabilité sur les mots (Elgott-Büchi-Trakhtenbrot); liens avec les automates et les monoïdes.
Le premier-ordre dans le second-ordre (théorème de Schützenberger).
Décidabilité sur les structures ressemblant à des arbres (théorème de Courcelle) et les limites structurelles à la décidabilité (théorème de Seese).
La méthode compositionnelle de Feferman-Vaught et Shelah.
La théorie sur les mots infinis (Büchi, Safra).
La théorie sur les arbres infinis et liens avec la théorie des jeux (Rabin, Gurevitch et Harrington).
Partie 3: Plus petits et plus grands points fixes en logique
Quelques résultats sur les points-fixes.
Syntaxes et sémantiques des logiques avec plus petits et plus grands points-fixes (définitions inductives à la Martin-Löf, mu-calcul pour les logiques classique, intuitionniste et modale).
Systèmes de déduction pour les logiques à points-fixes: induction à la Park, règle Omega, preuves circulaires.
Relations avec les automates, avec la logique du second-ordre monadique.
Complétude du mu-calcul et autres résultats.
Bibliographie
- Rudiments of mu-calculus, A. Arnold and D. Niwinski
- Proofs and Types, JY Girard, P Taylor, Y Lafont
- Proof-theory and Logical complexity, JY Girard -Lambda-calculus and models, JL Krivine
- Proof Theory, Gaisi Takeuti
- Survey of Wolfgang Thomas, Languages, Automata and Logic
- Automata toolbox book https://www.mimuw.edu.pl/~bojan/papers/toolbox.pdf