\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{ternary frame}

\hypertarget{ternary_frames}{}\section*{{Ternary frames}}\label{ternary_frames}

\noindent\hyperlink{warning}{Warning}\dotfill \pageref*{warning} \linebreak
\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{modeling_substructural_logic}{Modeling substructural logic}\dotfill \pageref*{modeling_substructural_logic} \linebreak
\noindent\hyperlink{additional_structure}{Additional structure}\dotfill \pageref*{additional_structure} \linebreak
\noindent\hyperlink{truth_sets}{Truth sets}\dotfill \pageref*{truth_sets} \linebreak
\noindent\hyperlink{compatibility_relations}{Compatibility relations}\dotfill \pageref*{compatibility_relations} \linebreak
\noindent\hyperlink{falsity_sets}{Falsity sets}\dotfill \pageref*{falsity_sets} \linebreak
\noindent\hyperlink{from_ternary_frames_to_quantales}{From ternary frames to quantales}\dotfill \pageref*{from_ternary_frames_to_quantales} \linebreak
\noindent\hyperlink{generalizations}{Generalizations}\dotfill \pageref*{generalizations} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{phase_spaces}{Phase spaces}\dotfill \pageref*{phase_spaces} \linebreak
\noindent\hyperlink{pcas}{PCAs}\dotfill \pageref*{pcas} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{warning}{}\subsection*{{Warning}}\label{warning}

\emph{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]].}

\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A \textbf{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]].

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

A \textbf{ternary frame} is a set $A$ together with a ternary relation $R$ on $A$; we write $R x y z$ 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 $R x y z$ and $x'\le x$, $y'\le y$, and $z\le z'$, then also $R x' y' z'$.

