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

\documentclass[a4paper,UKenglish]{lipics-v2016}

%This is a template for producing LIPIcs articles. 

%See lipics-manual.pdf for further information.

%for A4 paper format use option "a4paper", for US-letter use option "letterpaper"

%for british hyphenation rules use option "UKenglish", for american hyphenation rules use option "USenglish"

% for section-numbered lemmas etc., use "numberwithinsect"

\usepackage{microtype}%if unwanted, comment out or use option "draft"

%\graphicspath{{./graphics/}}%helpful if your graphic files are in another directory

\bibliographystyle{plainurl}% the recommended bibstyle

\usepackage[lutzsyntax]{virginialake}

\usepackage{amsmath}

\usepackage{amssymb}

\usepackage{amsthm}

\usepackage{times}

%\usepackage{sans}

\usepackage{cmll}

\usepackage{bm}

%\newtheorem{theorem}{Theorem}

%\newtheorem{maintheorem}[theorem]{Main Theorem}

%\newtheorem{observation}[theorem]{Observation}

%\newtheorem{corollary}[theorem]{Corollary}

%\newtheorem{lemma}[theorem]{Lemma}

\newtheorem{proposition}[theorem]{Proposition}

%\newtheorem{conjecture}[theorem]{Conjecture}

%

%\theoremstyle{definition}

%\newtheorem{definition}[theorem]{Definition}

%\newtheorem{example}[theorem]{Example}

%\newtheorem{notation}[theorem]{Notation}

%\newtheorem{convention}[theorem]{Convention}

%\newtheorem{remark}[theorem]{Remark}

%\newtheorem{discussion}[theorem]{Discussion}

