nLab ternary frame

Ternary frames

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.

The construction generalizes from posets to categories using the Day convolution of a promonoidal category (see below), or a “promagmal category” in the weakest version.

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 \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.
  • xPQx \Vdash P \multimap Q (the one-sided linear implication) if and only if for all y,zy,z, if RxyzR x y z and yPy\Vdash P, then zQz\Vdash Q.
  • xQPx \Vdash Q ⟜ P (the dual linear implication) if and only if for all y,zy,z, if RxyzR x y z and zPz\Vdash P, then yQy\Vdash Q.

The logic obtained thereby will generally be substructural: it need not satisfy the structural rules like weakening, contraction, exchange or even associativity and unit for the tensor product. 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, and if and only if there exists an sTs\in T with RxsyR x s y. (If RR is commutative, as above, then the two conditions are equivalent.) 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 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.

A false set FF is of course just an arbitrary object of this quantale. Closing up under double-negation means restricting to the sub-poset of elements that are equal to their “double dual” x=(xF)Fx = (x \multimap F) \multimap F. Since the self-adjunction (F)(-\multimap F) is idempotent, this sub-poset is itself a quantale, and indeed a *-autonomous one.

The quantale-theoretic content of a compatibility relation is somewhat trickier: as defined it is a profunctor from AA to itself, whereas the negation of a pro-**-autonomous poset would be a profunctor from A opA^{op} to AA. (This would induce a functor (2 A) op2 A(\mathbf{2}^A)^{op} \to \mathbf{2}^{A} due to the special property that 22 op\mathbf{2}\cong \mathbf{2}^{op}.) Moreover, the definition of x¬Px \Vdash \neg P for a compatibility relation is also the (metatheoretic) negation of the map on 2 A\mathbf{2}^A that would be induced profunctorially. If we put these together, we can see that negation ought to be the the composite of the map 2 A2 A\mathbf{2}^A \to \mathbf{2}^A induced by the profunctor CC with the isomorphism 2 A(2 A op) op\mathbf{2}^A \cong (\mathbf{2}^{A^{op}})^{op} (using again that 22 op\mathbf{2}\cong \mathbf{2}^{op}). At least if AA is discrete, so that AA opA\cong A^{op}, then this has the correct domain and codomain, so we should be able to assert an axiom ensuring that it makes 2 A\mathbf{2}^A **-autononmous.

To be completed…

Generalizations

The quantale-theoretic viewpoint suggests a generalization replacing 2\mathbf{2} by any other quantale. That is, for any quantale QQ, we can define a notion of “QQ-valued ternary frame” that generates a new quantale by Day convolution. Everything goes through without significant change, except that compatibility relations seem to require QQ itself to be **-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={x|tx}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 semantics (see there for more). 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.

PCAs

If AA is a partial combinatory algebra (PCA), we can make it a ternary frame by defining RxyzR x y z to mean that xyx \cdot y is defined and equals zz. (Similarly, if AA is an ordered PCA we can make it an ordered ternary frame.) The resulting interpretation of \multimap almost coincides with the usual interpretation of implication in realizability over AA, and the combinators k,sk,s have the property that kP(QP)k \Vdash P \multimap (Q \multimap P) and s(PQR)(PQ)PRs \Vdash (P \multimap Q \multimap R) \multimap (P \multimap Q) \multimap P \multimap R for any P,Q,RP,Q,R, as would be expected from typed combinatory logic.

References

  • R. Routley and R.K. Meyer, The Semantics of Entailment I, Truth, Syntax and Modality, ed. H. Leblanc, North-Holland Publishing Company (Amsterdam), pp. 199-243. (1973)

  • R. Routley and R.K. Meyer, The Semantics of Entailment, II-III. Journal of Philosophical Logic, 1, 53-73 and 192-208. (1972)

  • Natasha Kurtonina, Frames and Labels - A modal analysis of categorial inference. Ph.D. Thesis, Institute of Logic, Language and Information (ILLC), Amsterdam, 1994

  • J. M. Dunn and R. K. Meyer, Combinators and Structurally Free Logic. Logic journal of the IGPL, 5(4):505-538, July 1997

  • Greg Restall, An introduction to substructural logic. Routledge, 2000.

Last revised on March 15, 2024 at 10:56:27. See the history of this page for a list of all contributions to it.