Master Logique et Fondements de l'Informatique

Le cours préliminaire sera du 2 au 13 septembre.

• 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.

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.

Depuis ses débuts, les corps valués ont toujours eu une place de choix parmi les structures étudiés en théorie des modèles. L'une des raisons de cet intérêt est que leur lien fort avec l’arithmétique et la géométrie ont permis l’introduction dans d’autres domaines des mathématiques des techniques de la théorie des modèles, avec pour résultat, dans la plupart des cas, la résolution de questions ouvertes dans ces domaines.

L’un des premiers exemples d'une telle interaction est les travaux d’Ax-Kochen et indépendement Ershov qui donnent une solution à une conjecture d’Artin sur l’existence de solutions à des équations homogènes sur le corps des nombres p-adiques. L’un des principaux intérêts conceptuels de leur preuve est qu’elle réduit une question sur (certains) corps Henséliens de caractéristique nulle, en l’occurence la description de leur théorie, à cette même question sur leur corps résiduel et leur groupe de valeur. L’idée de cette réduction se retrouve ensuite dans la plupart des travaux sur la théorie des modèles des corps valués.

Le but de ce cours sera, en commençant par les questions d’élimination des quantificateurs, puis en allant vers des questions de théories des modèles plus « géométrique », en passant par la théorie de classification de Shelah, d’illustrer l’omniprésence de ce principe dit d’Ax-Kochen-Ershov en théorie des modèles des corps valués. Nous essayerons aussi, dans la mesure du possible, d’esquisser certaines des applications récentes de la théorie des modèles des corps valués.

La théorie des ensembles est connue pour des raisons diverses : pour sa prouesse en modélisation des mathématiques par certains et pour son agilité à manipuler la combinatoire de l’infini par d'autres. L’axiomatisation classique de la théorie des ensembles est donnée par les axiomes de Zermelo-Frankel avec l’Axiome du Choix (ZFC), mais elle connaisse des limitations. Une façon concrète de les étudier est donnée par la méthode du Forcing et les axiomes du forcing et leur positionnent par rapport de l’univers constructible L.

En suivant ce cours, l’étudiant déjà connaisseur des bases de la théorie axiomatique des ensembles, débutera sur les parties avancées du sujet. On expliquera la méthode du forcing, dont la preuve célèbre du fait que l’hypothèse du continu (HC) n’es pas démontrable en théorie des ensembles. En passant par d’autres exemples classiques du forcing, tels que l’Effondrement de Lévy, on sera naturellement amenés à l’étude d’itérations du forcing et d’Axiome de Martin, tout comme ces applications et les limitations.

Les axiomes de grands cardinaux postulent l'existence de cardinaux ayant un degré de transcendance donné par rapport aux petits cardinaux et fournissent une superstructure pour l'analyse des énoncés mathématiques forts. L'étude de ces axiomes est en effet un courant dominant de la théorie moderne des ensembles. Par exemple, ils jouent un rôle crucial dans l'étude des ensembles définissables de réels et de leurs propriétés de régularité telles que la mesurabilité de Lebesgue. Bien que formulées à différents stades du développement de la théorie des ensembles et avec des motivations différentes, il s'est avéré que ces hypothèses former une hiérarchie linéaire allant jusqu'à l'incohérence. Toutes les propositions connues de la théorie des ensembles peuvent être évaluées dans cette hiérarchie en fonction de leur force de cohérence, et la structure émergente des implications fournit une image remarquablement riche, détaillée et cohérente des propositions les plus fortes des mathématiques telles qu'elles sont intégrées dans la théorie des ensembles.

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é aux développements depuis les années 60 et présentera les outils classiques pour l'étude de la correspondance de Curry-Howard. Après quelques rappels et compléments du cours fondamental, le cours se concentrera sur deux concepts fondamentaux, le second-ordre et la linéarité, et à leurs développements, notamment dans un cadre algébrique. On appliquera notamment les résultats du cours à l'étude de PCF, un langage de programmation idéalisé.

L’objectif du cours est de présenter plusieurs point de vue sur la complexité venant de la logique, de la théorie de la récursion ou de l’analyse. Ces approches ont pour point commun de s’abstraire de la notion de machine (et de ses mesures associées comme le temps et l’espace) au profit d’une vision plus descriptive du calcul. Le cours vise notamment à étudier des formalismes logiques sous l’angle de leur pouvoir d’expression et à présenter de multiples caractérisations des classes de complexité usuelles.

