Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\section{Preliminaries}

\label{sect:preliminaries}

%

%\todo{consider removing and just have a section on linear logic, including free-cut elimination.}

%

%

%\paragraph*{Notation}

%Fix conventions here for use throughout:

%\begin{itemize}

%\item Eigenvariables: $a, b , c$.

%\item (Normal) variables: $u,v,w$. (only when distinction is important, e.g.\ $u^{!\nat}$).

%\item (Safe) variables: $x,y,z$. (as above, e.g.\ $x^\nat$.)

%\item Terms: $r,s,t$.

%\item Formulae: $A,B,C$.

%\item Atomic formulae: $p,q$.

%\item Free variables in a term, formula, sequent: $FV(u)$, $FV(A)$, $FV(\Gamma)$

%\item Sequents: $\Gamma, \Delta, \Sigma, \Pi$.

%\item lists of formulas $A(\vec{x})$, $!A(\vec{x})$ (in particular for $A=N$).

%\item Proofs: $\pi, \rho, \sigma$.

%\item Theories: $\mathcal T$. Sequent systems: $\mathcal S$.

%\end{itemize}

%

%\subsection{Linear logic}

%\anupam{use a system that is already in De Morgan form, for simplicity.}

%\anupam{Have skipped units, can reconsider this when in arithmetic. Also in affine setting can be recovered by any contradiction/tautology.}

We formulate linear logic without units with usual notation for the multiplicatives, additives and exponentials from \cite{Girard87}. We restrict negation to the atoms, thus formulae are always in De Morgan normal form, and this is reflected in the sequent system below. We have included rules for arbitrary weakening for working in affine settings.

%\anupam{positive and negative.}

\begin{definition}

%[Sequent calculus for linear logic]

%[Sequent calculus for affine linear logic]

\label{def:LLsequentcalculus}

The sequent calculus for (affine) linear logic is as follows:

\[

\small

\begin{array}{l}

\begin{array}{cccc}

\vlinf{\lefrul{\bot}}{}{p, \lnot{p} \seqar }{}

& \vlinf{\id}{}{p \seqar p}{}

& \vlinf{\rigrul{\bot}}{}{\seqar p, \lnot{p}}{}

& \vliinf{\cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta, A }{\Sigma, A \seqar \Pi}

\\

\noalign{\bigskip}

%\text{Multiplicatives:} & & & \\

%\noalign{\bigskip}

\vliinf{\lefrul{\lor}}{}{\Gamma,\Sigma, A \lor B \seqar \Delta, \Pi}{\Gamma, A \seqar \Delta}{\Sigma , B \seqar \Pi}

&

\vlinf{\lefrul{\land}}{}{\Gamma, A\land B \seqar \Delta}{\Gamma, A , B \seqar \Delta}

&

\vlinf{\rigrul{\lor}}{}{\Gamma \seqar \Delta, A \lor B}{\Gamma \seqar \Delta, A, B}

&

\vliinf{\rigrul{\land}}{}{\Gamma, \Sigma \seqar \Delta , \Pi , A \land B}{\Gamma \seqar \Delta , A}{\Sigma \seqar \Pi , B}

\\

\noalign{\bigskip}

%\text{Additives:} & & & \\

%\noalign{\bigskip}

\vliinf{\lefrul{\laor}}{}{\Gamma, A \laor B \seqar \Delta}{\Gamma , A \seqar \Delta}{\Gamma, B \seqar \Delta}

&

\vlinf{\lefrul{\laand}}{}{\Gamma, A_1\laand A_2 \seqar \Delta}{\Gamma, A_i \seqar \Delta}

&

%\vlinf{\lefrul{\laand}}{}{\Gamma, A\laand B \seqar \Delta}{\Gamma, B \seqar \Delta}

%\quad

\vlinf{\rigrul{\laor}}{}{\Gamma \seqar \Delta, A_1\laor A_2}{\Gamma \seqar \Delta, A_i}

&

%\vlinf{\rigrul{\laor}}{}{\Gamma \seqar \Delta, A\laor B}{\Gamma \seqar \Delta, B}

%\quad

\vliinf{\rigrul{\laand}}{}{\Gamma \seqar \Delta, A \laand B }{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, B}

\\

\noalign{\bigskip}

%\text{Exponentials:} & & & \\

%\noalign{\bigskip}

\vlinf{\lefrul{?}}{}{!\Gamma, ?A \seqar ?\Delta}{!\Gamma , A \seqar ?\Delta}

&

\vlinf{\lefrul{!}}{}{\Gamma, !A \seqar \Delta}{\Gamma, A \seqar \Delta}

&

\vlinf{\rigrul{?}}{}{\Gamma \seqar \Delta, ?A}{\Gamma \seqar \Delta, A}

&

\vlinf{\rigrul{!}}{}{!\Gamma \seqar ?\Delta, !A}{!\Gamma \seqar ?\Delta, A}

\\

\noalign{\bigskip}

%\text{Structural:} & & & \\

%\noalign{\bigskip}

%\vlinf{\lefrul{\wk}}{}{\Gamma, !A \seqar \Delta}{\Gamma \seqar \Delta}  %% linear logic weakening

\vlinf{\lefrul{\wk}}{}{\Gamma, A \seqar \Delta}{\Gamma \seqar \Delta}

&

\vlinf{\lefrul{\cntr}}{}{\Gamma, !A \seqar \Delta}{\Gamma, !A, !A \seqar \Delta}

&

%\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, ?A }{\Gamma \seqar \Delta}   %% linear logic weakening

