nLab phase semantics

Phase semantics

Phase semantics

Idea

Girard’s phase semantics is a way of building star-autonomous posets with exponential modalities, hence models of classical linear logic.

Definition

Let MM be a commutative monoid, and M\bot\subseteq M a specified subset. (MM equipped with \bot is sometimes called a phase space.) Then PMP M, the powerset of MM, is a commutative quantale, with tensor product

XY={mnmXnY} X\otimes Y = \{ m n \mid m\in X \wedge n \in Y \}

and internal-hom

XY={mnX,mnY}. X\multimap Y = \{ m \mid \forall n \in X, m n \in Y \}.

Indeed, if we regard MM as a discrete poset, hence as a category enriched over 2={01}\mathbf{2} = \{0\le 1\}, then PMP M is its 2\mathbf{2}-enriched presheaf category, and this is its Day convolution monoidal structure.

Now \bot is an object of PMP M, hence induces a contravariant self-adjunction ()()(-\multimap\bot) \dashv (-\multimap \bot) of PMP M, which is idempotent since PMP M is a poset. We define a fact to be a fixed point of this adjunction, i.e. a subset XPMX\in P M of the form YY\multimap \bot, or equivalently such that X=(X)X = (X\multimap\bot)\multimap\bot.

Theorem

The poset of facts is star-autonomous.

Proof

It is closed under \multimap, since (X(Y))=(XY)(X\multimap (Y\multimap\bot)) = (X\otimes Y\multimap \bot). And it is reflective, with reflector ()(-\multimap\bot)\multimap\bot. Thus, it is closed symmetric monoidal with tensor product ((XY))((X\otimes Y)\multimap\bot)\multimap\bot. Since it also contains \bot, as =(I)\bot = (I\multimap \bot), it is therefore star-autonomous by construction.

The poset of facts is also, of course, a complete lattice, since it a reflective sub-poset of the complete lattice PMP M. In addition, it admits exponential modalities !! and ??. There are different ways to obtain these, but perhaps the simplest (see here) is to take

!X=((XIdem1)) !X = ((X \cap Idem \cap 1)\multimap\bot)\multimap\bot

where Idem={mmm=m}Idem= \{ m \mid m m = m \} is the set of idempotents in MM, and 1=({1})1 = (\{1\}\multimap\bot)\multimap\bot is the unit object of the monoidal category of facts.

Properties

Phase semantics is complete for provability in linear logic, i.e. if a sequent of linear logic is valid in the phase semantics for all choices of MM and \bot, then it is provable. This follows from a construction of a particular MM and \bot out of the syntax: let MM be the free commutative monoid on the formulas of linear logic subject to the relation that formulas of the form ?A?A are idempotent, and let \bot be the set of ΓM\Gamma\in M that are provable when regarded as one-sided sequents Γ\vdash\Gamma, and interpret a formula AA by the set of ΓM\Gamma\in M such that Γ,A\vdash \Gamma,A is provable. See Girard for details.

Generalizations

When phrased categorically as above, there is an obvious generalization to the case when MM is a commutative monoidal poset, with PMP M replaced by its 2\mathbf{2}-enriched presheaf category, i.e. the poset DMD M of downsets in MM. We can also generalize to other enrichments, although in that case the idempotence of the adjunction ()()(-\multimap\bot) \dashv (-\multimap \bot) is no longer automatic but has to be assumed.

If MM is assumed only to be a promonoidal 2\mathbf{2}-enriched category, i.e. equipped with a suitable relation M×MMM\times M ⇸ M, then it is a ternary frame. This can be used to construct models of more general substructural logics.

References

Last revised on January 31, 2018 at 22:00:36. See the history of this page for a list of all contributions to it.