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

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

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 approaches to calculi, to types and to the semantics. Quantitative systems are able to provide information such as the cost of computation, and are crucial to express paradigms of computation which are intrinsically quantitative, such as probabilistic, differential or quantum 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.

This is a course on Stone-Priestley duality theory and categorical logic. The main goal is to provide students with the necessary background to be able to start independently reading current research in this field.

We will start from bounded distributive lattices, which are fundamental structures in logic, capturing an extremely basic language that contains as its only primitives "or", "and", "true", and "false". Stone showed that distributive lattices are in a duality with a class of topological spaces with non-trivial specialization order. Priestley re-framed this duality as one between distributive lattices and certain partially ordered topological spaces. Duality theory has since then found applications in a number of areas within logic and the foundations of computer science.

The first part of the course will introduce the mathematical foundations of the theory, also introducing along the way the necessary order theory, topology, and category theory. In the second part of the course, we will discuss applications of the theory to logic, first to intuitionistic propositional and modal logics, and then to higher order logics. This last part will naturally lead to discussing concepts and methods from categorical logic and possibly also topos theory. The precise topics treated in this part will also depend on student interest.

Some basic knowledge of category theory and topology will be helpful, although not strictly required.

Les formes du général