\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, A }{\Gamma \seqar \Delta}

&

\vlinf{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, ?A}{\Gamma \seqar \Delta, ?A, ?A}

\\

\noalign{\bigskip}

\vlinf{\lefrul{\exists}}{}{\Gamma, \exists x . A(x) \seqar \Delta}{\Gamma, A(a) \seqar \Delta}

&

\vlinf{\lefrul{\forall}}{}{\Gamma, \forall x. A(x) \seqar \Delta}{\Gamma, A(t) \seqar \Delta}

&

\vlinf{\rigrul{\exists}}{}{\Gamma \seqar \Delta, \exists x . A(x)}{ \Gamma \seqar \Delta, A(t)}

&

\vlinf{\rigrul{\forall}}{}{\Gamma \seqar \Delta, \forall x . A(x)}{ \Gamma \seqar \Delta, A(a) } \\

%\noalign{\bigskip}

% \vliinf{mix}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta}{\Sigma \seqar \Pi} &&&

\end{array}

\end{array}

\]

where $p$ is atomic, $i \in \{ 1,2 \}$, $t$ is a term and the eigenvariable $a$ does not occur free in $\Gamma$ or $\Delta$.

\end{definition}

%\todo{$\limp$ abbreviation for ...}

%\todo{bracketing}

We do not formally include a symbol for implication but we sometimes write $A \limp B$ as shorthand for $\lnot{A} \lor B$, where $\lnot A$ is the De Morgan dual of $A$. We often omit brackets under associativity, and when writing long implications we assume the right-most bracketing.

We will use standard terminology to track formulae in proofs, as presented in e.g.\ \cite{Buss98:intro-proof-theory}.

In particular, each rule has a distinguished \textit{principal formula}, e.g.\

  $A \lor B$ in rule $\lefrul{\lor}$ (and similarly for all rules for connectives) and $?A$ in rule $\rigrul{\cntr}$, and \emph{active formulae}, e.g.\ $A$ and $B$ in $\lefrul{\lor}$ and so on. These induce the notions of (direct) descendants and ancestors in proofs, as in \cite{Buss98:intro-proof-theory}.

