Game semantics for the Lambek-calculus: Capturing directionality and the absence of structural rules (Q1005955)

In the paper, a game semantics for the associative Lambek calculus \(L\) is proposed. Following [\textit{M. H. Sørensen} and \textit{P. Urzyczyn}, Lectures on the Curry-Howard isomorphism. Studies in Logic and the Foundations of Mathematics 149. Amsterdam: Elsevier (2006; Zbl 1183.03004)], the authors introduce a game semantics for the implicational fragment of intuitionistic propositional calculus (IIPC). The semantics defines a game over \((\Gamma, \varphi),\) where \(\Gamma=\{\varphi_1,\ldots, \varphi_n \}\) is a set of well-formed IIPC formulas (wffs) and \(\varphi\) is a metavariable ranging over the wffs, as a dialogue between two players. The first player, called Prover, wants to produce a witness derivation establishing \(\vdash_{\text{IIPC}} \Gamma \triangleright \varphi.\) The second player, called Skeptic, wants to establish non-derivability of \(\varphi\) from \(\Gamma\) in IIPC. The game starts when the Prover makes an assertion. In answer, the Skeptic can challenge the assertion, presenting a set of well-formed formulas that the Prover may assume derivable. The prover must meet the challenge using the offers offered so far or by introducing new assertions. The Skeptic may challenge any of these assertions but one only. The game ends when the player who is up has no response (then the other player wins) or it may go on foreover (the Skeptic wins). A winning strategy for the Prover over the game \((\Gamma, \varphi)\) is a finite labelled tree composed from nodes corresponding to the Prover or the Skeptic moves in the game and satisfying some conditions. Generalizing a result of Sørensen and Urzyczyn [loc. cit.], the authors prove that there is a winning strategy for the game \((\Gamma, \varphi)\) if and only if \(\vdash_{\text{IIPC}} \Gamma \triangleright \varphi.\) Applying a similar reasoning, they prove the main result of the paper saying that there is a winning Prover strategy for \((\Gamma, \varphi)\) if and only if \(\vdash_{L} \Gamma \triangleright \varphi.\)