nLab
ternary frame

Ternary frames

Warning

The term ‘frame’ is used in a different sense here than in geometric logic; see frame. The usage here is analogous to Kripke frames in modal logic.

Idea

A ternary frame is a way of presenting a model for a substructural logic (such as linear logic and relevant logic?) in terms of a set of “worlds” or “states of information” and a ternary relation.

Definition

A ternary frame is a set AA together with a ternary relation RR on AA; we write RxyzR x y z when RR holds of three elements x,y,zAx,y,z\in A.

We may additionally ask that AA have a partial ordering; in this case we demand the compatibility condition that if RxyzR x y z and xxx'\le x, yyy'\le y, and zzz\le z', then also RxyzR x' y' z'.

Modeling substructural logic

We can model logic using a ternary frame with a “forcing” or “satisfaction” relation between points of AA and formulas. We begin by assigning to each atomic formula? a set of points of AA which satisfy it. If AA has a partial order, as above, then we ask each of these sets to be up-closed.

The logical connectives can then be defined inductively by clauses such as the following:

  • xP&Qx \Vdash P \& Q (the negative conjunction) if and only if xPx\Vdash P and xQx\Vdash Q.
  • xPQx \Vdash P \oplus Q (the positive disjunction) if and only if xPx \Vdash P or xQx\Vdash Q.
  • x0x \Vdash \mathbf{0} (the positive falsity) never.
  • xx \Vdash \top (the negative truth) always.
  • xPQx \Vdash P \multimap Q (the one-sided linear implication) if and only if for all x,y,zx,y,z, if RxyzR x y z and yPy\Vdash P, then zQz\Vdash Q.
  • xPQx \Vdash P \otimes Q (the positive conjunction) if and only if there exist y,zy,z such that RyzxR y z x and yPy\Vdash P and zQz\Vdash Q.

The logic obtained thereby will generally be substructural: it need not satisfy the structural rules like weakening, contraction, or even exchange. On this page, we have used the notation for substructural connectives from linear logic.

Additional structure

We can impose properties or structure on the ternary frame to affect the logic. For instance, if RxyzR x y z implies RyxzR y x z, then the logic we obtain will satisfy the exchange rule.

We also need additional structure in order to model positive truth, negative falsity, negative disjunction, and negation.

Truth sets

A truth set in an ordered ternary frame is a subset TAT\subseteq A such that xyx\le y if and only if there exists a tTt\in T with RtxyR t x y. Alternatively, given an unordered ternary frame AA and a subset TT, we could define xyx\le y in this way, and then require as a property of TT that the resulting relation is a partial order.

If TT is a truth set, then it makes sense to define

  • x1x \Vdash \mathbf{1} (the positive truth) if and only if xTx\in T.

Compatibility relations

One way to model negation (and thereby obtain negative falsity \bot and negative disjunction \parr by duality from positive truth 1\mathbf{1} and positive conjunction \otimes) is with a compatibility relation, which is just a binary relation CC. If AA has a partial order, we demand additionally that if xCyx C y and xxx'\le x and yyy\le y', then xCyx' C y'.

Given such a CC, we define

  • x¬Px \Vdash \neg P if and only if for all yy, if xCyx C y then not yPy\Vdash P.

Falsity sets

Negation can alternatively be modeled using a false set. Suppose given a subset FAF\subseteq A, to be the interpretation of the negative falsity \bot:

  • xx\Vdash \bot if and only if xFx\in F.

We can then, if we wish, interpret negation and negative disjunction by defining ¬P(P)\neg P \coloneqq (P\multimap \bot) and PQ¬(¬P¬Q)P\parr Q \coloneqq \neg (\neg P \otimes \neg Q).

The latter is most sensible if negation is involutive, which it need not be in general — that is, if x¬¬Px \Vdash \neg \neg P we need not have xPx\Vdash P. One solution to this (if we want negation to be involutive) is to close up \Vdash under double-negation. This entails replacing the clauses defining the interpretation of the positive connectives \otimes, \oplus, 1\mathbf{1}, and 0\mathbf{0} with their double-negation closure. This is commonly done in the phase space semantics for linear logic (see below).