\newcommand{\todo}[1]{{\color{red}{\textbf{Todo:} #1}}}

\newcommand{\anupam}[1]{{\color{orange}{\textbf{Anupam:} #1}}}

\newcommand{\patrick}[1]{{\color{blue}{\textbf{Patrick:} #1}}}

\newcommand{\defined}{:=}

\begin{document}

	\newcommand{\LL}{\it{LL}}

	\vllineartrue

	\newcommand{\FV}{\mathit{FV}}

	%terms

	\renewcommand{\succ}{s}

	\renewcommand{\epsilon}{\varepsilon}

	% linear connectives

	\newcommand{\limp}{\multimap}

	\renewcommand{\land}{\otimes}

	\newcommand{\laand}{\&}

	\newcommand{\laor}{\oplus}

	\renewcommand{\lor}{\vlpa}

	\renewcommand{\lnot}[1]{{#1^{\perp}}}

	\newcommand{\lnotnot}[1]{#1^{\perp \perp}}

	% classical connectives

	\newcommand{\cimp}{\supset}

	\newcommand{\cand}{\wedge}

	\newcommand{\cor}{\vee}

	\newcommand{\cnot}{\neg}

	\newcommand{\Ax}{\mathit{(Ax)}}

	\newcommand{\Rl}{\mathit{(Rl)}}

	\newcommand{\MELL}{\mathit{MELL}}

	\newcommand{\MEAL}{\mathit{MELLW}}

	\newcommand{\MELLW}{\mathit{MELL(W)}}

	\newcommand{\Aonetwo}{\mathcal{A}^1_2}

	\newcommand{\logic}{\mathit{L}_{\mathcal A} }

	% predicates

	\newcommand{\nat}{N}

	\newcommand{\Nat}{\mathbb{N}}

	%axioms

	\newcommand{\wk}{\mathit{wk}}

	\newcommand{\impl}{\cimp\text{-}\mathit{l}}

	\newcommand{\impcomm}{\mathit{com}}

	\newcommand{\conint}{\cand\text{-}\mathit{i}}

	\newcommand{\conel}{\cand\text{-}\mathit{e}}

	\newcommand{\negclass}{\cnot}

	%rules

	\renewcommand{\mp}{\mathit{mp}}

	\newcommand{\gen}{\mathit{gen}}

	\newcommand{\inst}{\mathit{ins}}

	\newcommand{\id}{\it{id}}

	\newcommand{\cut}{\it{cut}}

	\newcommand{\multicut}{\it{mcut}}

	\newcommand{\indr}{\mathit{IND}}

	\newcommand{\nec}{\mathit{nec}}

	\newcommand{\tax}{\mathit{T}}

	\newcommand{\four}{\mathit{4}}

	\newcommand{\kax}{\mathit{K}}

	\newcommand{\cntr}{\mathit{cntr}}

	\newcommand{\lefrul}[1]{#1\text{-}\mathit{l}}

	\newcommand{\rigrul}[1]{#1\text{-}\mathit{r}}

	%consequence relations

	\newcommand{\admits}{\vDash}

	\newcommand{\seqar}{\vdash}

	\newcommand{\proves}{\vdash_e}

	%induction

	\newcommand{\ind}{\mathit{IND}}

	\newcommand{\pind}{\mathit{PIND}}

	\newcommand{\cax}[2]{#1\text{-}#2}

% Author macros::begin %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Free-cut elimination in linear logic: an application to implicit complexity}

%\titlerunning{A Sample LIPIcs Article} %optional, in case that the title is too long; the running title should fit into the top page column

%% Please provide for each author the \author and \affil macro, even when authors have the same affiliation, i.e. for each author there needs to be the  \author and \affil macros

\author[1]{Patrick Baillot}

\author[2]{Anupam Das}

\affil[1]{Dummy University Computing Laboratory, Address/City, Country\\

  \texttt{open@dummyuniversity.org}}

\affil[2]{Department of Informatics, Dummy College, Address/City, Country\\

  \texttt{access@dummycollege.org}}

\authorrunning{J.\,Q. Open and J.\,R. Access} %mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et. al.'

\Copyright{John Q. Open and Joan R. Access}%mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/

\subjclass{Dummy classification -- please refer to \url{http://www.acm.org/about/class/ccs98-html}}% mandatory: Please choose ACM 1998 classifications from http://www.acm.org/about/class/ccs98-html . E.g., cite as "F.1.1 Models of Computation". 

\keywords{Dummy keyword -- please provide 1--5 keywords}% mandatory: Please provide 1-5 keywords

% Author macros::end %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\EventEditors{John Q. Open and Joan R. Acces}

\EventNoEds{2}

\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}

\EventShortTitle{CVIT 2016}

\EventAcronym{CVIT}

\EventYear{2016}

\EventDate{December 24--27, 2016}

\EventLocation{Little Whinging, United Kingdom}

\EventLogo{}

\SeriesVolume{42}

\ArticleNo{23}

% Editor-only macros::end %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\maketitle

\begin{abstract}

We prove a general form of free-cut elimination for first-order theories in linear logic. We consider a version of Peano Arithmetic in linear logic and prove a witnessing theorem via the Buss and Mints \emph{witness function method}, characterising polytime as the provably total functions.

 \end{abstract}

\section{Introduction}

\todo{words or integers?}

\section{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 Sequents: $\Gamma, \Delta, \Sigma, \Pi$.

\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.}

\begin{definition}\label{def:LLsequentcalculus}

[Sequent calculus for linear logic]

We define the following calculus in De Morgan normal form:

\[

\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}

&

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

&

\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) }

\end{array}

\end{array}

\]

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

\end{definition}

  We will consider extensions of linear logic with a \textit{theory}  $\mathcal T$ consisting in a finite set of additional axioms and rules, depicted as:

 \[

 \begin{array}{cc}

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

\end{array}

\]

 where in rule (R), $I$ is a finite set (indicating the number of premises) and we assume the following condition:

  \textit{for any $i\in I$, formulas in $\Sigma_i, \Delta_i$ do not share any free variable with   $\Gamma, \Pi$.} 

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

  A proof in this 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 $\tau$ are called \textit{non-logical}.

  As usual rules come with a notion of \textit{active 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).

  While in usual logical systems such as linear logic cut rules can be eliminated, this is in general not the case anymore when one considers extension with a theory $\tau$. For this reason we need now to define the kind of cuts that  will remain in proofs after reduction.

  \begin{definition}\label{def:anchoredcut}

  An instance of cut rule in a  $\mathcal T$-proof is an \textit{anchored cut} if  its cut-formulas $A$ in the two premises are both principal for their rule, and at least one of these rules is non-logical.

  \end{definition}

  So for instance a cut on an (active) formula $A \lor B$ between a rule $\rigrul{\lor}$ and a rule (R) (where  $A \lor B$ occurs in $\Sigma'$) is anchored, while a cut between 

  a rule $\rigrul{\lor}$ and a rule $\lefrul{\lor}$ is not.

   Now we can state the main result of this section:

   \begin{theorem}

    GIven a theory  $\mathcal T$, any  $\mathcal T$-proof $\pi$ can be transformed into a $\mathcal T$-proof $\pi'$ with same conclusion sequent and in which all cuts are anchored.

   \end{theorem}

\subsection{Deduction theorem}

[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} }

%	\]

\begin{theorem}

	[Deduction]

	If $\mathcal T , A \proves B$ then $\mathcal{T} \proves !A \limp B$.

\end{theorem}

\todo{need that $A$ above is closed! Check for rules to axioms.}

\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 , A(\epsilon) \seqar A(t) , ?\Delta }{ !\Gamma , A(x) \seqar A(s_0 x ), ?\Delta }{ !\Gamma, A(x) \seqar A( s_1 x ) , ?\Delta}

	\]

\end{corollary}

\begin{proof}

	By proposition above, generalisation and Currying.

\end{proof}

\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?

\section{Free-cut elimination in linear logic}

\todo{patrick}

\anupam{Possibly need to include the cases for affine logic too, e.g.\ if weakening is native, since it does not play nice as an axiom.}

\todo{include some bounds on free-cut elimination? Look at paper "Corrected upper bounds for free-cut elimination" by Beckmann and Buss for comparison.}

\section{Some variants of arithmetic in linear logic}

For pretty much all variants discussed we will actually work in the \emph{affine} variant of linear logic, which validates weakening: $(A \land B )\limp A$. There are many reasons for this; essentially it has not much effect on complexity while also creating a more robust proof theory. For example it induces the following equivalence:

\[

!(A\land B) \equiv (!A \land !B)

\]

(The right-left direction is already valid in usual linear logic, but the left-right direction requires weakening).

We define a variant of arithmetic inspired by Bellantoni and Hofmann's $A^1_2$. We describe later some connections to bounded arithmetic.

\subsection{Based on Bellantoni-Hoffmann, Leivant, etc.}

\newcommand{\natcntr}{\nat\mathit{cntr}}

\newcommand{\geneps}{\nat_{\epsilon}}

\newcommand{\genzer}{\nat_{0}}

\newcommand{\genone}{\nat_{1}}

\newcommand{\sepeps}{\epsilon}

\newcommand{\sepzer}{\succ_{0}}

\newcommand{\sepone}{\succ_{1}}

\newcommand{\inj}{\mathit{inj}}

\newcommand{\surj}{\mathit{surj}}

\begin{definition}

[Arithmetic]

We have the following axioms:

\[

\begin{array}{rl}

\wk & (A \land B )\limp A \\

\natcntr & \forall x^N . (N(x) \land N(x)) \\

\geneps & \nat(\epsilon) \\

\genzer & \forall x^N . N(\succ_0 x) \\

\genone & \forall x^N . N(\succ_1 x) \\

\sepeps & \forall x^N . (\epsilon \neq \succ_0 x \land \epsilon \neq \succ_1 x) \\

\sepzer & \forall x^N , y^N. ( \succ_0 x = \succ_0 y \limp x=y ) \\

\sepone & \forall x^N , y^N. ( \succ_1 x = \succ_1 y \limp x=y ) \\

\inj & \forall x^N . \succ_0 x \neq \succ_1 x \\

\surj & \forall x^N . (x = \epsilon \lor \exists y^N . x = \succ_0 y \lor \exists y^N . x = \succ_1 y ) \\

\noalign{\bigskip}

\ind & A(\epsilon) \limp !( \forall x^{!\nat} . ( A(x) \limp A(\succ_0 x) ) ) \limp !( \forall x^{!\nat} . ( A(x) \limp A(\succ_1 x) ) ) \limp \forall x^{!\nat} . A(x)

\end{array}

\]

Induction rule should be the following, to take account of relativised quantifiers?

\[

\vliinf{\ind}{}{ !N(t) , !\Gamma , A(\epsilon) \seqar A(t), ?\Delta }{ !N(a) , !\Gamma, A(a) \seqar A(\succ_0 a) , ?\Delta }{ !N(a) , !\Gamma, A(a) \seqar A(\succ_0 a) , ?\Delta  }

\]

\todo{in existential above, is there a prenexing problem?}

\todo{what about $\leq$? Introducing this could solve prenexing problem, e.g.\ by induction?}

\end{definition}

\subsection{$\nat$-hierarchy}

\begin{definition}

\todo{replace N with nat.}

	Let us define the quantifiers $\exists x^N . A$ and $\forall x^N . A$ as $\exists x . (N(x) \land A)$ and $\forall x . (N(x) \limp A) $ respectively.

	We define $\Sigma^N_0 = \Pi^N_0 $ as the class of formulae that are free of quantifiers. For $i\geq 0$ we define:

	\begin{itemize}

		\item $\Sigma^N_{i+1}$ is the class of formulae $\exists x^N . A$ where $A \in \Pi^N_i$.

		\item $\Pi^N_{i+1}$ is the class of formulae $\forall x^N . A$ where $A \in \Sigma^N_i$.

		\item ($\Delta^N_i$ is the class $\Sigma^N_i \cap \Pi^N_i$.)

	\end{itemize}

\end{definition}

\todo{allow closure under positive Boolean operations?}

\todo{What about prenexing rules? Should not change provably total functions!}

\subsection{Equivalent rule systems}

For the quantifiers $\exists x^N $ and $\forall x^N$ we introduce the following rules, which are compatible with free-cut elimination:

\[

\begin{array}{cc}

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

\quad & \quad

\vlinf{}{}{\Gamma, N(t),\forall x^N A(x) \seqar \Delta}{\Gamma,  A(t) \seqar \Delta}

\\

\noalign{\bigskip}

\vlinf{}{}{\Gamma , \exists x^N A(x) \seqar \Delta}{\Gamma, N(a), A(a) \seqar \Delta}

\quad &\quad 

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

\end{array}

\]

CHECK THESE!

\todo{Also include rules for contraction and weakening.}

\section{Convergence of Bellantoni-Cook programs}

\subsection{Bellantoni-Cook programs}

We first recall the notion of safe recursion on notation from BC. TODO

\subsection{Convergence in arithmetic}

\begin{theorem}

	[Convergence]

	If $\Phi(f)$ is an equational specification corresponding to a BC-program defining $f()$, then $\cax{\Sigma^N_1}{\pind} \proves  \ !\Phi(f) \limp \forall \vec{x}^{!N} . N(f(\vec x))$.

\end{theorem}

\begin{proof}

	We show by induction on the structure of a BC-program for $f(\vec x ; \vec y)$ that:

	\begin{equation}

	\Phi(f) , \cax{\Sigma^N_1}{\pind} \proves \ \forall \vec{x}^{!N} . \forall \vec{y}^N . N(f(\vec x ; \vec y))

	\end{equation}

	We give some key cases in what follows.

	Suppose $f$ is defined by PRN by:

	\[

	\begin{array}{rcl}

	f(0,\vec x ; \vec y) & = & g(\vec x ; \vec y) \\

	f(\succ_i x , \vec x ; \vec y) & = & h_i (x, \vec x ; \vec y , f(x , \vec x ; \vec y))

	\end{array}

	\]

	By the inductive hypothesis we already have that $g, h_0, h_1$ are provably convergent, so let us suppose that $N(\vec x)$ and prove,

	\begin{equation}

	\forall x^{!N} . ( N(\vec y) \limp N(f(x , \vec x ; \vec y)  )

	\end{equation}

	by $\cax{\Sigma^N_1}{\pind}$ on $x$.

	In the base case we have the following proof:

	\[

	\vlderivation{

		\vliin{}{}{N(\vec y) \limp N(f(0, \vec x ; \vec y))}{

			\vltr{IH}{N(\vec y) \limp N(g(\vec x ; \vec y))}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

		}{

		\vlin{}{}{N(g (\vec x ; \vec y) ) \limp N(f(0, \vec x ; \vec y)) }{

			\vlin{}{}{g(\vec x ; \vec y) = f(0 , \vec x ; \vec y)}{\vlhy{}}

		}

	}

}

\]

For the inductive step, we need to show that,

\[

\forall x^{!N} . (( N(\vec y) \limp N( f(x, \vec x ; \vec y) ) ) \limp N(\vec y) \limp N(f(\succ_i x , \vec x ; \vec y) )   )

\]

so let us suppose that $N(x)$ and we give the following proof:

\[

\vlderivation{

	\vlin{N\cntr}{}{N(y) \limp ( N(y ) \limp N(f( x , \vec x ; \vec y ) ) ) \limp N(f (\succ_i x , \vec x ; \vec y)  ) }{

		\vliin{}{}{N(y) \limp N(y) \limp ( N(y ) \limp N(f( x , \vec x ; \vec y ) ) ) \limp N(f (\succ_i x , \vec x ; \vec y)  ) }{

			\vliin{}{}{ N(y) \limp N(y) \limp ( N(y) \limp N( f(x, \vec x ; \vec y) ) ) \limp N( h_i (x , \vec x ; \vec y , f(x , \vec x ; \vec y) ) ) }{

				\vltr{MLL}{( N(\vec y) \limp (N (\vec y) \limp N(f(x, \vec x ; \vec y) )) \limp N(f(x, \vec x ; \vec y)) }{\vlhy{\quad }}{\vlhy{\ }}{\vlhy{\quad }}

			}{

			\vlhy{2}

		}

	}{

	\vlhy{3}

}

}

}

\]

TOFINISH

\end{proof}

\section{Witness function method}

Key features/differences from realisability:

\begin{itemize}

\item De Morgan normal form: reduces type level to $0$, complementary to double-negation translation that \emph{increases} type level.

\item Free-cut elimination: allows us to handles formulae of fixed logical complexity throughout the proof. 

\item Respects logical properties of formulae, e.g.\ quantifier complexity, exponential complexity.

\end{itemize}

\todo{say some more here}

\newcommand{\type}{\mathtt{t}}

\newcommand{\norm}{\nu}

\newcommand{\safe}{\sigma}

\subsection{Typing}

\begin{definition}

	[Types]

	To each formula we associate a tuple type as follows:

	\[

	\begin{array}{rcll}

	\type (\nat (t)) & := & \Nat & \\

	\type(s = t) & := & \Nat & \\

	\type (A \star B)  & : = & \type (A) \times \type (B) & \text{for $\star \in \{ \lor, \land, \laor, \laand \} $.} \\

	\type (! A) & : = & \type_\norm (A) & \\

	\type (\exists x^N . A) & := & \Nat \times \type (A) & \\

%	\type (\forall x^N . A) & := & \Nat \to \type(A)

	\end{array}

	\]

	where $\nu$ designates that the inputs are normal.

	\end{definition}

	\todo{compatibility with safety. To consider.}

	\newcommand{\witness}[2]{\mathit{Witness}^{#1}_{#2}}

	\begin{definition}

		[Witness predicate]

		We define the following formula:

		\[

		\begin{array}{rcll}

		\witness{\vec a}{A} (w, \vec a) & := & A(\vec a) & \text{for $A$ quantifier-free.} \\

		\witness{\vec a}{\exists x . A} (w, \vec w , \vec a) & := & \witness{\vec{a}, a}{A(a)}(\vec w , \vec a, w ) & \\

		\witness{\vec a}{A \star B} ( \vec w^1 , \vec w^2 ) & := &  \witness{\vec a}{A} (\vec w^1) \star \witness{\vec a}{B} (\vec w^2) & \text{for $\star \in \{ \land, \lor, \laand , \laor\}$.} \\

		\end{array}

		\]

	\end{definition}

	\todo{problem: what about complexity of checking equality? }

	\todo{What about $\nat (t)$? What does it mean? Replace with true?}

	\todo{either use the witness predicate above, or use realizability predicate at meta-level and a model theory, like BH.}

	\anupam{Need to check above properly. $N(t)$ should be witnessed by the value of $t $ in the model. For equality of terms the witness should not do anything.}

	\subsection{The translation}

	Need witness predicate so that we know what is being preserved.

\begin{definition}

	[Translation]

	We give a translation of proofs $\pi$ of sequents $\Gamma(\vec a) \seqar \Delta(\vec a)$ to BC-programs for a vector of functions $\vec f^\pi : \type(\bigotimes\Gamma) \times \Nat^{|\vec a|} \to \type(\bigparr\Delta)$ such that:

	\[

	\witness{\vec a}{\bigotimes \Gamma} (\vec w , \vec a) \implies \witness{\vec a}{\bigparr \Delta } (\vec f(\vec w , \vec a), \vec a)

	\]

	We will be explicit about normal and safe inputs when necessary, for the most part we will simply rearrange inputs into lists $(\vec x; \vec a)$ as in BC framework.

	We often suppress the parameters $\vec a$ when it is not important.	

	\anupam{Is this implication provable in Bellantoni's version of PV based on BC?}

	\anupam{for moment try ignore decoration on right? what about negation?}

	\[

	\vlderivation{

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

			\vltr{\pi_1}{ \Gamma \seqar \Delta, A }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

			}{

			\vltr{\pi_2}{ \Sigma \seqar \Pi, B }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

			}

		}

	\]

	So we have $\vec f^{1} (\vec x ; \vec a)$ and $\vec f^2 (\vec y ; \vec b)$ for $\pi_1 $ and $\pi_2$ respectively, by the inductive hypothesis. We simply construct $\vec f^\pi$ by rearranging these functions:

	\[

	\vec f^\pi (\vec x , \vec y ; \vec a , \vec b) \quad := \quad ( f^1_1 (\vec x ; \vec a) , \dots , f^1_{|\Delta|} (\vec x ; \vec a) , f^2_1 (\vec y; \vec b) , \dots , f^2_{|\Pi|} (\vec y ; \vec b) , f^1_{|\Delta|+1} (\vec x ; \vec a ) , f^2_{|\Pi|+1} (\vec y ; \vec b)

	\] 

	\anupam{bad notation since need to include free variables of sequent too. (also of theory.) Reconsider.}

	\[

	\vlderivation{

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

			\vltr{\pi'}{  !A, !A , \Gamma \seqar \Delta}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

			}

		}

	\]

	Have $\vec f' (x_1 , x_2 , \vec y ; \vec a)$ for $\pi'$. Define

	\[

	\vec f (x_1 , \vec y ; \vec a) \quad := \quad \vec f'(x_1 , x_1 , \vec y ; \vec a)

	\]

	\[

	\vlderivation{

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

	\vltr{\pi'}{  \Gamma \seqar \Delta, ?A, ?A}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

	}

	}

	\]

	(need test function against witness predicate?)

	\anupam{problem: how to test even equality of two terms? Maybe treat $?$ as $!$ on left?}

	\anupam{Not a problem by free-cut elimination! Can assume there are no $?$ in the proof! Is this equivalent to treaing $?$ as $!$ on left?}

	\anupam{Yes I think so. We can work in a left-sided calculus. only problem is for induction. But this can never be a problem for modalities since induction formulae are modality-free.}

	\anupam{this is actually the main point.}

	\[

	\vlderivation{

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

	\vltr{\pi_1}{  \Gamma \seqar \Delta, A}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

	}{

	\vltr{\pi_2}{  \Gamma \seqar \Delta, B}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

	}

	}

	\]

	Suppose we have $\vec f^i (\vec x , \vec a ; \vec y , \vec b)$ from $\pi_i$.

	\anupam{problem: does this require many tests, just like for contraction? Can we isolate a different complexity class? e.g.\ PH or Grzegorzyck?}

	\anupam{skip this case and consider later.}

\[

\vlderivation{

\vliin{\cut}{}{\Gamma , \Sigma \seqar \Delta , \Pi}{

\vltr{\pi_1}{ \Gamma \seqar \Delta, A }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}{

\vltr{\pi_2}{\Sigma , A \seqar \Pi}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}

}

	\]

We can assume that $A$ in the conclusion of $\pi_2$ is free of modalities, since one of the $A$s must be directly descended from an induction formula, and so consists of only safe inputs. Therefore we have functions $\vec f^1 (\vec w; \vec x)$ and $\vec f^2 (\vec y ; \vec z , \vec u)$ for $\pi_1$ and $\pi_2 $ respectively (free variable parameters are suppressed), with $\vec u$ corresponding to the (safe) inputs for $A$. 

Let us write:

\[

\begin{array}{rcl}

\vec f^1 & = & ( \vec f^1_i )^{|\Delta|+1}_{i=1} \\

\vec f^2 & = & ( \vec f^2_i )^{|\Pi|}_{i=1}

\end{array}

\]

to denote the parts of $\vec f^i$ corresponding to formulae in their sequents.

We define:

\[

\vec f (\vec w , \vec y ; \vec x , \vec z)

\quad := \quad

(

( \vec f^1_i (\vec w ; \vec x) )_{i \leq |\Delta|}

,

\vec f^2 ( \vec y ; \vec z , \vec f^1_{|\Delta| +1 } (\vec w ; \vec x) )

)

\]

Notice that all safe inputs are hereditarily right of a $;$, and so these terms are definable by safe composition and projection.

\todo{another case for $!\nat(x)$ cut formula.}

\anupam{should work for arbitrary $!$-cuts due to principal case for $!$}

Right existential:

\[

\vlderivation{

\vlin{\rigrul{\exists}}{}{ \Gamma, \nat(t) \seqar \Delta , \exists x^\nat . A(x) }{

\vltr{\pi'}{ \Gamma \seqar \Delta , A(t) }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}

}

\]

Suppose we have functions $\vec f^X (\vec x ; \vec y)$ from $\pi'$ for $X = \Delta$ or $ X=A$. 

\[

\vec f(\vec x ; \vec y , z) \quad := \quad ( \vec f^\Delta (\vec x ; \vec y)   ,  z , \vec f^A ( \vec x ; \vec y ) )

\]

Left existential:

\[

\vlderivation{

\vlin{\lefrul{\exists}}{}{ \Gamma, \exists x^N . A(x) \seqar \Delta }{

\vltr{\pi'(a)}{ \Gamma,  N(a) , A(a) \seqar \Delta  }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}

}

\]

Suppose we have functions $\vec f' (\vec u , \vec v ; x , \vec y , \vec z)$ from $\pi'$ with $(\vec u ; \vec x )$ corresponding to $\Gamma$, $(;x)$ corresponding to $N(a)$ and $(\vec v ; \vec z)$ corresponding to $A(a)$. We define:

\[

\vec f ( \vec u , \vec v ;  )

\]

\anupam{should just be same, no? To consider.}

%Suppose we have functions $\vec g (\vec v  , \vec w ; \vec x , y , \vec z)$ where $(\vec v ; \vec x) $ corresponds to $\Gamma$, $y$ corresponds to $\nat(a)$ and $(\vec w ; \vec z) $ corresponds to $A(a)$. Then we define:

%\[

%\vec f ( \vec v , \vec w ; \vec x , y , \vec z )

%\]

\todo{finish}

!:

\[

\vlderivation{

\vlin{!}{}{\Gamma, !A \seqar \Delta}{

\vltr{\pi'}{ \Gamma , A \seqar \Delta  }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}

}

\]

\anupam{Again, use free-cut elimination to get rid of this case. We know $!$-ed formulae in advance, so just fix those as normal inputs in advance.}

Induction: (can assume no side-formulae on right for same reason as no contraction.)

\[

\vlderivation{

\vliin{\ind}{}{ !\Gamma , !\nat (t) ,  A(\epsilon) \seqar A(t) }{

\vltr{\pi_0}{ !\Gamma , !\nat(a) , A(a) \seqar A(\succ_0 a)}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}{

\vltr{\pi_1}{ !\Gamma , !\nat(a), A(a)\seqar A(\succ_1 a) }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}

}

\]

Suppose we have functions $\vec f^i (\vec x , y ; \vec u)$ from proofs $\pi_i$ where $\vec x $ corresponds to $!\Gamma$, $y$ corresponds to $!N(a)$ and $\vec u$ corresponds to $A(a)$.

\anupam{role of $!N(a)$ versus having $a$ as a parameter to function. To consider!}

Define the function $f_k$ (for $k = 1 , \dots , |\vec u|$) by PRN:

\[

\begin{array}{rcl}

f_k(\epsilon, \vec x , y ; \vec u) & := & u_k \\

f_k (\succ_i w , \vec x , y ; \vec u) & : = & f^i_k ( \vec x ,  y ; \vec f ( w, \vec x , y ; \vec u ) )

\end{array}

\]

\anupam{check this, esp use of parameters, cf.\ above.}

\anupam{Is this not using a simultaneous version of PRN? Might need concatenation of words/basic coding to deal with this.}

\end{definition}

\newcommand{\concat}{\mathit{concat}}

\paragraph{Some points on concatenation \anupam{if necessary}}

We can define the concatenation operation by PRN:

\[

\begin{array}{rcl}

\concat (\epsilon ; y) & : = & x \\

\concat (\succ_i x ; y) & := & \succ_i \concat (x ; y)

\end{array}

\]

From here we can define iterated concatenation:

\[

\concat (x_1 , \dots x_n ; y) \quad := \quad \concat (x_n ; \concat (x_{n-1} ; \vldots \concat (x_1 ; y) \vldots ) )

\]

(notice all safe inputs are hereditarily to the right of $;$ so this is definable by safe composition and projection.)

\section{Further work}

Say something about minimisation and the polynomial hierarchy. Could be achieved by controlling contraction/additives, since this requires a notion of tests.

\section{Conclusions}

\appendix

\section{Some cut-elimination cases}

We work in a one-sided calculus for full linear logic. When working in the affine setting we simply drop the condition that weakened formulae are $?$-ed.

As well as all usual rules, we have the induction rule:

\[

\vlinf{\indr}{(x \notin FV (\Gamma) )}{? \Gamma, A^\perp (0) , A(t)}{? \Gamma , A^\perp (x) , A(s x) }

\]

We give all the various cut-reduction cases in the following section but first we give a simple cut-elimination argument.

\subsection{A basic (free-)cut elimination argument}

We give an argument that easily scales to free-cut elimination, i.e.\ in the presence of non-logical rules.

\newcommand{\anarrow}[2]{\overset{#1}{\underset{#2}{\longrightarrow}}}

\newcommand{\cutredlin}{\mathit{ma}}

\newcommand{\cutredexp}{exp}

\begin{definition}

	Let $\anarrow{}{\cutredexp}$ denote the reduction steps concerning exponential cuts, and $\anarrow{}{\cutredlin}$ be the set of cut-reduction steps concerning multiplicative and additive cuts.

\end{definition}

\newcommand{\rk}{\mathsf{rk}}

	\renewcommand{\deg}{\mathsf{deg}}

\begin{definition}

	[Measures]

	For a $\anarrow{}{\cutredlin}$-redex $r$, let its \emph{degree} $\deg( r)$ be the number of logical connectives or quantifiers in its cut-formula. For a proof $\pi$, its \emph{degree} $\deg( \pi)$ is the multiset of the degree of its redexes.

\end{definition}

\begin{proposition}

If $\pi$ is not $\anarrow{}{\cutredlin}$-normal then there is a derivation $L:\pi \anarrow{*}{\cutredlin} \pi'$ such that $\deg(\pi')< \deg(\pi)$.

\end{proposition}

\begin{proof}

	First let us show the statement in the special case that $\pi$ contains precisely one $\cut$-inference as its final step, by induction on $|\pi|$. Each commutative $\anarrow{}{\cutredlin}$-step results in us being able to apply the inductive hypothesis to smaller proofs,- in the case of $\vlan $ two smaller proofs. Each key $\anarrow{}{\cutredlin}$-case strictly reduces the degree of the proof. Consequently we can eventually transform $\pi$ to a proof $\pi'$ which has possibly several cuts of smaller degree, as required.

	Now to the general case, we simply apply the above procedure to the subproof above a topmost cut in $\pi$.

\end{proof}

\begin{corollary}

	$\anarrow{}{\cutredlin}$ is weakly normalising.

\end{corollary}

\newcommand{\cntdown}{\mathit{cn}}

\begin{definition}

	[Lazy contraction]

	Let $\anarrow{}{\cntdown}$ comprise of the following reduction steps:

	\begin{enumerate}

		\item The commuting steps,

			\[

			\vlderivation{

				\vlin{\rho}{}{\Gamma', ?A, }{

					\vlin{\cntr}{}{\Gamma, ?A}{\vlhy{\Gamma, ? A, ? A}}

				}

			}

			\quad\to \quad

			\vlderivation{

				\vlin{\cntr}{}{\Gamma', ?A}{

					\vlin{\rho}{}{\Gamma', ?A, ?A}{\vlhy{\Gamma, ? A, ? A}}

				}

			}	

			\]

			for each unary rule $\rho$.

			\item 

			The key steps:

			\[ 	

			\begin{array}{rcl}

			\vlderivation{

				\vlin{\cntr}{}{\Gamma, ?A}{

					\vlin{\wk}{}{\Gamma, ?A, ?A}{\vlhy{\Gamma, ?A}}

				}

			}

			\quad &\to & \quad

			\Gamma, ?A 

%			\]

%			and

%			\[

\\

\noalign{\smallskip}

				\vlderivation{

					\vlin{\wk}{}{\Gamma, ?A, ?A}{

						\vlin{\cntr}{}{\Gamma, ?A}{\vlhy{\Gamma, ?A, ?A}}

					}

				}

				\quad &\to& \quad

				\Gamma, ?A, ?A

							\end{array}

			\].

\item The commuting steps,

\[

	\vlderivation{

		\vliin{\rho}{}{\Gamma ,?A}{

			\vlin{\cntr}{}{\Gamma_1, ?A}{\vlhy{\Gamma_1, ?A, ?A}}

		}{\vlhy{\Gamma_2}}

	}

	\quad \to \quad

	\vlderivation{

		\vlin{\cntr}{}{\Gamma, ?A}{

			\vliin{\rho}{}{\Gamma,?A, ?A}{\vlhy{\Gamma_1, ?A, ?A}}{ \vlhy{\Gamma_2} }

		}

	}

\]

%\[

%\begin{array}{rcl}

%	\vlderivation{

%		\vliin{\land}{}{\Gamma, \Delta, ?A, B\land C}{

%			\vlin{\cntr}{}{\Gamma, ?A, B}{\vlhy{\Gamma, ?A, ?A, B}}

%		}{\vlhy{\Delta, C}}

%	}

%	\quad &\to &\quad

%	\vlderivation{

%		\vlin{\cntr}{}{\Gamma, \Delta, ?A, B\land C}{

%			\vliin{\land}{}{\Gamma, \Delta, ?A, ?A, B\land C}{\vlhy{\Gamma, ?A, ?A, B}}{ \vlhy{\Delta, C} }

%		}

%	}

%%	\]

%%	

%%	\[

%\\

%\noalign{\smallskip}

%	\vlderivation{

%		\vliin{\cut}{}{\Gamma, \Delta, ?A}{

%			\vlin{\cntr}{}{\Gamma, ?A, B}{\vlhy{\Gamma, ?A, ?A, B}}

%		}{\vlhy{\Delta, \lnot{B}}}

%	}

%	\quad &\to& \quad

%	\vlderivation{

%		\vlin{\cntr}{}{\Gamma, \Delta, ?A}{

%			\vliin{\cut}{}{\Gamma, \Delta, ?A, ?A}{\vlhy{\Gamma, ?A, ?A, B}}{ \vlhy{\Delta, \lnot{B}} }

%		}

%	}

%\end{array}

%\]

for each binary rule $\rho \in \{ \land, \cut \}$.

\item The commuting step:

	\[

	\vlderivation{

		\vliin{\vlan}{}{\Gamma, ?A, B\vlan C}{

			\vlin{\cntr}{}{\Gamma, ?A, B}{\vlhy{\Gamma, ?A, ?A, B}}

		}{\vlhy{\Gamma, ?A, B}}

	}

	\quad \to \quad

	\vlderivation{

		\vlin{\cntr}{}{\Gamma, ?A, B\vlan C}{

			\vliin{\vlan}{}{\Gamma, ?A, ?A, B\vlan C}{\vlhy{\Gamma, ?A, ?A, B}}{

				\vlin{\wk}{}{\Gamma, ?A, ?A, C}{\vlhy{\Gamma, ?A, C}}

			}

		}

	}

	\]

	\end{enumerate}

	For binary rules:

\end{definition}

\begin{proposition}

	$\anarrow{}{\cntdown}$ is weakly normalising

	, modulo $\cntr$-$\cntr$ redexes,

	and degree-preserving. 

	If $\pi$ is $\anarrow{}{\cutredlin}$-normal and $\pi \downarrow_\cntdown \pi'$, then so is $\pi'$.

\end{proposition}

\begin{proof}

	By induction on the number of redexes in a proof. Start with bottommost redex, by induction on number of inference steps beneath it.

\end{proof}

\begin{remark}

	Only weakly normalising since $\cntr$ can commute with $\cntr$, allowing cycles.

\end{remark}

\begin{proposition}

	If $\pi$ is $\anarrow{}{\cutredexp}$-reducible but $\anarrow{}{\cutredlin}$- and $\anarrow{}{\cntdown}$-normal then there is a derivation $H:\pi \anarrow{*}{\cutredexp} \pi'$ such that $\deg (\pi')<\deg(\pi)$.

\end{proposition}

\subsection{Base cases}

\[

\vlderivation{

\vliin{\cut}{}{ \Gamma,a }{ \vlhy{\Gamma,a} }{ \vlin{\id}{}{a,a^\bot}{ \vlhy{} } }

}

\quad\to\quad

\vlderivation{

\Gamma,a

}

\]

\[

\vlderivation{

\vliin{\cut}{}{\Gamma}{ \vlin{\bot}{}{ \Gamma,\bot }{ \vlhy{\Gamma} } }{ \vlin{1}{}{1}{ \vlhy{} } }

}

\quad\to\quad

\vlderivation{

\Gamma

}

\]

\[

\vlderivation{

\vliin{\cut}{}{ \Gamma,\Delta,\top }{ \vlin{\top}{}{ \Gamma,\top,0 }{ \vlhy{} } }{ \vlhy{\Delta , \top } }

}

\quad\to\quad

\vlinf{\top}{}{ \Gamma,\Delta,\top }{}

\]

\subsection{Commutative cases}

These are the cases when the principal formula of a step is not active for the cut-step below.

\begin{enumerate}

\item The cut-step is immediately preceded by an initial step. Note that only the case for $\top$ applies:

\[

\vlderivation{

\vliin{\cut}{}{\Gamma,\Delta,\top}{ 

\vlin{\top}{  }{ \Gamma,\top,A }{ \vlhy{} }

 }{ \vlhy{\Delta,A^\bot } }

}

\quad\to\quad

\vlinf{\top}{}{ \Gamma,\Delta,\top }{}

\]

%Notice that this commutation eliminates the cut entirely and preserves the height of all cuts below.

\item\label{CaseCommOneStep} A cut-step is immediately preceded by a step $\rho$ with exactly one premiss:

\[

\vlderivation{

\vliin{\cut}{}{\Gamma',\Delta}{\vlin{\rho}{}{\Gamma',A}{\vlhy{\Gamma,A}}}{\vlhy{A^\bot , \Delta}}

}

\]

We have three subcases:

\begin{enumerate}

\item\label{subcase:unary-commutation-vanilla} 

%$\Delta$ consists of only $?$-ed formulae or 

If $\rho \notin \{! , \indr \}$ then we can simply permute as follows:

\begin{equation}

\label{eqn:com-case-unary-simple}

\vlderivation{

\vliin{\cut}{}{\Gamma',\Delta}{\vlin{\rho}{}{\Gamma',A}{\vlhy{\Gamma,A}}}{\vlhy{A^\bot , \Delta}}

}

\quad \to \quad

\vlderivation{

\vlin{\rho}{}{\Gamma',\Delta}{

\vliin{\cut}{}{\Gamma,\Delta}{\vlhy{\Gamma,A}}{\vlhy{A^\bot , \Delta}}

}

}

\end{equation}

(If $\rho$ was $\forall$ then we might need to rename some free variables in $\Delta$.)

\item $\rho $ is a $!$-step. Therefore $\Gamma$ has the form $? \Sigma , B$ and $A$ has the form $?C$, yielding the following situation:

\[

\vlderivation{

\vliin{\cut}{}{? \Sigma, !B, \Delta }{

\vlin{!}{}{? \Sigma, !B , ?C}{\vlhy{?\Sigma , B , ?C}  }

}{

\vlin{\rho'}{}{!C^\perp , \Delta}{\vlhy{\vlvdots}}

}

}

\]

Now, if $!C^\perp$ is principle for $\rho'$ then $\rho'\in \{! , \indr\}$ and so $\Delta $ must be $?$-ed; in this case we are able to apply the transformation \eqref{eqn:com-case-unary-simple}. Otherwise $A^\perp$ is not principal for $\rho'$ and so $\rho' \notin \{! , \indr \}$, which means we can apply \ref{subcase:unary-commutation-vanilla} along this side of the subproof.

\item $\rho$ is a $\indr$-step. Therefore $\Gamma$ has the form $? \Sigma , B^\perp(x), B(s x) $ and $A$ has the form $?C$, and the argument is similar to the case above.

% yielding the following situation:

%\[

%\vlderivation{

%	\vliin{\cut}{}{? \Sigma, B^\perp (0) , B(t), \Delta }{

%		\vlin{\indr}{}{? \Sigma, B^\perp (0) , B(t) , ?C}{\vlhy{?\Sigma , B^\perp(x) , B(s x) , ?C}  }

%	}{

%	\vlin{\rho'}{}{!C^\perp , \Delta}{\vlhy{\vlvdots}}

%}

%}

%\]

\end{enumerate}

\item A cut-step is immediately preceded by a $\vlte $-step:

\[

\vlderivation{

\vliin{\cut}{}{\Gamma,\Delta,\Sigma,A\vlte B }{

\vliin{\vlte}{}{\Gamma,\Delta,A\vlte B,C }{\vlhy{\Gamma,A,C}}{\vlhy{\Delta,B}}

}{\vlhy{ \Sigma , C^\bot  }}

}

\quad\to\quad

\vlderivation{

\vliin{\vlte}{}{\Gamma,\Delta,\Sigma,A\vlte B}{

\vliin{\cut}{}{\Gamma,\Sigma,A}{\vlhy{\Gamma,A,C}}{\vlhy{\Sigma,C^\bot}}

}{\vlhy{\Delta,B}}

}

\]

%Notice that this commutation might increase the height of any cuts below along the right branch of the indicated cut, but decreases the height along the left branch.

\item\label{CommCaseAmpersand} A cut-step is immediately preceded by a $\vlan$-step.

\[

\vlderivation{

\vliin{\cut}{}{ \Gamma,\Delta,A\vlan B }{ \vliin{\vlan}{}{\Gamma,A\vlan B,C}{ \vlhy{\Gamma,A,C} }{\vlhy{\Gamma,B,C}}}{ \vlhy{\Delta, C^\bot} }

}

\quad\to\quad

\vlderivation{

\vliin{\vlan}{}{\Gamma,\Delta,A\vlan B }{

\vliin{cut}{}{\Gamma,\Delta,A }{ \vlhy{\Gamma,A,C} }{ \vlhy{ \Delta,C^\bot } }

}{

\vliin{ \cut }{}{\Gamma,\Delta,B}{ \vlhy{\Gamma,B,C } }{ \vlhy{\Delta,C^\bot} }

}

}

\]

\item (No rule for cuts commuting with cuts.)

%A cut-step is immediately preceded by another cut-step:

\[

\vlderivation{

	\vliin{\cut}{}{\Gamma, \Delta, \Sigma}{

		\vliin{\cut}{}{\Gamma, \Delta, B}{\vlhy{\Gamma, A}}{\vlhy{\Delta, \lnot{A}, B}}

		}{\vlhy{\Sigma, \lnot{B}}}

	}

	\quad\to\quad

\vlderivation{

	\vliin{\cut}{}{\Gamma, \Delta, \Sigma}{\vlhy{\Gamma, A}}{

		\vliin{\cut}{}{\Delta, \Sigma, \lnot{A}}{\vlhy{\Delta, \lnot{A}, B}}{\vlhy{\Sigma, \lnot{B}}}

		}

	}

\]

\end{enumerate}

\subsection{Key cases: structural steps}

%[THIS SECTION MIGHT NOT BE NECESSARY]

We attempt to permute cuts on exponential formulae over structural steps whose principal formula is active for the cut. 

We use the commutative case \ref{CaseCommOneStep} to assume that the topmost cut-step in a sequence has already been permuted up to its origin on the $!$-side. 

We have two cases.

\begin{enumerate}

\item\label{StructStepCont} The structural step preceding the cut is a weakening:

\[

\vlderivation{

\vliin{\cut}{}{?\Gamma,\Delta}{ \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} } }{ \vlin{w}{}{ ?A^\bot }{ \vlhy{\Delta	} } }

}

\quad\to\quad

\vlinf{w}{}{?\Gamma,\Delta}{ \Delta }

\]

%\item The structural step preceding the cut is a contraction:

%\[

%\vlderivation{

%\vliin{\cut}{}{ ?\Gamma,\Delta }{

% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%}{ \vlin{c}{}{ ?A^\bot , \Delta }{ \vlhy{ ?A^\bot , ?A^\bot ,  \Delta} } }

%}

%\quad\to\quad

%\vlderivation{

%\vliq{c}{}{?\Gamma, \Delta}{

%\vliin{\cut}{}{?\Gamma, ?\Gamma,\Delta }{

% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%}{

%\vliin{\cut}{}{?\Gamma,?A^\bot , \Delta }{

% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%}{ \vlhy{?A^\bot , ?A^\bot , \Delta } }

%}

%}

%}

%\]

%OR use a multicut:

%\[

%\vlderivation{

%\vliin{\cut}{}{ ?\Gamma,\Delta }{

% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%}{ \vlin{c}{}{ ?A^\bot , \Delta }{ \vlhy{ ?A^\bot , ?A^\bot ,  \Delta} } }

%}

%\quad\to\quad

%\vlderivation{

%\vliin{\multicut}{}{?\Gamma,?A^\bot , \Delta }{

% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%}{ \vlhy{?A^\bot , ?A^\bot , \Delta } }

%}

%\]

\item The structural step preceding a cut is a contraction:

\[

\vlderivation{

	\vliin{\cut}{}{?\Gamma, \Sigma }{ \vlhy{?\Gamma,!A^\bot} }{

		\vlin{\cntr}{}{ ?A,\Sigma }{ \vlhy{ ?A,?A,\Sigma } }

	}

}

\quad\to\quad

\vlderivation{

	\vliq{\cntr}{}{ ?\Gamma,\Sigma }{

		\vliin{\cut}{}{ ?\Gamma,?\Gamma,\Sigma }{ \vlhy{?\Gamma,!A^\bot } }{

			\vliin{\cut}{}{ ?A,?\Gamma,\Sigma }{ \vlhy{?\Gamma,!A^\bot} }{ \vlhy{ ?A,?A,?\Delta,\Sigma } }

		}

	}

}

\]

%\item The structural step preceding a cut is a parallel contraction:

%\[

%\vlderivation{

%\vliin{\cut}{}{?\Gamma,?\Delta, \Sigma }{ \vlhy{?\Gamma,!A^\bot} }{

%\vlin{}{}{ ?A,?\Delta,\Sigma }{ \vlhy{ ?A,?A,?\Delta,?\Delta,\Sigma } }

%}

%}

%\quad\to\quad

%\vlderivation{

%\vlin{}{}{ ?\Gamma,?\Delta,\Sigma }{

%\vliin{\cut}{}{ ?\Gamma,?\Gamma,?\Delta,?\Delta,\Sigma }{ \vlhy{?\Gamma,!A^\bot } }{

%\vliin{\cut}{}{ ?A,?\Gamma,?\Delta,?\Delta,\Sigma }{ \vlhy{?\Gamma,!A^\bot} }{ \vlhy{ ?A,?A,?\Delta,?\Delta,\Sigma } }

%}

%}

%}

%\]

\end{enumerate}

\subsection{Key cases: logical steps}

Finally, once all cuts have been permuted maximally on both sides, we have the cases when the cut-formula is principal for a preceding logical step on both sides. We have three cases, one for every pair of connectives.

\begin{enumerate}

\item The cut-formula is multiplicative:

\[

\vlderivation{

\vliin{\cut}{}{ \Gamma,\Delta,\Sigma }{

\vliin{\vlte}{}{ \Gamma,\Delta,A\vlte B }{ \vlhy{\Gamma,A} }{ \vlhy{\Delta,B} }

}{ \vlin{\vlpa}{}{ \Sigma, A^\bot \vlpa B^\bot }{ \vlhy{\Sigma , A^\bot , B^\bot} } }

}

\quad\to\quad

\vlderivation{

\vliin{\cut}{}{ \Gamma,\Delta,\Sigma }{ \vlhy{\Gamma,A} }{

\vliin{\cut}{}{ \Delta,\Sigma,A^\bot }{ \vlhy{\Delta,B} }{ \vlhy{\Sigma , A^\bot,B^\bot } }

}

}

\]

\item The cut-formula is additive,

\[

\vlderivation{

\vliin{\cut}{}{ \Gamma,\Delta }{ 

\vliin{\vlan}{}{ \Gamma,A\vlan B }{ \vlhy{\Gamma,A} }{ \vlhy{\Gamma,B} }

 }{ \vlin{\vlor}{}{ \Delta,A^\bot\vlor B^\bot }{ \vlhy{\Delta, A^\bot } } }

}

\quad\to\quad

\vliinf{\cut}{}{ \Gamma,\Delta }{ \Gamma,A }{ \Delta,A^\bot }

\]

where the case for the other $\vlor$-rule is symmetric.

\item The cut-formula is exponential.

\[

\vlderivation{

\vliin{\cut}{}{ ?\Gamma,\Delta }{

 \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

}{

\vlin{?}{}{ \Delta,?A^\bot }{ \vlhy{\Delta, A^\bot } }

}

}

\quad\to\quad

\vliinf{\cut}{}{ ?\Gamma,\Delta }{ ?\Gamma,A }{ \Delta,A^\bot }

\]

\item The cut-formula is quantified.

\[

\vlderivation{

	\vliin{\cut}{}{\Gamma, \Delta}{

		\vlin{\forall}{}{\Gamma, \forall x. A(x)}{\vltr{\pi(a)}{\Gamma, A(a)}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}}

		}{

		\vlin{\exists}{}{\Delta, \exists x . \lnot{A}(x)}{\vlhy{\Delta, \lnot{A}(t)}}

		}

	}

	\quad \to \quad

	\vlderivation{

		\vliin{\cut}{}{\Gamma, \Delta}{

			\vltr{\pi(t)}{\Gamma, A(t)}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

			}{\vlhy{\Delta, \lnot{A}(t)}}

		}

\]

\end{enumerate}

\end{document}