Preuves et jeux sémantiques

National audienceHintikka 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 seenHintikka distingue entre deux types de jeux : les jeux qui ont trait à la constitution de la vérité, comme ceux qu'il utilise pour définir les conditions de vérité et de fausseté des formules de la logique du premier ordre et de la logique IF, et les jeux qui ont trait à la recherche de la vérité, comme les jeux de preuve. Il serait hautement désirable, d'un point de vue philosophique, d'établir une connexion entre ces deux types de jeux - ce point est développé dans la section 1. Moyennant une certaine modification des jeux de Hintikka, présentée dans la section 2 - le vérificateur est autorisé à reprendre ses coups - nous montrons, en adaptant des résultats de Thierry Coquand en théorie de la preuve, qu'il est possible d'établir un lien substantiel entre ces deux types de jeu. Nous proposons ainsi une sémantique des preuves pour la logique classique qui permet d'interpréter les preuves comme donnant des stratégies gagnantes sur des jeux sémantiques analogues aux jeux de Hintikka. Le résultat technique est présenté dans la section 3, tandis que les preuves sont rassemblées dans la section 4