On phase semantics and denotational semantics: the exponentials Original Research Article

We extend to the exponential connectives of linear logic the study initiated in Bucciarelli and Ehrhard (Ann. Pure. Appl. Logic 102 (3) (2000) 247). We define an indexed version of propositional linear logic and provide a sequent calculus for this system. To a formula A of indexed linear logic, we associate an underlying formula View the MathML source of linear logic, and a family 〈A〉 of elements of View the MathML source, the interpretation of View the MathML source in the category of sets and relations. Then A is provable in indexed linear logic iff the family 〈A〉 is contained in the interpretation of some proof of View the MathML source. We extend to this setting the product phase semantics of indexed multiplicative additive linear logic introduced in Bucciarelli and Ehrhard (2000), defining the symmetric product phase spaces. We prove a soundness result for this truth-value semantics and show how a denotational model of linear logic can be associated to any symmetric product phase space. Considering a particular symmetric product phase space, we obtain a new coherence space model of linear logic, which is non-uniform in the sense that the interpretation of a proof of !A−∘B contains informations about the behavior of this proof when applied to “chimeric” arguments of type A (for instance: booleans whose value can change during the computation). In this coherence semantics, an element of a web can be strictly coherent with itself, or two distinct elements can be “neutral” (that is, neither strictly coherent, nor strictly incoherent).