Finite games for a predicate logic without contractions (Q1314388)

The author investigates a multiset calculus LS. LS is in fact equivalent to LC, a similar calculus for classical first-order predicate logic. LS is derived from LC by dropping the contraction rule that permits the inference \({A+ A\over A}\), that is, ``\(A\)'' may be derived from ``\(A\) or \(A\)''. It is known that LS is decidable, in the sense that it can always be determined whether a given formula is a theorem of LS or not. There is an intuitive game schema, whose rules are closely related to the rules of inference of LS, which associates to each formula \(A\) of LS a two-player zero-sum game \(G(A)\), with player 1 being the ``proponent'' and player 2 the ``opponent''. The main result is that \(A\) is a theorem of LS if and only if the proponent has a winning strategy in \(G(A)\). The main interest of this result seems to be that a very similar game \(G^c(A)\) can be constructed to relate provability in LC to the value of \(G^c\). The additional case that must be added to handle the contraction rule pinpoints closely the reason for the undecidability of LC. Some examples are given to emphasize this point.