%The  \textit{direct ancestor} relation on occurrences of formulas in a proof is defined to keep track of identity of formulas from line to line, in the usual way.

  % Observe that we do not consider here any exchange rules, the sequence are made of multisets of formulas and exchanges are implicit. Note that this system is \textit{affine} in the sense that it includes general weakening rules $\rigrul{\wk}$ and  $\lefrul{\wk}$, while in linear logic   $\rigrul{\wk}$ (resp. $\lefrul{\wk}$) is restricted to formulas of the form $?A$ (resp. $!A$).   In the following though, by linear logic we will mean affine linear logic.

  \subsection{Theories and systems}

%  \anupam{need to add a note on semantics}

%  \anupam{mention equality rules}

%  \anupam{mention equality axioms and first-order theories and models at some point.}

 A \emph{language} is a set of nonlogical symbols (i.e.\ constants, functions, predicates) and a \emph{theory} a set of closed formulae over some language. We assume that all theories contain the axioms of equality:

% \[

% \begin{array}{rl}

%\refl & \forall x . x = x \\

%\symm & \forall x, y. (x = y \limp y = x )\\

%\trans & \forall x , y , z . ( x = y \limp y = z \limp x = z ) \\

%\subst_f & \forall \vec x , \vec y . (\vec x = \vec y \limp f(\vec x) = f(\vec y) ) \\

%\subst_P & \forall \vec x , \vec y. (\vec x = \vec y \limp P(\vec x) \limp P(\vec y)  )

% \end{array}

%\left\{

\begin{equation}

\label{eqn:equality-theory}

\begin{array}{l}

\forall x . x = x \quad, \quad \forall x, y. (x = y \limp y = x )\quad, \quad \forall x , y , z . ( x = y \limp y = z \limp x = z ) \\ \forall \vec x , \vec y . (\vec x = \vec y \limp f(\vec x) = f(\vec y) )  \quad , \quad \forall \vec x , \vec y. (\vec x = \vec y \limp P(\vec x) \limp P(\vec y)  )

\end{array}

\end{equation}

%\right\}

% \]

  where $\vec x = \vec y$ is shorthand for $x_1 = y_1 \land \vldots \land x_n = y_n$.

\newcommand{\init}{\mathit{init}}    

