On phase semantics and denotational semantics: The exponentials (Q5939845)

An indexed version of propositional linear logic with exponentials is defined together with a sequent calculus for this system. To a formula \(A\) of indexed linear logic are associated: an underlying formula \(\underline{A}\) of linear logic, an interpretation \(|\underline{A}|\) of this formula in the category of sets and relations, and a family \(\langle A\rangle\) of elements of \(A\). Then \(A\) is provable in indexed linear logic iff the family \(\langle A\rangle\) is contained in the interpretation of some proof of \(\underline{A}\). To this setting the product phase semantics of indexed multiplicative additive linear logic (by the same authors) is extended (symmetric product phase spaces are defined). A soundness result is proved and it is shown how a denotational model of linear logic can be associated to any symmetric product phase space. On this basis a new coherence space model of linear logic is obtained. Some details to give an idea how indexed linear logic \(\text{LL}(I)\) is defined. Let \(I\) be an infinite denumerable set. Let \(J, K\) be two sets. A function \(u:J\rightarrow K\) is almost injective if, for any \(k\in K\), the set \(u^{-1}(k)\) is finite. Every formula \(A\) has a domain \(d(A)\subseteq I\). (\dots) If \(A, B\) are formulae of a domain \(J\subseteq I\) then \(A\otimes B\) is a formula of the domain \(J\). (Similarly for \(par\).) If \(A\) is a formula of a domain \(J\) and \(B\) is a formula of a domain \(K\), \(J\cap K=\emptyset\), then \(A\oplus B, A\& B\) are formulae of the domain \(J+K\) (the disjoint union of \(J\) and \(K\)). If \(A\) is a formula of a domain \(J\) and \(u:J\rightarrow K\) is an almost injective function then \(!_uA\) and \(?_uA\) are formulae of the domain \(K\) (\dots) For \(\text{LL}(I)\) a succedent-only sequent calculus is considered.