On phase semantics and denotational semantics in multiplicative–additive linear logic Original Research Article

We study the notion of logical relation in the coherence space semantics of multiplicative-additive linear logic View the MathML source. We show that, when the ground-type logical relation is “closed under restrictions”, the logical relation associated to any type can be seen as a map associating facts of a phase space to families of points of the web of the corresponding coherence space. We introduce a sequent calculus extension of View the MathML source whose formulae denote these families of points. This logic View the MathML source (where I is a set of indexes) admits a truth-value semantics in the previously mentioned phase space, and this truth-value semantics faithfully describes the logical relation model we started from. Then we generalize this notion of phase space, we prove a truth-value completeness result for View the MathML source and we derive from any phase model of View the MathML source a denotational model for View the MathML source. Using the truth-value completeness result, we obtain a weak denotational completeness result based on this new denotational semantics.