From ternary frames to quantales

Since the models above associate to formulas subsets of AA, it seems natural to describe them in a purely algebraic way using structure on the powerset of AA. In the case when AA is a poset, instead of the powerset of AA we must use the set of up-closed subsets of AA. Since this subsumes the unordered case (use the discrete ordering), we henceforth assume AA to be a poset, with RR having the assumed compatibility relation.

In fact, this axiom (which we repeat here for the reader’s convenience):

  • if RxyzR x y z and xxx'\le x, yyy'\le y, and zzz\le z', then also RxyzR x' y' z'.

says precisely that RR is a 2\mathbf{2}-enriched profunctor A op×A opA opA^{op} \times A^{op} ⇸ A^{op}. (Here we are identifying posets with 2\mathbf{2}-enriched categories, where 2\mathbf{2} is the interval category.)

Therefore, by Day convolution, RR induces a binary tensor product on the 2\mathbf{2}-enriched presheaf category 2 A\mathbf{2}^A, which is precisely the poset of up-closed sets in AA. This tensor product is precisely the above interpretation of \otimes. By the usual Day convolution arguments, this tensor product functor has both left and right adjoints, which are precisely the interpretation of \multimap and its dual.

Of course, the interpretations of &\& and \oplus are just the categorical product and coproduct in 2 A\mathbf{2}^A. Similarly, that of 0\mathbf{0} and \top are the initial and terminal objects.

A truth set TT corresponds to a profunctor 1A op1 ⇸ A^{op} which is a unit for the pro-multiplication RR. Therefore, in this case the tensor product on 2 A\mathbf{2}^A has a unit object, which is precisely TT, the interpretation of the positive truth 1\mathbf{1}.

If we were to additionally add the assumption that RR is associative, in the sense that

  • there exists a zz with RxyzR x y z and RzuvR z u v if and only if there exists a ww with RxwvR x w v and RyuwR y u w

then A opA^{op} would become a promonoidal poset, and hence 2 A\mathbf{2}^A would be a complete and cocomplete closed monoidal poset, i.e. a quantale.

… compatibility relations, satisfying some axioms, should make 2 A\mathbf{2}^A *-autonomous

Examples

Phase spaces

If AA is a magma with multiplication \cdot, then we can make it a ternary frame by defining RxyzR x y z to mean xy=zx \cdot y = z. More generally, if AA is a poset equipped with a binary multiplication \cdot, we can make it an ordered ternary frame by defining RxyzR x y z to mean xyzx \cdot y \le z.

If \cdot has a unit object tt, then T={t}T = \{t\} (in the unordered case) or T={xtx}T = \{x | t \le x \} (in the ordered case) is a truth set.

Categorically, this corresponds to the usual way of regarding a monoidal category as a promonoidal category.

In the special case when AA is a commutative monoid equipped with a “false set” FF as above (usually written \bot) in this context, this semantics for linear logic is called phase space semantics. It is usually expressed in terms of the quantale 2 A\mathbf{2}^A obtained by Day convolution, but after passing to fixed points of the double-negation monad (in order to obtain an involutive negation). In this context, fixed points of ¬¬\neg\neg are referred to as facts.

It is also possible to interpret the exponential modalities !! and ?? of linear logic using phase space semantics. For instance, we can define

  • x!Px \Vdash !P if and only if xx belongs to the ¬¬\neg\neg-closure of the set of all idempotents yy such that yP&1y\Vdash P \& \mathbf{1}.

and obtain ?P?P by duality.

Phase space semantics is complete for linear logic, in the sense that a formula is provable if and only if in any phase space semantics we have 1P1\vDash P, where 11 is the unit element of the monoid AA.

Created on May 15, 2012 10:28:56 by Mike Shulman (71.136.228.203)