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{\u0131}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.

@article{PHSC_2004__8_2_105_0, 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 = {http://archive.numdam.org/item/PHSC_2004__8_2_105_0/} }

Bonnay, Denis. Preuves et jeux sémantiques. Philosophia Scientiae, Volume 8 (2004) no. 2, pp. 105-123. http://archive.numdam.org/item/PHSC_2004__8_2_105_0/