An Indexed System for Multiplicative Additive Polarized Linear Logic

We present an indexed logical system MALLP( I) for Laurent's multiplicative additive polarized linear logic ( MALLP ) [14]. The system is a polarized variant of Bucciarelli-Ehrhard's indexed system for multiplicative additive linear logic [4]. Our system is derived from a web-based instance of Hamano-Scott's denotational semantics [12] for MALLP . The instance is given by an adjoint pair of right and left multi-pointed relations. In the polarized indexed system, subsets of indexes for Iwork as syntactical counterparts of families of points in webs. The rules of $\sf MALLP({\it I})$ describe (in a proof-theoretical manner) the denotational construction of the corresponding rules of MALLP . We show that $\sf MALLP({\it I})$ faithfully describes a denotational model of MALLP by establishing a correspondence between the provability of indexed formulas and relations that can be extended to (non-indexed) proof-denotations.