We consider \emph{systems} of `nonlogical' rules extending Dfn.~\ref{def:LLsequentcalculus}, which we write as follows,

 \[

 \begin{array}{cc}

  \vlinf{\init}{}{ \seqar A}{}  &  \vlinf{(R)}{}{ !\Gamma , \Sigma' \seqar \Delta' , ? \Pi  }{ \{!\Gamma , \Sigma_i \seqar \Delta_i , ? \Pi \}_{i \in I} }

\end{array}

\]

 where, in each rule $(R)$, $I$ is a finite possibly empty set (indicating the number of premises) and we assume the following conditions and terminology:

 \begin{enumerate}

 \item In $(R)$ the formulas of $\Sigma', \Delta'$  are called \textit{principal}, those of $\Sigma_i, \Delta_i$ are called \textit{active}, and those of   

$ !\Gamma,  ? \Pi$ are called \textit{context formulas}. In $\init$ $A$ is called a principal formula.

\item Each rule $(R)$ comes with a list $a_1$, \dots, $a_k$ of eigenvariables such that each $a_j$ appears in exactly one $\Sigma_i, \Delta_i$ (so in some active formulas of exactly one premise)  and does not appear in  $\Sigma', \Delta'$ or $ !\Gamma,  ? \Pi$.

    \item A system $\system$ of rules must be closed under substitutions of free variables by terms (where these substitutions do not contain the eigenvariables $a_j$ in their domain or codomain).  

   \item $ \Sigma'$ (resp. $\Delta'$) does not contain any formula of the shape $?A$ (resp. $!A$).  

 \end{enumerate}

%The distinction between modal and nonmodal formulae in $(R)$ induces condition 1

 Conditions 2 and 3 are actually standard for nonlogical rules, independently of the logical setting, c.f.\ \cite{Beckmann11}. Condition 2 reflects the intuitive idea that often we need in our nonlogical rules a notion of \textit{bound} variables in the active formulas (typically for induction rules), and the eigenvariables play this role. Condition 3 is needed for our proof system to admit elimination of cuts on quantified formulas. Condition 4 and the conventions of 1 is peculiar to our linear logic setting in order to carry out certain proof-theoretic manipulations, mainly free-cut elimination in Sect.~\ref{sect:free-cut-elim}.

%  

 Observe that $\init$ rules can actually be seen as particular cases of $(R)$ rules, with no premise, so in the following we will only consider $(R)$ rules.

%  \patrick{Anupam: note that I had to strengthen the conditions for the rules (R). Condition (1) is needed 

%  to be able to commute a cut with (R), in the case where this cut is with a principal formula of a   ($\rigrul{!}$) rule. 

%  

%  Condition (2) is a sufficient condition to avoid the following situation: cut between a principal formula in say $\Delta'$ in the conclusion of an (R) rule (left premise), and a context formula in $!\Gamma$ in the conclusion of another (R) rule (right premise). Indeed this is not an anchored cut in our sense, but we cannot eliminate it in general (because we cannot commute the cut with (R) up the right premise).

%  }

    To each theory $\theory$ we formally associate the system of $\init$ rules $\seqar A$ for each $A \in \theory$.\footnote{Notice that this naively satisfies condition 3 since theories consist of only closed formulae.}  A proof in such a system will be called a \textit{ $\mathcal T$-proof}, or just {proof} when there is no risk of confusion.

%    

%  

%  In what follows we will be interested in an example of theory  $\mathcal T$ which is a form of arithmetic.

%   Let us give an example of a possible nonlogical rule that appears later in Sect.~\ref{sect:arithmetic}:

%   

%   \[

%	\vliinf{\ind}{}{ !\word(t), !\Gamma , A(\epsilon) \seqar A(t) , ?\Delta }{!\Gamma , !\word(a), A(a) \seqar A(s_0 a ), ?\Delta }{ !\Gamma , !\word(a), A(a) \seqar A(s_1 a ), ?\Delta }

%\]

%

%So here we have $I=\{0,1\}$ (two premises), $\Sigma_i=!\word(a), A(a)$ and $\Delta_i= A(s_i a )$ for $i=0,1$, $\Sigma'= !\word(t), A(\epsilon)$, $\Delta'= A(t)$. So condition 2 is satisfied provided $a\notin FV(!\Gamma, ?\Delta)$ and $a \notin FV(t)$. 

%\[

%	\vliinf{}{(x \notin \FV(\Gamma, \Delta))}{ !\Gamma , A(\epsilon) \seqar A(t) , ?\Delta }{ !\Gamma , A(x) \seqar A(s_0 x ), ?\Delta }{ !\Gamma, A(x) \seqar A( s_1 x ) , ?\Delta}

%	\]

%  A proof in such a system will be called a \textit{ $\mathcal T$-proof}, or just \textit{proof} when there is no risk of confusion.

%   The rules of Def. \ref{def:LLsequentcalculus} are called \textit{logical rules} while the rules (ax) and (R) of $\mathcal T$  are called \textit{non-logical}.

%  

%  As usual rules come with a notion of \textit{principal formulas}, which are a subset of the rules in the conclusion, e.g.:

%  $A \lor B$ in rule $\lefrul{\lor}$ (and similarly for all rules for connectives); $?A$ in rule $\rigrul{\cntr}$; all conclusion formulas in axiom rules;

%   $\Sigma', \Delta'$ in rule (R).

% \anupam{15/04: add definitions of theories and systems, unions, rules vs axioms etc. and abuses of notation:

% 	sometimes use same symbol for theory and system if fixed in advance;

% 	sometimes coincide axiom with initial rule;

% 	}

\begin{remark}

	[Semantics]

	The models we consider are usual Henkin models, with linear connectives interpreted by their classical counterparts. Consequently, we do not have any completeness theorem for our theories, but we do have soundness.

\end{remark}

\subsection{Some basic proof-theoretic results}

We briefly survey some well-known results for theories of linear logic.

A rule is \emph{invertible} if each of its upper sequents is derivable from its lower sequent.

\begin{proposition}

[Invertible rules, folklore]

\label{prop:invertible-rules}

The rules $\lefrul{\land}, \rigrul{\lor}, \lefrul{\lor}, \rigrul{\land}, \lefrul{\exists}, \rigrul{\forall}$ are invertible.

\end{proposition}

We will typically write $\inv{c}$ to denote the inverse derivation for a logical symbol $c$.

%[cite Avron:`semantics and proof theory of linear logic']