\hypertarget{modeling_substructural_logic}{}\subsection*{{Modeling substructural logic}}\label{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:

\begin{itemize}%
\item $x \Vdash P \& Q$ (the negative [[conjunction]]) if and only if $x\Vdash P$ and $x\Vdash Q$.
\item $x \Vdash P \oplus Q$ (the positive [[disjunction]]) if and only if $x \Vdash P$ or $x\Vdash Q$.
\item $x \Vdash \mathbf{0}$ (the positive [[falsity]]) never.
\item $x \Vdash \top$ (the negative [[truth]]) always.
\item $x \Vdash P \multimap Q$ (the one-sided linear implication) if and only if for all $y,z$, if $R x y z$ and $y\Vdash P$, then $z\Vdash Q$.
\item $x \Vdash P \otimes Q$ (the positive conjunction) if and only if there exist $y,z$ such that $R y z x$ and $y\Vdash P$ and $z\Vdash Q$.

\end{itemize}
The logic obtained thereby will generally be [[substructural logic|substructural]]: it need not satisfy the structural rules like [[weakening rule|weakening]], [[contraction rule|contraction]], or even [[exchange rule|exchange]]. On this page, we have used the notation for substructural connectives from [[linear logic]].

\hypertarget{additional_structure}{}\subsection*{{Additional structure}}\label{additional_structure}

We can impose properties or structure on the ternary frame to affect the logic. For instance, if $R x y z$ implies $R 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.

\hypertarget{truth_sets}{}\subsubsection*{{Truth sets}}\label{truth_sets}

A \textbf{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 $R t x y$, and if and only if there exists an $s\in T$ with $R x s y$. (If $R$ is commutative, as above, then the two conditions are equivalent.) Alternatively, given an unordered ternary frame $A$ and a subset $T$, we could \emph{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

\begin{itemize}%
\item $x \Vdash \mathbf{1}$ (the positive truth) if and only if $x\in T$.

\end{itemize}
\hypertarget{compatibility_relations}{}\subsubsection*{{Compatibility relations}}\label{compatibility_relations}

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

Given such a $C$, we define

\begin{itemize}%
\item $x \Vdash \neg P$ if and only if for all $y$, if $x C y$ then not $y\Vdash P$.

\end{itemize}
\hypertarget{falsity_sets}{}\subsubsection*{{Falsity sets}}\label{falsity_sets}

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

\begin{itemize}%
\item $x\Vdash \bot$ if and only if $x\in F$.

\end{itemize}
We can then, if we wish, interpret negation and negative disjunction by defining $\neg P \coloneqq (P\multimap \bot)$ and $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 \Vdash \neg \neg P$ we need not have $x\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$, $\mathbf{1}$, and $\mathbf{0}$ with their double-negation closure. This is commonly done in the [[phase semantics]] for linear logic (see below).

\hypertarget{from_ternary_frames_to_quantales}{}\subsection*{{From ternary frames to quantales}}\label{from_ternary_frames_to_quantales}

Since the models above associate to formulas \emph{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):

\begin{itemize}%
\item if $R x y z$ and $x'\le x$, $y'\le y$, and $z\le z'$, then also $R x' y' z'$.

\end{itemize}
says precisely that $R$ is a $\mathbf{2}$-[[enriched category|enriched]] [[profunctor]] $A^{op} \times A^{op} &#8696; A^{op}$. (Here we are identifying posets with $\mathbf{2}$-enriched categories, where $\mathbf{2}$ is the [[interval category]].)

Therefore, by [[Day convolution]], $R$ induces a binary tensor product on the $\mathbf{2}$-enriched [[presheaf category]] $\mathbf{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 $\multimap$ and its dual.

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

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

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

\begin{itemize}%
\item there exists a $z$ with $R x y z$ and $R z u v$ if and only if there exists a $w$ with $R x w v$ and $R y u w$

\end{itemize}
then $A^{op}$ would become a [[promonoidal category|promonoidal]] poset, and hence $\mathbf{2}^A$ would be a complete and cocomplete closed monoidal poset, i.e. a [[quantale]].

A false set $F$ 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 = (x \multimap F) \multimap F$. Since the self-adjunction $(-\multimap F)$ is [[idempotent adjunction|idempotent]], this sub-poset is itself a quantale, and indeed a [[star-autonomous category|\emph{-autonomous]] one.}

The quantale-theoretic content of a compatibility relation is somewhat trickier: as defined it is a profunctor from $A$ to itself, whereas the negation of a pro-$*$-autonomous poset would be a profunctor from $A^{op}$ to $A$. (This would induce a functor $(\mathbf{2}^A)^{op} \to \mathbf{2}^{A}$ due to the special property that $\mathbf{2}\cong \mathbf{2}^{op}$.) Moreover, the definition of $x \Vdash \neg P$ for a compatibility relation is also the (metatheoretic) \emph{negation} of the map on $\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 $\mathbf{2}^A \to \mathbf{2}^A$ induced by the profunctor $C$ with the isomorphism $\mathbf{2}^A \cong (\mathbf{2}^{A^{op}})^{op}$ (using again that $\mathbf{2}\cong \mathbf{2}^{op}$). At least if $A$ is discrete, so that $A\cong A^{op}$, then this has the correct domain and codomain, so we should be able to assert an axiom ensuring that it makes $\mathbf{2}^A$ $*$-autononmous.

To be completed\ldots{}

\hypertarget{generalizations}{}\subsubsection*{{Generalizations}}\label{generalizations}

The quantale-theoretic viewpoint suggests a generalization replacing $\mathbf{2}$ by any other quantale. That is, for any quantale $Q$, we can define a notion of ``$Q$-valued ternary frame'' that generates a new quantale by Day convolution. Everything goes through without significant change, except that compatibility relations seem to require $Q$ itself to be $*$-autonomous.

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

\hypertarget{phase_spaces}{}\subsubsection*{{Phase spaces}}\label{phase_spaces}

If $A$ is a [[magma]] with multiplication $\cdot$, then we can make it a ternary frame by defining $R x y z$ 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 $R x y z$ to mean $x \cdot y \le z$.

If $\cdot$ has a unit object $t$, then $T = \{t\}$ (in the unordered case) or $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 $A$ is a commutative [[monoid]] equipped with a ``false set'' $F$ 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 $\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 \emph{facts}.

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

\begin{itemize}%
\item $x \Vdash !P$ if and only if $x$ belongs to the $\neg\neg$-closure of the set of all idempotents $y$ such that $y\Vdash P \& \mathbf{1}$.

\end{itemize}
and obtain $?P$ by duality.

Phase space semantics is \emph{complete} for [[linear logic]], in the sense that a formula is provable if and only if in any phase space semantics we have $1\vDash P$, where $1$ is the unit element of the monoid $A$.

\hypertarget{pcas}{}\subsubsection*{{PCAs}}\label{pcas}

If $A$ is a [[partial combinatory algebra]] (PCA), we can make it a ternary frame by defining $R x y z$ to mean that $x \cdot y$ is defined and equals $z$. (Similarly, if $A$ 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 $A$, and the combinators $k,s$ have the property that $k \Vdash P \multimap (Q \multimap P)$ and $s \Vdash (P \multimap Q \multimap R) \multimap (P \multimap Q) \multimap P \multimap R$ for any $P,Q,R$, as would be expected from typed [[combinatory logic]].

\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item R. Routley and R.K. Meyer, \emph{The Semantics of Entailment I}, Truth, Syntax and Modality, ed. H. Leblanc, North-Holland Publishing Company (Amsterdam), pp. 199-243. (1973)


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


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


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


\item Greg Restall, \emph{An introduction to substructural logic}. Routledge, 2000.



\end{itemize}
[[!redirects ternary frames]]



\end{document}