Master Logique Mathématique et Fondements de l'Informatique

• Calcul des propositions : tables de vérité, tautologies, formes normales, compacité.
• Calcul des prédicats : langages du premier ordre, termes, formules, modèles ; satisfaction d’une formule dans un modèle ; sous-structures ; isomorphismes ; équivalence élémentaire.
• Théorie des ensembles : axiomes de Zermelo-Frænkel ; cardinaux ; théorèmes de Cantor et de Cantor- Bernstein ; ensembles finis, ensembles dénombrables.
• Introduction à la programmation : Mise à niveau en programmation fonctionnelle Ocaml ; Lien avec le lambda-calcul, récursivité, typage ML ; structures de données usuelles (booléens, entiers, listes, options, arbres, ...).

• Langages, structures, théories du premier ordre
• Ultraproduits, compacité.
• Extensions élémentaires, Théorèmes de Lowenheim-Skolem, chaînes élémentaires.
• Théorèmes de préservation.
• Va et vients.
• Élimination des quantificateurs, modèle-complétude.
• Espace des types.
• (Si le temps le permet) Typer réalisés et types omis, modèles atomiques.

• Les axiomes de ZF
• Ordinaux, Cardinaux, récurrence transfinie
• Arithmétique ordinaux et cardinaux
• Axiom du Choix et équivalents, filtres et ultrafiltres
• Cofinalité, cardinaux réguliers/singuliers, théorème de König
• Ensembles stationnaires, clubs, Lemma de Fodor
• Absoluité et théorèmes de reflexion
• L'universe constructible

• Théorème de complétude du calcul des séquents égalitaire LK par les témoins de Henkin.
• Calcul des séquents : Élimination des coupures et théorème du séquent médian dans LK. Théorème de Herbrand. Sous-calcul LJ : la logique intuitionniste et son interprétation BHK. Propriétés de la sous-formule et du témoin existentiel dans LJ.
• Déduction naturelle : Systèmes NK et NJ. Élimination des coupures de NJ. Propriétés de la sous-formule et du témoin existentiel dans NJ, puis dans HA (arithmétique intuitionniste).
• Lambda-calcul : Propriétés de confluence et de standardisation. Représentation des fonctions récursives. Système T. Correspondance de Curry-Howard. Réalisabilité, normalisation forte et correction des programmes.

• Calculabilité : fonctions récursives et fonctions calculables par machine ; caractérisation logique des fonctions calculables ; théorème smn et théorèmes de point fixe ; notions de réduction et problèmes indécidables.
• Introduction à la complexité : classes en temps et espace, théorèmes de hiérarchie, réductions, complétude, circuits booléens, introduction à la complexité algébrique.
• Arithmétique formelle : axiomes de Peano et sous-systèmes faibles ; arithmétisation de la logique ; théorèmes d’indécidabilité ; les théorèmes d’incomplétude de Gödel.

Le cours présente les concepts fondamentaux de la théorie des catégories, illustrés de nombreux exemples. L’objectif essentiel est préparer l’accès aux applications actuelles des catégories en logique, en informatique théorique et en théorie de l’homotopie.

Une moitié des heures de ces modules consistera en des cours, l’autre en des TP sur machine. Ces cours se concluront par un projet à réaliser en Coq. Le contenu de ces cours est un prérequis pour le cours de théorie des types homotopiques.

Ce cours sera une continuation naturelle du cours de théorie des modèles du premier semestre. On cherchera à comprendre et classifier les modèles d'une théorie du 1er ordre donnée à travers les types que l'on peut réaliser ou omettre.

En termes modèle-théoriques, une expansion M du corps ordonné des réels est o-minimale si tout sous-ensemble M-définissable de R a un nombre fini de composantes connexes. Ceci peut être également formulé en des termes purement géométriques, en tant que propriété d'une collection d'ensembles réels stable par les opération booléennes ensemblistes, produits cartésiens et projections linéaires. Les ensembles définissables dans une structure o-minimale partagent de nombreuses bonnes propriétés topologiques avec les ensembles algébriques et analytiques réels (théorie de la dimension, finitude uniforme, stratification), d'où l'intérêt pour la géométrie o-minimale en lien avec la géométrie Diophantienne et arithmétique, les systèmes dynamiques non-oscillants et l'analyse asymptotique. Je donnerai une vue d'ensemble des résultats principaux sur les structures o-minimales et ensuite j'illustrerai les principales méthodes pour démontrer qu'une collection de fonctions réelles engendre une structure o-minimale. Il n'y a essentiellement pas de prérequis pour ce cours, outre que les notions de base d'algèbre et d'analyse acquises en licence : les notions de théorie de modèles nécessaires sont minimales et je fournirai de la bibliographie sur le sujet si besoin.

