A ternary frame is a set together with a ternary relation on ; we write when holds of three elements .
We may additionally ask that have a partial ordering; in this case we demand the compatibility condition that if and , , and , then also .
We can model logic using a ternary frame with a “forcing” or “satisfaction” relation between points of and formulas. We begin by assigning to each atomic formula? a set of points of which satisfy it. If 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:
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.
We can impose properties or structure on the ternary frame to affect the logic. For instance, if implies , 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.
A truth set in an ordered ternary frame is a subset such that if and only if there exists a with . Alternatively, given an unordered ternary frame and a subset , we could define in this way, and then require as a property of that the resulting relation is a partial order.
If is a truth set, then it makes sense to define
One way to model negation (and thereby obtain negative falsity and negative disjunction by duality from positive truth and positive conjunction ) is with a compatibility relation, which is just a binary relation . If has a partial order, we demand additionally that if and and , then .
Given such a , we define
Negation can alternatively be modeled using a false set. Suppose given a subset , to be the interpretation of the negative falsity :
We can then, if we wish, interpret negation and negative disjunction by defining and .
The latter is most sensible if negation is involutive, which it need not be in general — that is, if we need not have . 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 , , , and with their double-negation closure. This is commonly done in the phase space semantics for linear logic (see below).
Since the models above associate to formulas subsets of , it seems natural to describe them in a purely algebraic way using structure on the powerset of . In the case when is a poset, instead of the powerset of we must use the set of up-closed subsets of . Since this subsumes the unordered case (use the discrete ordering), we henceforth assume to be a poset, with having the assumed compatibility relation.
In fact, this axiom (which we repeat here for the reader’s convenience):
Therefore, by Day convolution, induces a binary tensor product on the -enriched presheaf category , which is precisely the poset of up-closed sets in . This tensor product is precisely the above interpretation of . 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 are just the categorical product and coproduct in . Similarly, that of and are the initial and terminal objects.
A truth set corresponds to a profunctor which is a unit for the pro-multiplication . Therefore, in this case the tensor product on has a unit object, which is precisely , the interpretation of the positive truth .
If we were to additionally add the assumption that is associative, in the sense that
… compatibility relations, satisfying some axioms, should make *-autonomous…
If is a magma with multiplication , then we can make it a ternary frame by defining to mean . More generally, if is a poset equipped with a binary multiplication , we can make it an ordered ternary frame by defining to mean .
If has a unit object , then (in the unordered case) or (in the ordered case) is a truth set.
In the special case when is a commutative monoid equipped with a “false set” as above (usually written ) in this context, this semantics for linear logic is called phase space semantics. It is usually expressed in terms of the quantale 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 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
and obtain 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 , where is the unit element of the monoid .