\documentstyle[11pt,fullpage]{article}
\input{macros}
\newcommand{\la}{\mbox{$-\!\circ$}}     % Linear Arrow
\newcommand{\bla}{\mbox{$\circ\!-$}}    % Backwards Linear Arrow
%\newcommand{\Par}{\,{\parfont P}\,}    % Par (font)
\newcommand{\Par}{{\mbox{\raisebox{.4ex}{$\wp$}}}} % Par (gross)
\newcommand{\with}{\mbox{\,{\&}\,}}     % With (Additive And) (&)
\newcommand{\lplus}{\mbox{$\oplus$}}    % oplus
\newcommand{\tensor}{\mbox{$\otimes$}}  % Tensor (Multiplicative And)
\newcommand{\one}{\mbox{$1$}}           % 1
\newcommand{\zero}{\mbox{$0$}}          % 0
\renewcommand{\bottom}{\mbox{$\bot$}}     % bottom
\newcommand{\ltop}{\mbox{$\top$}}       % top

\begin{document}
\begin{center}
{\Large\bf Phase Semantics }\\
CS 358, Spring 1995 \\
April 26 Lecture\\
John Mitchell
\end{center}
\vskip 2ex


\section{Phase Space and Multiplicatives}

A \i{monoid} $\s{M}$ consists of a set $M$, 
associative binary operation $\cdot$ and unit $1 \el M$ with 
$1 \cdot x = x \cdot 1 = 1$ for all $x \el M$.
We generally omit the binary operation
$\,\cdot\,$ and write $xy$ for $x \cdot y$.

A \i{phase space} consists of a commutative monoid 
$\s{M} = \tuple{M,\,\cdot\,,1}$
and a chosen subset $\bottom \subs M$.
We interpret formulas of linear
logic as particular subsets of $M$ called \q{facts,} 
identified below, using the following operations 
\[
\begin{array}{lll}
XY &=& \set{xy}{x\el X\mbox{ and }y\el Y}\\
X \la Y &=& \set{z \el M}{zx\el Y \mbox{ all } x \el X}\\
X^\perp &=&  X \la \bottom\\
X \tensor Y &=& (XY)^{\perp\perp}\\
X \Par Y &=& (X^\perp \tensor Y^\perp)^\perp 
= (X^\perp Y^\perp)^\perp 
\quad\quad \mbox{\small (see below)}
\end{array}
\]
A subset $X \subs M$ is a \i{fact}
if $X^{\perp\perp} = X$.
We say a fact $X$ is \i{valid} if $1 \el X$.

\vskip 1ex\noindent
\b{Straightforward properties:}
\begin{quote}\noindent
1. For any $X,Y \subs M$, if $X \subs Y$, then $Y^\perp\subs X^\perp$.\\
2. For any $X \subs M$,we have $X \subs X^{\perp\perp}$.\\
3. Any $X^\perp$ is a fact since $X^{\perp\perp\perp} = X^\perp$.\\
4. $\bottom$ is a fact since $\bottom = \{1\}^\perp$.\\
5. The intersection of any collection of facts is a fact.\\
6. $X^{\perp\perp}$ is the smallest fact containing $X$.
\end{quote}

Associativity and commutativity of the connectives (other than $\la$)
follows from the associativity and commutativity of the underlying
monoid.  For associativity of $\tensor$, 
we use $(X \tensor Y) \tensor Z = (X \tensor Y \tensor Z)^{\perp\perp}$.
This follows from the following lemma.

\vskip 1ex
\noindent{\bf Lemma:}
For any $X, Y \subs M$, we have
$X^{\perp\perp}Y^{\perp\perp} \subs (XY)^{\perp\perp}$.

\vskip 1ex
\noindent{\bf Proof:}
Suppose $a \el X^{\perp\perp}$, $b \el Y^{\perp\perp}$ and
$c \el (XY)^{\perp}$. We must show that $abc = cba \el \bottom$.
Since $c \el (XY)^{\perp}$,  we know that if $x \el X$ and $y \el Y$,
then $cxy \el \bottom$. It follows that 
$cx \el Y^\perp = Y^{\perp\perp\perp}$ and 
therefore $cxb \el \bottom$.
By similar reasoning, we can use $cxb \el \bottom$
and commutativity to show 
$cb \el X^\perp = X^{\perp\perp\perp}$ and
therefore conclude $cba \el \bottom$.
\qed


The remaining constants of linear logic are interpreted as the
following facts:
\[
\begin{array}{lll}
\b{1} &=& \bottom^\perp \\
\top &=& \ns^\perp \quad( = M) \\
\b{0} &=& \top^\perp \\
\end{array}
\]

A number of expected identities are relatively easy to
check for all facts $X,Y,Z \subs M$. 
\[
\begin{array}{cc}
\mbox{\quad\quad\quad}
X \tensor Y = (X^\perp \Par Y^\perp)^\perp 
\mbox{\quad\quad\quad}& 
\mbox{\quad\quad\quad}
X \la     Y = X^\perp \Par Y 
\mbox{\quad\quad\quad}\\
X \Par Y = (X^\perp \tensor Y^\perp)^\perp &
X \la     Y = (X \tensor Y^\perp)^\perp\\
X \Par Y = X^\perp \la Y &
X \tensor Y = (X \la Y^\perp)^\perp\\[2ex]

\bottom \Par X = X &
{\bf 1} \tensor X = X \\

{\bf 1} \la X = X &
X \la \bottom = X^\perp 
\end{array}
\]
\vskip 1ex\noindent
{\bf Exercise}\\
1. Show that if $\ts \Gamma$, then the interpretation of $\Gamma$
in any phase space is a valid fact. A propositional letter may be
assigned any fact, and a sequent $\Gamma = A_1, \ldots, A_k$ is
interpreted as the  par of its formulas, $A_1 \Par \ldots \Par A_k$. 