Le 8 août 1900, lors du second Congrès International des mathématiciens, à Paris, David Hilbert énonça une liste de 23 problèmes mathématiques qui, selon lui, devaient servir de guide pour les recherches à venir dans le nouveau siècle. Le premier problème de cette liste, l’hypothèse du continu de Cantor, a été résolu, en deux temps : par Gödel (1938) qui construisit un modèle interne de l'hypothèse généralisée du continu, et par Paul Cohen (1963), qui a inventé une construction de modèle pour la négation de l’hypothèse de Cantor. Ce cours couvrira principalement les deux constructions de modèles de la théorie des ensembles introduites par Gödel et Cohen.

Le thème principal du cours est l’interaction entre la logique et les jeux. De nombreux exemples d’une telle interaction existent, notamment la clôture stratégique et la détermination en théorie des ensembles, les jeux de Ehrenfeucht-Fraïssé en théorie des modèles, le jeux des cailloux en complexité descriptive et d’arguments de décision en théorie d’automates. Pour citer Jouko Väänänen, il y a trois sortes de jeux en logique, les trois en connexion étroite. Il nomme cette connexion « l’équilibre stratégique en logique ». Le cours sera librement inspiré par cette connexion et basé sur le livre « Models and games » par Väänänen, avec d’explorations supplémentaires en théorie descriptive des ensembles, les grands cardinaux et la décidabilité.

La théorie de la démonstration a connu au moins deux évolutions majeures au cours du siècle dernier suite aux théorèmes d'incomplétude de Gödel. La première a eu lieu dans les années 30, immédiatement après les résultats d'incomplétude, avec l'introduction et l'étude de la déduction naturelle et du calcul des séquents par Gentzen et du lambda-calcul par Church. Church montrait alors l'indécidabilité du calcul des prédicats via le lambda-calcul tout en introduisant un modèle de calcul universel tandis que Gentzen déduisait la consistance de divers systèmes logiques comme corollaire de l'élimination des coupures en calcul des séquents.

La seconde étape a eu lieu dans les années 60 avec la mise en évidence progressive, par le biais de la correspondance de Curry-Howard, des liens profonds entre preuves et programmes, depuis la correspondance entre lambda-calcul simplement typé et déduction naturelle propositionnelle minimale jusqu'aux diverses extensions de cette correspondance au second ordre, à la logique classique et jusqu'à l'émergence de la notion de linéarité en théorie de la démonstration. La logique linéaire a profondément renouvelé les liens entre la sémantique formelle des langages de programmation d'un côté et la théorie de la démonstration de l'autre. L'algèbre linéaire s'impose comme troisième pôle de cette correspondance, en mettant au centre la notion de ressource du calcul.

Le cours fondamental a traité de la première étape. Ce cours sera consacré à quelques développements plus récents.

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.

Ce cours est une continuation naturelle du cours "Calculabilité et incomplétude" du premier semestre. Les travaux de Godel, Church, Turing et d'autres, sur la définition formelle d'ensemble calculable, ont posés les bases sur lesquelles allait s'échafauder l'étude des degrés d'insolubilité : un important corpus de connaissances permettant de classer et comprendre l'univers des objets incalculables. Nous mèneront durant ce cours une étude détaillée de cet univers.

La calculabilité a aussi obtenu des succès majeurs en fournissant un cadre formel pour l'étude de certaines questions épistémologiques. Nous en verrons un exemple avec l'étude de l'aléatoire algorithmique. Nous verrons comment utiliser la calculabilité pour étudier avec une approche mathématique la question informelle de ce qu'est une suite de bits ``aléatoire''.

La deuxième partie du cours traite de la complexité de Kolmogorov. On donnera les définitions et les propriétés élémentaires. Nous verrons comment on utilise la complexité algorithmique dans les preuves de complexité. Nous étudierons les objets aléatoires finis et infinis.

Vers la moitié des années ’80 du siècle dernier, lorsque grâce à la correspondance de Curry-Howard le domaine de recherche au carrefour entre l’informatique théorique et la théorie de la démonstration est en plein essor, Jean-Yves Girard introduit et étudie des modèles dénotationnels du système F. Il découvre alors un modèle très simple de F, les espaces cohérents, qui possèdent de remarquables propriétés de dualité, et que les connecteurs de la logique intuitionniste se décomposent au moyen d’opérations plus élémentaires dans ce modèle. Qui plus est, il s’avère que cette décomposition peut être internalisée par le biais de nouveaux connecteurs logiques : c’est ainsi qu’aparaît la Logique Linéaire, comme structure sous-jacente à “la” logique en général, et aux processus calculatoires. La Logique Linéaire est un puissant outil pour analyser et contrôler l’utilisation des ressources en logique et en informatique. Sa nature de structure sous-jacente à la logique a conduit les chercheurs à développer des techniques, des approches et des méthodes qui ont été appliquées dans bien d’autres domaines (théorie de la séquentialité, sémantique de Scott, lambda-calcul, sémantiques de jeux, analyse de la logique classique et de son contenu calculatoire, complexité implicite, vérification, etc.).

Le cours présentera quelques outils fondamentaux de la théorie de la démonstration de la Logique Linéaire. Ils seront introduits à partir des questions qui ont conduit à leur mise au point et on cherchera à mettre en valeur les perspectives écloses par leurs propriétés.

Les formes du général