Preuves et jeux sémantiques
Philosophia Scientiae, Volume 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 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 as effectively providing the needed winning strategies on the semantic games.

     author = {Bonnay, Denis},
     title = {Preuves et jeux s\'emantiques},
     journal = {Philosophia Scientiae},
     pages = {105--123},
     publisher = {\'Editions Kim\'e},
     volume = {8},
     number = {2},
     year = {2004},
     language = {fr},
     url = {}
AU  - Bonnay, Denis
TI  - Preuves et jeux sémantiques
JO  - Philosophia Scientiae
PY  - 2004
SP  - 105
EP  - 123
VL  - 8
IS  - 2
PB  - Éditions Kimé
UR  -
LA  - fr
ID  - PHSC_2004__8_2_105_0
ER  - 
%0 Journal Article
%A Bonnay, Denis
%T Preuves et jeux sémantiques
%J Philosophia Scientiae
%D 2004
%P 105-123
%V 8
%N 2
%I Éditions Kimé
%G fr
%F PHSC_2004__8_2_105_0
Bonnay, Denis. Preuves et jeux sémantiques. Philosophia Scientiae, Volume 8 (2004) no. 2, pp. 105-123.