Sujet de mémoire de recherche pour un master en informatique ou en mathématiques
Contexte
La logique intuitionniste (LJ) est très usitée en informatique car les démonstrations formelles de cette logique peuvent se traduire en algorithmes, comme on le voit dans la programmation fonctionnelle typée (par exemple: ML, CaML, Haskell) et dans certains démonstrateurs ou vérificateurs automatiques (par exemple: Coq).
Il est connu que LJ est complète par rapport aux faisceaux de L-structures (un ensemble muni d'une interprétation de chaque symbole de relation ou de fonction) sur un espace topologique :
(*) une formule du premier ordre est démontrable dans LJ si et seulement si (**) elle est valide dans tout faisceau de modèles.
Un faisceau de L-structures associe à chaque ouvert U d'un espace topologique X un modèle M(U), de sorte que:
Dans la littérature, la complétude (**)=>(*) est établie en montrant que l'algèbre de Lindenbaum Ω des formules (formules quotientées par l'équivalence A~B ssi A|-B et B|-A, A≤B ssiA|-B ) a la structure des ouverts d'un espace topologique (plus précisément, d'une algèbre de Heyting complète, ce qui correspond à une prétopologie) , puis la complétude pour les modèles Ω-valués, afin de conclure grâce à l'équivalence entre la catégorie des faisceaux sur Ω et des modèles Ω-valuées.
Objectif
Le but de ce mémoire est de produire et de rédiger une preuve directe de ce résultat. On pourra ensuite l'étendre à al logique multivaluée (ce qui est facile) puis à la logique d'ordre supérieur (ce qui est un peu plus difficile). On illustrera ce travail par la construction de modèles qui réfutent des théorèmes démontrables en logique classique mais pas en logique intuitionniste. En cas de franche réussite, l'étudiant pourra poursuivre en thèse sur l'étude des modèles de la théorie des types intuitionniste ou linéaire avec premier ordre. Ceci a des applications très prometteuses pour la formalisation et l'automatisation de la sémantique du langage naturel (il y a aussi des applications plus traditionnelles en spécification et vérification de programmes, même si ce point de vue est moins développé dans notre équipe).
Prérequis
Des connaissances en logique sont indispensables et une familiarité avec la topologie générale est souhaitable. Une allergie à la théorie des catégories peut être un obstacle.