Séminaires : Séminaire Général de Logique

Equipe(s) : lm,
Responsables :O. Finkel, T. Ibarlucía, A. Khélif, S. Rideau, C. Sureson
Email des responsables :
Salle : salle 2015
Adresse :Sophie Germain
Description

ArchivesRetour ligne automatique
Abonnement à la liste de diffusion


Orateur(s) Hugo Herbelin - IRIF, Université Paris Diderot,
Titre Calculer avec le théorème de complétude de Gödel
Date03/12/2018
Horaire15:10 à 16:10
RésumeDans un premier temps, nous donnerons une analyse du contenu calculatoire de la preuve de Henkin du théorème de complétude (dans le cas d'une théorie récursivement énumérable).

Dans un deuxième temps, on s'intéressera à la traduction de forcing de l'énoncé de complétude pour s'apercevoir qu'on obtient alors un énoncé de complétude vis à vis des modèles de Kripke. En ré-interprétant la preuve standard de complétude vis à vis des modèles de Kripke en style direct (dans le même sens où la logique classique est un « style direct » pour raisonner intuitionnistiquement au travers des traductions négatives de Kolmogorov-Gödel-Gentzen), on obtiendra une preuve originale et calculatoire très simple du théorème de complétude... mais qui utilise une allocation mémoire !
Sallesalle 2015
AdresseSophie Germain
© IMJ-PRG