Master Logique Mathématique et Fondements de l'Informatique

Calcul des prédicats:

- langages, structures, formules, satisfaction, équivalence logique, formes prénexes;
- morphismes, plongements, isomorphismes, préservation des formules;
- calcul des propositions, tables de vérité, formes normales disjonctives et conjonctives.

Cardinalité:

- ensembles finis, ensembles dénombrables, equipotence, subpotence, classes cardinales, arithmétique cardinale;
- théorèmes de Cantor et de Cantor Bernstein ;
- Applications de Zorn et de l'axiome du choix, trichotomie.

Introduction à la théorie des modèles:

- théories consistantes, théories complètes, équivalence élémentaire, classes élémentaires, sous-structures et plongements élémentaires, test de Tarski, va et vients;
- exemples de théories, complétude: ensemble sans structure, prédicat unaire, ordre, relation d'équivalence, bijection sans cycles, groupes, anneaux, corps algébriquement clos, espaces vectoriels; 
- théorème de compacité, différents énoncés et applications: modèles infinis d'une théorie, théories finiment axiomatisables, classes non élémentaires, constructions de modèles non-standards. 

Topologie (bases):

- ouverts, fermés d'une topologie, topologie discrète topologie engendrée par une famille d'ensembles, base d'ouverts, topologie induite, topologie produit, voisinages, base de voisinages, axiomes de dénombrabilité, notion de limite, continuité, espaces séparés, adhérence, intérieur, parties denses,  espaces séparables, espaces compacts, Tychonov, Bolzano Weierstrass, Borel Lebesgue;
- espaces métriques, topologie de l'ordre, topologie de l'espace des théories complètes et closes par conséquence et lien avec le théorème de compacité du calcul des prédicats; conditions nécessaires de métrisabilité, espaces normaux;
- filtres, bases de filtres, filtre image, filtre principal, filtre de Fréchet. Comparaison de filtres, filtres compatibles, ultra-filtres. Applications à la topologie : filtre des voisinages d'un élément dans un espace topologique, convergence, valeur d'adhérence, application à la compacité, démonstration des théorèmes de Bolzano Weierstrass et de Tychonov, application : théorème de compacité du calcul propositionnel.

Systèmes de Hilbert, théorème de complétude

- axiomes, règles de déduction, démonstrations formelles , conséquence syntaxique. Cas du calcul propositionnel (théorème de complétude en devoir). Cas du calcul des prédicat, quelques preuves formelles, lemme de finitude, lemme de déduction, lemme fondamental, théories cohérentes, théories syntaxiquement complètes;
- témoins de Henkin, théorème de complétude, applications à la logique du premier ordre: théorème de compacité du calcul des prédicats, théorème de Lowenheim-Skolem, critère de Vaught.

  Introduction à la théorie des ensembles (en utilisant la théorie des modèles):

- présentation des axiomes de ZF; définitions: couples, relations, applications, familles d'ensembles;
- construction des entiers principe de démonstration et de définition par récurrence;
- axiome du choix, énoncés équivalents, équivalence de l'axiome du choix avec Zermelo, Zorn, trichotomie, Tychonov quasi-compact (ébauches de démonstrations). 

• 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

• Calcul des séquents : Étude des calculs des séquents classique (LK) et intuitioniste (LJ). Théorème de complétude du calcul des séquents LK. Élimination des coupures et ses applications (pour LK: théorème du séquent médian, théorème de Herbrand, interpolation de Craig-Lyndon; pour LJ: propriétés de la disjonction et du témoin existentiel).
• Déduction naturelle : Systèmes NK et NJ. Élimination des coupures de NJ. Arithmétique de Heyting (HA).
• Logique intuitioniste: Interpretation BHK. Modèles de Kripke. Traductions par double négation.
• Lambda-calcul pur: Confluence et standardisation. Représentation des fonctions récursives. Théorème de séparation et Arbres de Böhm.
• Lambda-calcul simplement typé et Système T: Correspondance de Curry-Howard. normalisation forte et correction des programmes.
• Sujets d'ouverture : en fonction du temps disponible en fin de semestre, on abordera quelques sujets d'ouverture (possibilités: système F, théorie des types dépendants, Curry-Howard pour la logique classique, calcul de termes pour les preuves en séquents, logiques linéaire et modale)

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

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.

Dans ce cours nous étudierons la théorie des modèles des structures métriques, telles que les espaces de Hilbert et de Banach, les algèbres de probabilité, les systèmes ergodiques ou les algèbres d'opérateurs. Celle-ci est basée sur le formalisme de la logique continue, une généralisation naturelle (à valeurs réelles) de la logique du première ordre classique. Nous étudierons également en détail un fragment distingué de la logique continue, appelé logique affine, et ses connexions toutes récentes avec la théorie de Choquet en analyse fonctionnelle.

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.

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.

Ce cours portera sur le contenu calculatoire des preuves, aussi bien en logique constructive qu'en logique classique et en présence de principes de choix comme la bar-induction.

The Curry-Howard correspondence highlights deep links between proofs and programs. Linear logic has profoundly renewed this connection between the formal semantics of programming languages on one hand and proof theory on the other, by bringing attention to the dynamics of programs (how the computation is performed) and on the use of resources. An outcome of this attention to resources are quantitative and interactive approaches to calculi, to types and to the semantics. Quantitative and interactive systems are able to provide information such as the costs of computation, and to express non-functional and low-level aspects of computation.

Nous aborderons différents thèmes de complexité. En complexité booléenne, nous parlerons en particulier de complexité de comptage et de complexité de communication. Nous étudierons aussi la complexité algébrique, sur laquelle s'appuient certains efforts récents pour résoudre le problème P vs. NP. En plus d'une présentation générale, nous explorerons des régimes calculatoires restreints, notamment les calculs non-commutatifs, et présenteront certaines bornes inférieures et les techniques de rang qui permettent de les obtenir.

The course is dedicated to the model-checking problem over finite structures, with a particular focus on algorithmic meta-theorems, the main highlight of the course being Courcelle's Theorem.

A number of topics are touched upon through this lens, including some basics in complexity theory, circuit complexity, parameterised complexity, monadic second-order logic, tree languages, logical transductions, structural graph theory, etc.

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.

Les formes du général