Salle 0C2 Bâtiment Chevaleret 175, rue du Chevaleret 75013 Paris Métro Chevaleret
Résumé de la thèse
La
sémantique des jeux est une modélisation du raisonnement logique : si
j'affirme une proposition, je dois être capable de répondre à toutes
les attaques de mon raisonnement par un adversaire imaginaire. Cette
interprétation de la logique se révèle à la fois flexible et précise,
ce qui en a fait un sujet de recherche très fécond au cours de la
dernière décennie. L'objet de cette thèse est l'étude de la
sémantique des jeux dans le cadre d'une quantification du second ordre,
c'est-à-dire lorsque l'on peut quantifier sur les propositions
logiques. Le modèle proposé, inspiré par les travaux antérieurs sur
cette question, est complet pour la logique etudiée, mais surtout
suffisamment souple pour permettre d'effectuer des calculs et des
raisonnements. Ainsi, on utilise ce modèle pour étudier une question
qui concerne la syntaxe logique que l'on modélise : la caractérisation
des isomorphismes de types, c'est-à-dire des équivalences entre
formules qui sont induites par la syntaxe. Cette thèse est centrée
autour de trois résultats principaux, à savoir la caractérisation des
isomorphismes de types pour le système F à la Church, pour son
extension classique, et pour le système F à la Curry. Dans chaque
cas, la caractérisation des isomorphismes dans le modèle passe par la
découverte d'un invariant géometrique qui se traduit ensuite en
équations.