\section{Examples}

\subsection{Integer phase space}

An easy phase space is the monoid $\tuple{\s{Z}, +, 0}$
of  integers with addition with $\bottom = \{0\}$.
Here we have 
\[
\begin{array}{lll}
XY &=& \set{x+y}{x\el X\mbox{ and }y\el Y}\\
X \la Y &=& \set{z \el M}{z+x\el Y \mbox{ all } x \el X}\\
X^\perp &=&  X \la \bottom = \set{y}{\fa x \el X.\, x+y = 0}
\end{array}
\]
In many cases, $X \la Y$ is empty.
For example,
\[
\begin{array}{lll}
\{1,2\} \la \{2,4\} &=& \set{x}{x+1 = 2 \mbox{ and } x+2=4} = \ns\\
\{1,2\} \la \{0\} &=& \set{x}{x+1 = 0 \mbox{ and } x+2=0} = \ns
\end{array}
\]
More generally, if $X$ has more than one element, 
then $X^\perp$ is empty and the smallest fact $X^{\perp\perp}$
containing $X$ is $\s{Z}$.
Therefore, the only facts are $\ns$, singletons, and $\s{Z}$, with
\[
\ns^\perp = \s{Z}\quad\quad
\{x\}^\perp  = \{-x\}^\perp \quad\quad
\s{Z}^\perp = \ns
\]
For the other connectives, we have
\[
\begin{array}{lll}
X \tensor Y &=& (XY)^{\perp\perp} = 
\left\{ \begin{array}{ll}
\s{Z} & \mbox{if } X=\s{Z} \mbox{ and } Y\ne\ns \\
\{x+y\} & \mbox{if } X=\{x\} \mbox{ and } Y=\{y\} \\
\ns & \mbox{if } X=\ns \mbox{ or } Y=\ns 
\end{array}\right.
\\
X \Par Y &=& (X^\perp \tensor Y^\perp)^\perp 
= X \tensor Y 
\end{array}
\]
This is therefore a largely degenerate phase space.

\subsection{Phase space of sequents}

We can construct a phase space of sequents using the
free commutative monoid 
$\s{M} = \tuple{M, \cdot, \epsilon}$ where $M$ is the
set of multisets of formulas (or, sequences modulo 
commutativity), $\cdot$ is concatenation
and $\epsilon$ is the empty multiset.
We let $\bottom = \set{\Gamma}{\ts \Gamma}$.

If $\Gamma$ is a multiset, then 
\[
\i{Pr}(\Gamma) = \set{\Sigma}{\ts \Gamma,\Sigma}
\]
is a fact.

If we associate each propositional symbol $P$ with
the fact $\i{Pr}(P)$, then we can show by induction
that the meaning of a formula $A$ is
$\i{Pr}(A)$.

Since $\epsilon \el \i{Pr}(A)$ means
$\ts A$, we can prove completeness using this 
phase space.

\vskip 1ex\noindent
{\bf Exercises}\\
2. Show that each $\i{Pr}(\Gamma)$ is a fact.\\
3. Complete the induction that the meaning of any 
formula $A$ is $\i{Pr}(A)$.

\section{Additives}

We can extend the interpretation of formulas, soundness and
completeness to additive connectives using
\[
\begin{array}{lll}
X \with Y &=& X \intersect Y\\
X \oplus Y &=& (X \union Y)^{\perp\perp}
\end{array}
\]

\vskip 1ex\noindent
{\bf Exercise}\\
4. Check your favorite laws involving additives.
For example, 
$X \with Y = (X^\perp \oplus Y^\perp)^\perp$ and
$X \oplus Y = (X^\perp \with Y^\perp)^\perp$,
or maybe commutativity, associativity or
units $\top \with X = X$ and $\b{0} \oplus X = X$.

\section{Modalities (Exponentials)}

A \i{topolinear space} $\s{P} = \tuple{\s{M}, \bottom, \s{F}}$
consists of a phase space $\s{M}, \bottom$ and a set $\s{F}$ of
facts of the phase space satisfying the following conditions:
\begin{quote}\noindent
(i) $\s{F}$ is closed under arbitrary \i{with} ($\with$)\\
(ii) $\s{F}$ is closed under finite \i{par} ($\Par$)\\
(iii) $\bottom$ is the smallest fact in $\s{F}$
(under the subset order)\\
(iv) $\Par$ is idempotent on $\s{F}$, \ie,
$F \Par F = F$ for all $F \el \s{F}$.
\end{quote}
The elements of $\s{F}$ are called the \i{closed facts} of $\s{P}$.
If $X \el \s{F}$, then $X^\perp$ is called an \i{open fact.}

The modal operators are interpreted in a topolinear space by
\[
\begin{array}{lll}
!X  &=& \mbox{the largest open fact } F \subs X\\
?X  &=& \mbox{the smallest closed fact } F \supseteq X
\end{array}
\]

\section{Quantifiers}

See Lafont and Scedrov, 
The undecidability of second-order multiplicative
linear logic.


\end{document}
