Preuves et jeux sémantiques

Bonnay, Denis

Philosophia Scientiae, Tome 8 (2004) no. 2, pp. 105-123.

Hintikka makes a distinction between two kinds of games: truth-constituting 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 $\exists lo\ddot{ı}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 as effectively providing the needed winning strategies on the semantic games.