Preuves et jeux sémantiques
Résumé
Hintikka makes a distinction between two kinds of games: truthconstituting games and truth-seeking games. His well-known game-theoretical semantics for first-order classical logic and its independence-friendly extension belongs to the first class of games. In order to ground Hintikka’s claim that truth-constituting games are genuine verification and falsification games that make explicit the language games underlying the use of logical constants, it would be desirable to establish a substantial link between these two kinds of games. Adapting a result from Thierry Coquand, we propose such a link, based on a slight modification of Hintikka’s games, in which we allow backward playing for ∃loïse. In this new setting, it can be proven that sequent rules for first-order logic, including the cut rule, are admissible, in the sense that for each rule, there exists an algorithm which turns winning strategies for the premisses into a winning strategy for the conclusion. Thus, proofs, as results of truth-seeking games, can be seen
Notes de l’auteur
Une version très préliminaire des résultats de la section 3 a été présentée lors du septième workshop ”Games in Logic, Language and Computation” organisé à Amsterdam le 28 novembre 2002. Je remercie Serge Bozon et Jacques Dubucs pour leurs suggestions fécondes.
Texte intégral
Texte intégral en libre accès disponible depuis le 15 juin 2011.
Pour citer cet article
Référence électronique
Denis Bonnay, « Preuves et jeux sémantiques », Philosophia Scientiæ [En ligne], 8-2 | 2004, mis en ligne le 15 juin 2011, consulté le 22 mai 2013. URL : http://philosophiascientiae.revues.org/567 ; DOI : 10.4000/philosophiascientiae.567
Haut de page