A constructive game semantics for the language of linear logic Original Research Article

I present a semantics for the language of first-order additive-multiplicative linear logic, i.e. the language of classical first-order logic with two sorts of disjunction and conjunction. The semantics allows us to capture intuitions often associated with linear logic or constructivism such as sentences = games, sentences = resources or sentences = problems, where “truth” means existence of an effective winning (resource-using, problem-solving) strategy. The paper introduces a decidable first-order logic ET in the above language and gives a proof of its soundness and completeness (in the full language) with respect to this semantics. Allowing noneffective strategies in the latter is shown to lead to classical logic. The semantics presented here is very similar to Blassʹs game semantics (A. Blass, “A game semantics for linear logic”, Ann. Pure Appl. Logic 56). Although there is no straightforward reduction between the two corresponding notions of validity, my completeness proof can likely be adapted to the logic induced by Blassʹs semantics to show its decidability (via equality to ET), which was the main problem left open in Blassʹs paper. The reader needs to be familiar with classical (but not necessarily linear) logic and arithmetic.