Ces approches de le complexité dîtes descriptives ou implicites ont connu des applications importantes en théorie des bases de données, des langages de programmation ainsi que plus récemment autour de l’analyse des systèmes d’équations différentielles, ou autour de la compréhension de la puissance de modèles alternatifs de calculs basés sur la bioinformatique, ou le calcul analogique.

On visera à présenter dans un premier temps des résultats sur la complexité classique [8, 13], pour aller vers des extensions à des modèles algébriques comme le modèle de Blum Shub et Smale [3, 2], à espace continus comme les modèles de réseaux de neurones/deep learning [17], puis à temps et espace continu comme le modèle de Shannon [16].

Attention, ce cours aura lieu les 6 dernières semaines du 1er semestre et les 6 premières semaines du 2nd semestre.

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 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 théorie de l'homotopie, ou l'étude des espaces topologiques à déformation près, a fait surgir une branche de l'algèbre appelée algèbre homotopique, où sont développés les outils pour la description de structures où les lois telles que l'associativité ne sont plus vérifiées exactement comme en algèbre classique, mais à homotopie près, ces homotopies étant elles-mêmes sujettes à des cohérences, et ainsi de suite.

La théorie de l'homotopie a aussi une dimension logique, avec l'interprétation de la notion de type comme espace, de preuve d'égalité comme chemin dans un espace et de preuve d'égalité de preuves d'égalité comme une homotopie entre chemins. Ces liens ont donné naissance à la théorie homotopique des types. La notion de fibration, qui joue un rôle essentiel en théorie de l'homotopie, est intimement liée à la notion de substitution en théorie des types dépendants.

Le cours, qui fera suite au cours de théorie des catégories du premier semestre, mais peut être suivi par des étudiants ayant déjà acquis ces bases par ailleurs, introduira les notions importantes sous-jacentes au domaine: les catégories enrichies, les catégories de modèles, et différentes façons de définir les catégories supérieures, notamment via les ensembles simpliciaux. Seront abordés aussi des sujets connexes comme les opérades et les ∞-opérades, eux aussi issus de la topologie. Le cours s'appuiera en partie sur plusieurs ouvrages parus dans les années récentes (Categorical homotopy theory d' Emily Riehl, The homotopy theory of (∞, 1)-categories de Julia Bergner, From categories to homotopy theory de Birgit Richter, Higher categories and homotopical algebra de Denis-Charles Cisinski, Simplicial methods for higher categories de Simona Paoli, qui offrent autant de lectures d'approfondissement pour les étudiantes et étudiants intéressés), avec une attention portée aux liens avec la théorie homotopique des types.

Ce cours vise à présenter les fondements logiques et informatiques des blockchains (protocoles de communications, théorie des jeux), ainsi que des exemples de protocoles mis en oeuvre en particulier dans les crypto-monnaies et les smart-contracts. Nous consacrerons une partie substantielle du cours à l’examen de la "finance décentralisée” c’est-à-dire l’ensemble des contrats existants sur chaine qui reporoduisent et pour certains étendent les pratiques financières.

En quoi la logique est-elle formelle ?

Le cours sera consacré à cette question. Il examinera en particulier trois grandes raisons de déclarer « formelle » la logique : parce qu’elle recourt à des ressources discursives qu’on peut dire formelles (schématiques) ; parce qu’elle porte sur des formes (dont le statut est à préciser : « constantes logiques » pour Russell, « formes dérivées du quelque chose en général » pour Husserl, pour prendre deux exemples importants) ; parce qu’elle vise à une validité indépendante de tout contenu particulier (logique comme science universelle).

Ces trois grandes raisons ne sont pas nécessairement compatibles. Par ailleurs, l’examen de la question posée impliquera bien entendu la prise en compte de l’histoire de la logique, et une réflexion sur la situation de la logique entre philosophie et mathématiques. Ce sera l’occasion d’examiner l’enjeu de la « généralité absolue », c’est-à-dire celui de la possibilité d’une théorie portant sur absolument toutes choses en général.

Compétences visées : connaissance des enjeux philosophiques de l’histoire de la logique au XXe siècle.