%

%We will make much use of the deduction theorem, allowing us to argue informally within a theory for hypotheses that have been promoted.

%

%%$$

%%	\vliiinf{}{}{ \seqar A}{ \seqar C}

%%	$$

%

%%\[

%%	\vliiinf{R}{}{ !\Gamma , \Sigma' \seqar \Delta' , ? \Pi  }{ \{!\Gamma , \Sigma_i \seqar \Delta_i , ? \Pi \}_{i \in I} }

%%	\]

We also rely on the following result, which is also folklore but appeared before in \cite{Avron88}.

\begin{theorem}

	[Deduction, folklore]

	\label{thm:deduction}

	For any theory $\theory$ and closed formula $A $, $\mathcal T \cup\{A\}$ proves $B$ if and only if $\mathcal{T}$ proves $!A \limp B$.

\end{theorem}

%The occurrence of $!$ in the deduction theorem above is crucial; this restriction is one of the reasons it can be difficult to reason informally in theories over linear logic.

For example, we can work in the following quantifier-free system for the theory of equality:

\begin{proposition}

	[Equality rules]

	\eqref{eqn:equality-theory} is equivalent to the following system of rules,

	\[

	\vlinf{}{}{\seqar t = t}{}

	\qquad

	\vlinf{}{}{s = t \seqar t = s}{}

	\qquad 

	\vlinf{}{}{r = s, s= t \seqar r = t}{}

	\qquad 

	\vlinf{}{}{\vec s = \vec t \seqar f(\vec s) = f(\vec t)}{}

	\qquad

	\vlinf{}{}{\vec s = \vec t, P(\vec s) \seqar P(\vec t)}{}

	\]

	where $r,s,t $ range over terms.

\end{proposition}

%\subsection{Converting axioms to rules in $\MELLW$}

%

%\begin{proposition}

%	An axiom $\Ax$ of the form,

%	\[

%	A_1 \limp \vldots \limp A_m \limp !B_1 \limp \vldots \limp !B_n \limp C

%	\]

%	is equivalent (over propositional $\LL$) to the rule $\Rl$:

%	\[

%	\vliiinf{\Rl}{}{ !\Gamma , A_1 , \dots , A_m \seqar C , ? \Delta  }{ !\Gamma \seqar B_1 , ?\Delta }{\vldots }{ !\Gamma \seqar B_n , ?\Delta}

%	\]

%\end{proposition}

%\begin{proof}

%	Let us first assume $\Ax$ and derive $\Rl$. From the axiom and Currying, we have a proof of:

%	\begin{equation}\label{eqn:curried-axiom}

%	A_1 , \dots , A_m , !B_1 , \dots , !B_n \seqar C

%	\end{equation}

%	

%	This can simply be cut against each of the premisses of $\Rl$, applying appropriate contractions and necessitations, to derive it:

