nLab
ternary frame

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 $A$ together with a ternary relation $R$ on $A$; we write $Rxyz$ when $R$ holds of three elements $x,y,z\in A$.

We may additionally ask that $A$ have a partial ordering; in this case we demand the compatibility condition that if $Rxyz$ and $x\prime \le x$, $y\prime \le y$, and $z\le z\prime$, then also $Rx\prime y\prime z\prime$.

Modeling substructural logic

We can model logic using a ternary frame with a “forcing” or “satisfaction” relation between points of $A$ and formulas. We begin by assigning to each atomic formula? a set of points of $A$ which satisfy it. If $A$ 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:

• $x⊩P\&Q$ (the negative conjunction) if and only if $x⊩P$ and $x⊩Q$.
• $x⊩P\oplus Q$ (the positive disjunction) if and only if $x⊩P$ or $x⊩Q$.
• $x⊩0$ (the positive falsity) never.
• $x⊩\top$ (the negative truth) always.
• $x⊩P⊸Q$ (the one-sided linear implication) if and only if for all $x,y,z$, if $Rxyz$ and $y⊩P$, then $z⊩Q$.
• $x⊩P\otimes Q$ (the positive conjunction) if and only if there exist $y,z$ such that $Ryzx$ and $y⊩P$ and $z⊩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 $Rxyz$ implies $Ryxz$, 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 $T\subseteq A$ such that $x\le y$ if and only if there exists a $t\in T$ with $Rtxy$. Alternatively, given an unordered ternary frame $A$ and a subset $T$, we could define $x\le y$ in this way, and then require as a property of $T$ that the resulting relation is a partial order.

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

• $x⊩1$ (the positive truth) if and only if $x\in T$.

Compatibility relations

One way to model negation (and thereby obtain negative falsity $\perp$ and negative disjunction $⅋$ by duality from positive truth $1$ and positive conjunction $\otimes$) is with a compatibility relation, which is just a binary relation $C$. If $A$ has a partial order, we demand additionally that if $xCy$ and $x\prime \le x$ and $y\le y\prime$, then $x\prime Cy\prime$.

Given such a $C$, we define

• $x⊩\neg P$ if and only if for all $y$, if $xCy$ then not $y⊩P$.

Falsity sets

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

• $x⊩\perp$ if and only if $x\in F$.

We can then, if we wish, interpret negation and negative disjunction by defining $\neg P≔(P⊸\perp )$ and $P⅋Q≔\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⊩\neg \neg P$ we need not have $x⊩P$. One solution to this (if we want negation to be involutive) is to close up $⊩$ under double-negation. This entails replacing the clauses defining the interpretation of the positive connectives $\otimes$, $\oplus$, $1$, and $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 $A$, it seems natural to describe them in a purely algebraic way using structure on the powerset of $A$. In the case when $A$ is a poset, instead of the powerset of $A$ we must use the set of up-closed subsets of $A$. Since this subsumes the unordered case (use the discrete ordering), we henceforth assume $A$ to be a poset, with $R$ having the assumed compatibility relation.

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

• if $Rxyz$ and $x\prime \le x$, $y\prime \le y$, and $z\le z\prime$, then also $Rx\prime y\prime z\prime$.

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

Therefore, by Day convolution, $R$ induces a binary tensor product on the $2$-enriched presheaf category $2^A$, which is precisely the poset of up-closed sets in $A$. 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 $⊸$ and its dual.

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

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

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

• there exists a $z$ with $Rxyz$ and $Rzuv$ if and only if there exists a $w$ with $Rxwv$ and $Ryuw$

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

… compatibility relations, satisfying some axioms, should make $2^A$ *-autonomous…

Examples

Phase spaces

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

If $\cdot$ has a unit object $t$, then $T=\{t\}$ (in the unordered case) or $T=\{x\mid 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 $A$ is a commutative monoid equipped with a “false set” $F$ as above (usually written $\perp$) in this context, this semantics for linear logic is called phase space semantics. It is usually expressed in terms of the quantale $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⊩!P$ if and only if $x$ belongs to the $\neg \neg$-closure of the set of all idempotents $y$ such that $y⊩P\&1$.

and obtain $?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 $1\models P$, where $1$ is the unit element of the monoid $A$.