Linking Game-Theoretical Approaches with Constructive Type Theory

Ce titre relie deux des courants de recherche les plus dominants dans la philosophie de la logique, à savoir la théorie des jeux et la théorie des preuves. Comme l'exprime le sous-titre de l'ouvrage, les auteurs établiront ce lien par le biais de l'approche dialogique de la logique. Un aspect important de cette étude est que les auteurs se limitent au fragment logiquement valide de la Théorie des Types Constructifs (CTT). La raison en est qu'une fois ce fragment atteint, le résultat peut être étendu pour couvrir l'ensemble du système CTT. Les premiers chapitres de l'ouvrage offrent des aperçus sur les deux cadres discutés dans le livre, avec un accent particulier sur le cadre dialogique. Le troisième chapitre démontre la direction de gauche à droite du résultat d'équivalence. Cela est suivi d'un chapitre qui montre l'utilisation de l'algorithme pour démontrer comment transformer une stratégie gagnante spécifique en une démonstration CCT de l'axiome du choix.