A New Dialogical Semantics for Linear Logic

Shahid Rahman

Since the publication of Andreas Blass’ paper “A game semantic for linear logic” (1992) different dialogical systems for linear logic containing different sets of connectives have been developed (see for example the work of Samson Abramsky and Martin Hyland in Pitts/Dybjer 1997). Moreover, Jean-Yves Girard, the father of linear logic, claims in his more recent papers that the meaning of logical particles should be sought in the dialogical semantics which poses that the meaning of the logical rules resides in the rules themselves. Indeed, dialogical logic was conceived as a new, pragmatic way of understanding semantics which results from introducing in the realm of logic Wittgenstein’s view of meaning as use - understood as residing in the formulation of rules. Furthermore, the advantage of dialogical semantics for linear logic over other types of semantics can, according to Blass and Girard, be expressed by means of the following observation:

My thesis is that the meaning of logical rules is to be found in the well-hidden geometrical structure of the rules themselves: typically, negation should not be interpreted by NO, but by the exchange between Player and Opponent (Girard 1998, 1).

Now, on one hand, though Blass’ game semantics are very appealing they actually describe affine logic (where some type of weakening for the multiplicatives is still valid) instead of linear logic. On the other hand, Girard’s game semantics is rather complicated and the link to the semantic motivations is quite difficult to build. The aim of this paper is to give a new dialogical semantics for linear logic (without weakening for the multiplicatives) which connects linear with with several dialogical relevance logics developed recently by S. Rahman and H. Rückert and which, is able to capture the dynamics typical of linear logic including the change of roles induced by the negation. The idea is that arguments are not only sequences of steps in a proof; they also contain interactive steps, where information can be exchanged, retracted, collected or tested: In this context it sometimes makes sense not only to distinguish between redundant and non-redundant parts of the argument in question but also to establish how often one premise may be used. This leads to a dialogical semantics for linear logic in which in order to show the validity of this formula it is possible to use exactly once every part of it - including different occurrences of the same formula. Notice that in dialogical logic there is a very natural way to distinguish between different occurrences of a formula, namely every occurrence of a formula can be attached to a different move.

Address: FR 5.1 Philosophie Universität des Saarlandes, Pf. 151150, 66041 Saarbrücken, Germany

E-mail: s.rahman@rz-uni.sb.de