On Faithfulness of Categorical Semantics for Polarized MALL
Masahiro Hamano
In the first part of this talk, we present a categorical model
for O. Laurent's Multiplicative Additive Polarized Linear Logic (MALLP)
by using adjunctions between positive and negative subcategories
of Barr's pre *-autonomous framework. We shall see several concrete
examples (hypercoherences, chu spaces, iterated double gluing)
and show some weakly full (Lauchli style) as well as
full completeness theorems for the multiplicative fragment.
So far almost all known concrete examples are not faithful
(though non degenerate) in that they cannot distinguish certain
distinct proofs of the same type. In a second part, we present
a construction to yield finer models from them so as to distinguish
these proofs. For this, we interpret polarity shiftings via additives
in a pre *-autonomous category so that each object is equipped
with permutations wrt these additives. Morphisms in positive/negative
subcategories are obtained by imposing certain invariance conditions under
the permutations. Then a quotient category (by a congruence on these
permutations) becomes a categorical model for MALLP. We also discuss
how to lift a (non faithful) full completeness theorem
in base categories into a faithful full completeness through the
construction.
This is joint work with Phil Scott.