%	\[

%	\vlderivation{

%		\vliq{c}{}{!\Gamma , A_1 , \dots , A_m \seqar C , ?\Delta }{

%			\vliin{\cut}{}{!\Gamma, \dots , !\Gamma , A_1 , \dots , A_m \seqar C , ?\Delta, \dots , ?\Delta }{

%				\vlin{!}{}{!\Gamma \seqar !B_n, ?\Delta }{\vlhy{!\Gamma \seqar B_n , ?\Delta }}

%			}{

%			\vliin{\cut}{}{\qquad \qquad \qquad \qquad  \vlvdots \qquad \qquad \qquad \qquad }{

%				\vlin{!}{}{!\Gamma \seqar !B_1 , ?\Delta}{\vlhy{!\Gamma \seqar B_1, ?\Delta }}

%			}{\vlhy{ A_1 , \dots , A_m , !B_1 , \dots , !B_n \seqar C } }

%		}

%	}

%}

%\]

%

%Now let us prove $\Ax$ (again in the form of \eqref{eqn:curried-axiom}) by using $\Rl$ as follows:

%\[

%\vliiinf{\Rl}{}{ A_1 , \dots , A_m , !B_1 , \dots , !B_n \seqar C }{  \vlderivation{

%		\vlin{w}{}{ !B_1 , \dots , !B_n \seqar B_1 }{

%			\vlin{!}{}{!B_1 \seqar B_1 }{

%				\vlin{\id}{}{B_1 \seqar B_1 }{\vlhy{}}

%			}

%		}

%	}  }{\vldots}{

%	\vlderivation{

%		\vlin{w}{}{ !B_1 , \dots , !B_n \seqar B_n }{

%			\vlin{!}{}{!B_n \seqar B_n }{

%				\vlin{\id}{}{B_n \seqar B_n }{\vlhy{}}

%			}

%		}

%	}

%}

%\]

%\end{proof}

%

%

%\textbf{NB:} The proof does not strictly require side formulae $? \Delta$ on the right of the sequent arrow $\seqar$, it would work without them, e.g.\ for the intuitionistic case. In a one-sided setting there is no difference.

%

%

%

%\begin{corollary}

%	The induction axiom of $A^1_2$ is equivalent to the rule:

%	\[

%	\vliinf{}{(x \notin \FV(\Gamma, \Delta))}{ !\Gamma , !N(t), A(\epsilon) \seqar A(t) , ?\Delta }{ !\Gamma , !N(x), A(x) \seqar A(s_0 x ), ?\Delta }{ !\Gamma, !N(x),  A(x) \seqar A( s_1 x ) , ?\Delta}

%	\]

%\end{corollary}

%\begin{proof}

%	By proposition above, generalisation and Currying.

%\end{proof}

%

%\begin{proposition}

% The following induction rule is derivable from the one of the previous corollary:

%\[

%	\vliinf{}{(a, \vec{v}, \vec{x} \notin \FV(\Gamma, \Delta))}{ !\Gamma , !N(\vec{w}), N(\vec{y}), !N(t)  \seqar A(t,\vec{w},\vec{y}) , ?\Delta }{ !\Gamma ,  !N(\vec{v}), N(\vec{x}) \seqar A(\epsilon,\vec{v},\vec{x}), ?\Delta }{ !\Gamma ,  !N(\vec{v}), N(\vec{x}),    A(a,\vec{v},\vec{x}) \seqar  A(s_ia,\vec{v},\vec{x}) , ?\Delta}

%	\]

%where the second premise corresponds actually to two premises, one for $i=0$ and one for $i=1$.

%\end{proposition}

%\subsection{Prenexing}

%%In the presence of weakening we have a prenex normal form due to the following:

%%

%%\[

%%\vlderivation{

%%	\vlin{}{}{\exists x . A \lor B \seqar \exists x . (A(x) \lor B) }{

%%		

%%		}

%%	}

%%\]

%

%Cannot derive prenexing operations, e.g.\ a problem with $\exists x . A \lor B \seqar \exists x . (A(x) \lor B)$. Can safely add prenexing rules? Or not a problem due to Witness predicate?