Propositional games with explicit strategies

This paper presents a game semantics for LP, Artemov’s Logic of Proofs. The language of LP extends that of propositional logic by adding formula-labeling terms, permitting us to take a term t and an LP formula A and form the new formula tA. We define a game semantics for this logic that interprets terms as winning strategies on the formulas they label, so tA may be read as “t is a winning strategy on A.” LP may thus be seen as a logic containing in-language descriptions of winning strategies on its own formulas.We apply our semantics to show how winnable instances of certain extensive games with perfect information may be embedded into LP. This allows us to use LP to derive a winning strategy on the embedding, from which we can extract a winning strategy on the original, non-embedded game. As a concrete illustration of this method, we compute a winning strategy for a winnable instance of the well-known game Nim.