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

%\newtheorem{theorem}{Theorem}    %% Patrick: added for 'article' class version

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

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

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

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

\theoremstyle{plain}

\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{\IH}{\mathit{IH}}

\newcommand{\defined}{:=}

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

\vllineartrue

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

%specification

\newcommand{\eqspec}{\mathcal E}

\newcommand{\closure}[1]{\overline{#1}}

\newcommand{\conv}{\mathit{Conv}}

% theories

\newcommand{\theory}{\mathcal T}

\newcommand{\system}{\mathcal S}

%terms

\newcommand{\pred}{p}

\newcommand{\cond}{C}

\renewcommand{\succ}{\mathsf{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}{\rightarrow}

\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{\word}{W}

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

\newcommand{\Word}{\mathbb{W}}

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

%equality

\newcommand{\refl}{\mathit{ref}}

\newcommand{\symm}{\mathit{sym}}

\newcommand{\trans}{\mathit{trans}}

\newcommand{\subst}{\mathit{sub}}

%rules

\newcommand{\inv}[1]{#1\text{-inv}}

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

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

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

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

\newcommand{\sigone}{\Sigma^{\word^+}_1 }

\newcommand{\sigzer}{\Sigma^{\word^+}_0}

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

\newcommand{\arith}{I\sigone}

% sizes

\newcommand{\height}[1]{\mathit{h}(#1)}

\section{Introduction}

%\anupam{i put all the notes/suggestions at the end, before references.}

\emph{Free-cut elimination}\footnote{Also known as \emph{anchored} or \emph{directed} completeness, \emph{partial} cut-elimination or \emph{weak} cut-elimination in other works.} is a normalisation procedure on formal proofs in systems including nonlogical rules, e.g.\ the axioms and induction rules in arithmetic, introduced in \cite{Takeuti87}. It yields proofs in a form where, essentially, each cut step has at least one of its cut formulas principal for a nonlogical step. It is an important tool for proving witnessing theorems in first-order theories, and in particular it has been extensively used in \emph{bounded arithmetic} for proving complexity bounds on representable functions, by way of the \textit{witness function method} \cite{Buss86book}. 

Linear logic \cite{Girard87} is a decomposition of both intuitionistic and classical logic, based on a careful analysis of duplication and erasure of formulas. It has been useful in proofs-as-programs correspondences, proof search \cite{Andreoli92} and logic programming \cite{Miller04}. By controlling  structural rules with designated modalities, the \textit{exponentials}, linear logic has allowed for a fine study of complexity bounds in the Curry-Howard interpretation, inducing variants with polynomial-time complexity \cite{GirardSS92:bounded-ll} \cite{Girard98} \cite{Lafont04}. 

%   However most of this work has been done for 'purely logical' linear logic, or at least for variants with full cut elimination procedure. 

In this work we explore how the finer granularity of linear logic can be used to control complexity in \emph{first-order theories}, restricting the provably convergent functions rather than the typable terms as in the propositional setting.

%     aim at exploring in which way the complementary techniques of free-cut elimination and linear logic can be combined to analyze properties of first-order theories in which structural rules play a critical r\^ole. 

We believe this to be of general interest, in particular to understand the effect of substructural restrictions on nonlogical rules, e.g.\ induction, in mathematical theories. Some related works exist, e.g.\ the na\"ive set theories of Girard and Terui \cite{Girard94:lll} \cite{Terui04}, but overall it seems that the first-order proof theory of linear logic is still rather undeveloped; in particular, to our knowledge, there seems to be no general form of free-cut elimination available in the literature (although special cases occur in \cite{LincolnMSS92} and \cite{Baelde12}). Thus our first contribution, in Sect.~\ref{sect:free-cut-elim}, is to provide general sufficient conditions on nonlogical rules for a first-order linear logic system to admit free-cut elimination.

\newcommand{\FP}{\mathbf{FP}}

We illustrate the usefulness of this result by proving a witnessing theorem for an arithmetic in linear logic, showing that the provably convergent functions are precisely the polynomial-time computable functions (Sects.~\ref{sect:bc-convergence} and \ref{sect:wfm}), henceforth denoted $\FP$. Our starting point is an axiomatisation $\mathcal{A}_2^1$ from \cite{BelHof:02}, based on a modal logic, already known to characterise $\FP$.

%    In this system ,following Leivant \cite{Leivant94:intrinsic-theories} functions are defined by first-order equational specifications. 

%    The main result of $\mathcal{A}_2^1$ is then that the provably total functions are exactly the polynomial time class. 

This approach, and that of \cite{Leivant94:found-delin-ptime} before, differs from the bounded arithmetic approach since it does not employ bounds on quantifiers, but rather restricts nonlogical rules by substructural features of the modality \cite{BelHof:02} or by \emph{ramification} of formulas  \cite{Leivant94:intrinsic-theories}. The proof technique employed in both cases is a realisability argument, for which \cite{Leivant94:found-delin-ptime} operates directly in intuitionistic logic, whereas \cite{BelHof:02} obtains a result for a classical logic via a double-negation translation, relying on a higher-type generalisation of \emph{safe recursion}

%     which is applied to an intuitionistic version of the theory. In  \cite{BelHof:02} the target language of the realizability argument is a higher-order language \cite{Hofmann00}, SLR, based on safe recursion 

\cite{BellantoniCook92}. 

%     In a second step the result is extended to the classical variant $\mathcal{A}_2^1$ by using the Friedman A translation.

We show that Buss' witness function method can be employed to extract functions directly for classical systems similar to $\mathcal{A}_2^1$ based in linear logic, by taking advantage of free-cut elimination. The De Morgan normal form available in classical (linear) logic means that the functions we extract remain at ground type, based on the usual safe recursive programs of \cite{BellantoniCook92}. A similar proof method was used by Cantini in \cite{Cantini02}, who uses combinatory terms as the model of computation as opposed to the equational specifications in this work.\footnote{This turns out to be important due to the handling of right-contraction steps in the witnessing argument.}

%    We show that the witness function method can be employed to extract functions directly for classical systems similar to $\mathcal{A}_2^1$ based on linear logic, taking advantage of free-cut elimination. De Morgan normal forms available in classical (linear) logic mean that extracted functions remain at ground type, based on the safe recursive programs of \cite{BellantoniCook92}. A similar proof method was used by Cantini \cite{Cantini02} using combinatory logic as the model of computation as opposed to the equational specifications in this work.\footnote{This turns out to be important due to the handling of right-contraction steps in the witnessing argument.}

Our result holds for an apparently weaker theory than $\mathcal{A}_2^1$, with induction restricted to positive existential formulas in a way similar to Leivant's $\mathit{RT}_0$ system in \cite{Leivant94:intrinsic-theories} (see also \cite{Marion01}), but the precise relationship between the two logical settings is unclear.

%

%   Our result holds for an apparently weaker theory than $\mathcal{A}_2^1$, with induction restricted to positive existential formulas in a way similar to Leivant's $\mathit{RT}_0$ system in \cite{Leivant94:intrinsic-theories}, but the precise relationship between the two logical settings is unclear.

%    We illustrate in the same time the relationship between  $\mathcal{A}_2^1$ and linear logic, which was hinted but not investigated in the original paper  \cite{BelHof:02}.  

We conclude in Sect.~\ref{sect:conclusions} with a survey of related work and some avenues for further applications of the free-cut elimination result. 

%More detailed proofs of the various results herein can be found in the appendices, Sects.~\ref{sect:app-preliminaries}-\ref{sect:app-wfm}.

A version of this article containing further proof details in appendices is available \cite{BaiDas}.

%in the appendices, Sects.~\ref{sect:app-preliminaries}-\ref{sect:app-wfm}. 

%Everything else remains the same, with the exception of this paragraph.

\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, so that formulae are always in De Morgan normal form, 

%and this is reflected in the sequent system below. We have included 

and we also consider

rules for arbitrary weakening when 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:\footnote{We consider a two-sided system since it is more intuitive for certain nonlogical rules, e.g.\ induction, and also convenient for the witness function method we use in Sect.~\ref{sect:wfm}.}

	\[

	\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 the rule $\lefrul{\lor}$ (and similarly for all rules for the binary connectives) and $?A$ in the 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} is 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  In $(R)$  the sequent $ \Sigma'$ (resp. $\Delta'$) does not contain any formula of the shape $?B$ (resp. $!B$), and  in $\init$ the formula $A$ is not of the form  $!B$.

\end{enumerate}

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

Conditions 2 and 3 are standard requirements for nonlogical rules, independently of the logical setting, cf.\ \cite{Beckmann11}. Condition 2 reflects the intuitive idea that, in our nonlogical rules, we often need a notion of \textit{bound} variables in the active formulas (typically for induction rules), for which we rely on eigenvariables. 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 for the free-cut elimination argument 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{\laor}, \rigrul{\laand}, \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.

Due to these results notice that, in place of the equality axioms, we can work in a quantifier-free system of rules:

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

\section{Free-cut elimination in linear logic}

\label{sect:free-cut-elim}

% While in plain 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 $\mathcal T$ . For this reason we need now to define the kind of cuts that  will remain in proofs after reduction. We will call these \textit{anchored cuts}. 

We first define which cut instances may remain in proofs after free-cut elimination.

%  They are called \textit{anchored cuts}.

%   Our first idea would be to consider as anchored  a cut whose cut-formulas  $A$ in the two premises are both principal for their rule, and at least one of these rules is non-logical. Now, the problem with this tentative definition is that a rule (R) of  $\mathcal T$ can contain several principal formulas  (in $\Sigma'$, $\Delta'$) and so we would like to allow an anchored cut on each of these principal formulas.

%  % Consider for instance the following derivation, where we have underlined principal formulas:

%  See for instance (the principal formulas are underlined):

%  \patrick{Anupam, could you please display this derivation in a suitable way?}

%  \[

%  \vlderivation{

%\vliin{cut_2}{}{ \seqar  \Delta}{

%\vliin{cut_1}{}{\seqar A_2 }{\vlin{\rigrul{\lor}}{}{\seqar \underline{A_1}}{}}{\vliin{(R)}{}{\underline{A_1}\seqar \underline{A_2}}{}{} }

%}{

%\vliin{\lefrul{\land}}{}{\underline{A_2}\seqar \Delta}{}{}

%}

%}

%\]

%  Here $cut_1$ is anchored in this sense, but not $cut_2$.   Therefore we propose a more general definition:

Since our nonlogical rules may have many principal formulae on which cuts may be anchored, we need a slightly more general notion of principality.

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

	We define the notions of \textit{hereditarily principal formula} and \textit{anchored cut} in a $\system$-proof, for a system $\system$, by mutual induction as follows:

	\begin{itemize}

		\item A formula $A$ in a sequent $\Gamma \seqar \Delta$ is \textit{hereditarily principal} for a rule instance (S) if either (i) the sequent is in the conclusion of (S) and $A$ is principal in it, or 

		(ii)  the sequent is in the conclusion of an anchored cut, the direct ancestor of $A$ in the corresponding premise is hereditarily principal for the rule instance (S), and the rule (S) is nonlogical.

		\item A cut-step is an \textit{anchored cut} if the two occurrences of its cut-formula $A$ in each premise are hereditarily principal for nonlogical steps, or one is hereditarily principal for a nonlogical step and the other one is principal for a logical step.

	\end{itemize}

	A cut which is not anchored will also be called a \textit{free-cut}.

\end{definition}

As a consequence of this definition, an anchored cut on a formula $A$ has the following properties:

\begin{itemize}

	\item At least one of the two premises of the cut has above it a sub-branch of the proof which starts (top-down) with a nonlogical step (R) with $A$ as one of its principal formulas, and then a sequence of anchored cuts in which $A$ is part of the context.

	\item The other premise is either of the same form or is a logical step with principal formula $A$. 

\end{itemize}

%  

%  Now, for instance a cut on a (principal) 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.

%   

%  With this new definition both $cut_1$ and $cut_2$ in the previous example are anchored.

%   \patrick{@Anupam: if we need to shorten this part, I think we should anyway keep the key lemmas \ref{lem:hereditaryprincipalnonlogical} and \ref{lem:keycommutations}.  In the proof of the thm itself, I would give priority to keep the first case, maybe by skipping the first situation and keeping the second item, $S_1$=$!r$, $?l$ or $R$. Second case could be kept too, and third case could be briefly summarized and pushed in the appendix or online version.}

%   Let us first prove a key lemma on hereditarily principal formulas:

Due to condition 4 in Sect.~\ref{sect:preliminaries}, we have the following:

\begin{lemma}\label{lem:hereditaryprincipalnonlogical}

	A formula occurrence $A$ on the LHS (resp.\ RHS) of a sequent and hereditarily principal for a nonlogical rule (R) 

	cannot be of the form $A=?A'$ (resp. $A=!A'$).

\end{lemma}

Now we can state the main result of this section:

\begin{theorem}

	[Free-cut elimination]

	\label{thm:free-cut-elim}

	Given a system  $\system$, any  $\system$-proof $\pi$ can be transformed into a $\system$-proof $\pi'$ with same end sequent and without any free-cut.

\end{theorem}

%The proof will be given below. It will proceed

The proof proceeds in a way similar to the classical proof of cut elimination for linear logic,

%, but here for eliminating only free-cuts, and one has to check that all steps of the reasoning are compatible with the fact that the proof here also contains $\mathcal{T}$ rules. 

%%     Define the \textit{degree} of a formula as the number of logical connectives or quantifiers in it.  Let us first state an easy building-block of the proof, which comes from standard linear logic:

%%    \begin{lemma}[Logical non-exponential cut-elimination steps]\label{lem:logical steps}

%%    Any cut $c$ whose cut-formulas $A$ are both principal formulas of logical rules distinct from $?$, $!$, $wk$, $cntr$ rules can be replaced in one step by cuts on formulas of strictly lower degree (0, 1 or 2 cuts).

%%    \end{lemma}

%%    \begin{proof}

%%    This is exactly as in plain linear logic. Just note that the case of a quantifier formula involves a substitution by a term $t$ throughout the proof, and this is where we need condition 3 on non-logical rules requiring that they are closed by substitution.

%%    \end{proof}

%    Actually the most important part of the proof of Thm \ref{thm:free-cut-elim} is  the handling of the commutation steps, since this is where the new non-logical rules could raise some problems.

but eliminating only free-cuts and verifying compatibility with our notion of nonlogical rule, in particular for the commutation cases.

First, observe that the only rules in which there is a condition on the context are the following ones: $(\rigrul{\forall})$, $(\lefrul{\exists})$, $(\rigrul{!})$, $(\lefrul{?})$, $(R)$. These are thus the rules for which the commutation with cut steps are not straightforward. Commutations with logical rules  other than $(\rigrul{!})$, $(\lefrul{?})$ are done in the standard way, as in pure linear logic:\footnote{Note that, for the $(\rigrul{\forall})$, $(\lefrul{\exists})$ rules, there might also be a global renaming of eigenvariables if necessary.}

\begin{lemma}[Standard commutations]\label{lem:standardcommutations}

	Any logical rule  distinct from $(\rigrul{!})$, $(\lefrul{?})$ can be commuted under a cut. If the logical rule is binary this may produce two cuts, each in a separate branch.

\end{lemma}

%     In the following we will need to be more careful about rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$. For that we establish our second key lemma:

For rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$ we establish our second key lemma:

\begin{lemma}[Key commutations]\label{lem:keycommutations}

	A cut of the following form, where $?A$ is not principal for $(R)$, can be commuted above the $(R)$ step:

	\[

	\vliinf{cut}{}{ !\Gamma', \Gamma,  \Sigma'   \seqar \Delta', ?A, ?\Pi, ?\Pi'}

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

	{  

		%                    	\vlinf{}{}{?A, !\Gamma' \seqar  ?\Pi'}{} 

		?A, !\Gamma' \seqar  ?\Pi'

	} 

	\]

	Similarly if $(R)$ is replaced with $(\rigrul{!})$, with $?A$ in its RHS context, and also for the symmetric situations:

	cut on the LHS of the conclusion of an $(R)$ or a $(\lefrul{?})$ step on a (non-principal) formula $!A$, with a sequent $!\Gamma' \seqar  ?\Pi', !A$.

\end{lemma}  

\begin{proof}

	The derivation is transformed as follows:

	\[

	\vlinf{(R)}{}{ !\Gamma', !\Gamma,  \Sigma'   \seqar \Delta', ?\Pi, ?\Pi'}

	{ \vliinf{cut}{}{\{!\Gamma', !\Gamma, \Sigma_i  \seqar \Delta_i, ?\Pi,?\Pi' \}_{i\in I}} {

			%                                 		 \vlinf{}{}{ !\Gamma, \Sigma_i  \seqar \Delta_i, ?A, ?\Pi}{}

			!\Gamma, \Sigma_i  \seqar \Delta_i, ?A, ?\Pi

		} {

		%                                 		  \vlinf{}{}{?A, !\Gamma' \seqar  ?\Pi'}{} 

		?A, !\Gamma' \seqar  ?\Pi'

	} }

	\]

	Here if an eigenvariable in $\Sigma_i, \Delta_i$ happens to be free in $!\Gamma', ?\Pi'$ we rename it to avoid the collision, which is possible because by condition 2 on nonlogical rules these eigenvariables do not appear in $\Sigma', \Delta'$ or $!\Gamma, ?\Pi$. So the occurrence of $(R)$ in this new subderivation is valid.

	Similarly  for the symmetric derivation with a cut on the LHS of the conclusion of an $(R)$ on a formula $!A$.

	The analogous situations with rules  $(\rigrul{!})$ and $(\lefrul{?})$ are handled in the same way, as usual in linear logic.

\end{proof}

%Now we have all the necessary lemmas to proceed with the proof of the theorem.

Now we can prove the main free-cut elimination result:

\begin{proof}[Proof sketch of Thm.~\ref{thm:free-cut-elim}]

	Given a cut step $c$ in a proof $\pi$, we call  \emph{degree} $\deg( c)$  the number of connectives and quantifiers of its  cut-formula. Now the \emph{degree} of $\pi$, $\deg( \pi)$, is the multiset of the degrees of its non-anchored cuts. We consider the usual Dershowitz-Manna ordering on multisets of natural numbers \cite{Dershowitz:1979:PTM:359138.359142}.\footnote{Let $M,N: \Nat \to \Nat$ be two multisets of natural numbers. Then $M<N$ if $M\neq N$ and, whenever $M(x) > N(x)$ there is some $y >x$ such that $N(y) > M(y)$. When $M$ and $N$ are finite, i.e.\ have finite support, $<$ is well-founded.}

	The proof proceeds by induction on $\deg( \pi)$.  For a given degree we proceed with a sub-induction on the \textit{height} $\height{\pi}$ of the proof.

	Consider a proof $\pi$ of non-null degree. We want to show how to reduce it to a proof of strictly lower degree. Consider a top-most non-anchored cut $c$ in $\pi$, i.e.\ such that there is no non-anchored cut above $c$.  Let us call $A$ the cut-formula, and $(S_1)$ (resp. $(S_2)$) the rule above the left (resp. right) premise of $c$.  

	\[    

	\vliinf{c \; \; \cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \vlinf{S_1}{}{\Gamma \seqar \Delta, A}{} }{\vlinf{S_2}{}{\Sigma, A \seqar \Pi}{}}

	\]

	Intuitively we proceed as follows: if $A$ is not hereditarily principal in one of its premises  we try to commute $c$ with the rule along its left premise  $(S_1)$, and if not possible then commute it with the rule along its right premise $(S_2)$, by Lemmas \ref{lem:hereditaryprincipalnonlogical}, \ref{lem:standardcommutations} and \ref{lem:keycommutations}. If $A$ is hereditarily principal in both premises we proceed with a cut-elimination step, as in standard linear logic. For this second step, the delicate part is the elimination of exponential cuts, for which we use a big-step reduction. This works because the contexts in the nonlogical rules $(R)$ are marked with $!$ (resp. $?$) on the LHS (resp. RHS). 

	%    See the appendix for the full proof.

\end{proof}

%   \begin{itemize}

%    \item \textbf{First case}: the cut-formula $A$ on the l.h.s. of  $c$ is non hereditarily principal. 

%    

%\begin{itemize}

%\item Consider first the situation where $(S_1)$ is not one of the rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$.

%

%In this case the commutation of $c$ with $(S_1)$ can be done in the usual way, by using Lemma \ref{lem:standardcommutations}. Let us handle as an example the case where $(S_1)=(\rigrul{\laand})$.

%{\small

%\[

%\vlderivation{

%\vliin{c}{}{ \Gamma, \Sigma \seqar B_1\vlan B_2, \Delta, \Pi }{ \vliin{S_1=\rigrul{\vlan}}{}{\Gamma  \seqar B_1\vlan B_2, \Delta, A}{ \vlhy{\Gamma  \seqar B_1, \Delta, A} }{\vlhy{\Gamma  \seqar  B_2,\Delta, A}}}{ \vlhy{ \Sigma, A \seqar  \Pi} }

%}

%\quad\to\quad

%\vlderivation{

%\vliin{\rigrul{\vlan}}{}{  \Gamma, \Sigma \seqar B_1\vlan B_2, \Delta, \Pi  }{

%\vliin{c_1}{}{\Gamma,\Sigma \seqar B_1, \Delta, \Pi }{ \vlhy{\Gamma  \seqar B_1, \Delta, A} }{\vlhy{ \Sigma, A \seqar  \Pi} }

%}{

%\vliin{c_2}{}{\Gamma,\Sigma \seqar B_2, \Delta, \Pi }{ \vlhy{\Gamma  \seqar B_2, \Delta, A} }{\vlhy{ \Sigma, A \seqar  \Pi} }

%}

%}

%\]

%}

%

%Observe that here $c$ is replaced by two cuts $c_1$ and $c_2$. Call $\pi_i$ the sub-derivation of last rule $c_i$, for $i=1,2$. As for $i=1, 2$ we have

%$\deg{\pi_i}\leq \deg{\pi}$ and $\height{\pi_i}< \height{\pi}$ we can apply the induction hypothesis, and reduce $\pi_i$ to a proof $\pi'_i$ of same conclusion and with

%$\deg{\pi'_i} < \deg{\pi_i}$. Therefore  by replacing $\pi_i$ by $\pi'_i$ for $i=1, 2$ we obtain a proof $\pi'$ such that $\deg{\pi'}<\deg{\pi}$.  

%

%The case (S)=($\lefrul{\laor}$) is identical, and the other cases are similar. % (see the Appendix for more examples). 

%

%\item Consider now the case where $(S_1)$ is equal to $(\rigrul{!})$, $(\lefrul{?})$ or $(R)$. Let us also assume that the cut-formula is hereditarily principal in its r.h.s. premise, because if this does not hold we can move to the second case below. 

%

%First consider  $(S_1)=(\rigrul{!})$. As $A$ is not principal in the conclusion of $(\rigrul{!})$ it is of the form $A=?A'$. By assumption we know that  $A=?A'$ in the conclusion of $(S_2)$ is hereditarily principal on the l.h.s., so by Lemma \ref{lem:hereditaryprincipalnonlogical} it cannot be hereditarily principal for a non-logical rule, so by definition of hereditarily principal we deduce that $(S_2)$ is not an $(R)$ rule. It cannot be an  $(\rigrul{!})$ rule either because then $?A'$ could not be a principal formula in its conclusion. Therefore the only possibility is that 

% $(S_2)$ is an  $(\lefrul{?})$ rule. So the r.h.s. premise is of the shape $?A',!\Gamma' \seqar ?\Pi'$ and by Lemma \ref{lem:keycommutations} the commutation on the l.h.s. is possible. We can conclude as previously. The case where  $(S_1)=(\lefrul{?})$ is the same.

% 

% Now consider the case where $(S_1)=(R)$.  As $A$ is not hereditarily principal in the conclusion of $(R)$, it is a context formula and it is on the r.h.s., so by definition of $(R)$ rules it is  the form $A=?A'$. So as before by Lemma \ref{lem:hereditaryprincipalnonlogical} we deduce that   $(S_2)=(\lefrul{?})$, and  so the r.h.s. premise is of the shape $?A',!\Gamma' \seqar ?\Pi'$.  By Lemma \ref{lem:keycommutations} the commutation on the l.h.s. is possible, and so again we conclude as previously.

% \end{itemize}

%    \item \textbf{Second case}: the cut-formulas on the l.h.s. and r.h.s. of  $c$ are both non hereditarily principal. 

%    

%   After the first case we are here left with the situation where  $(S_1)$ is equal to $(\rigrul{!})$, $(\lefrul{?})$ or $(R)$.

%   \begin{itemize}

%    \item Consider the case where  $(S_1)$=$(\rigrul{!})$, $(\lefrul{?})$, so $A$ is of the form $A=?A'$. All cases of commutation of $c$ with $(S_2)$ are as in standard linear logic, except if $(S_2)=(R)$. In this case though we cannot have $A=?A'$ because of the shape of rule $(R)$. So we are done. 

%    \item Consider  $(S_1)=(R)$. Again as $A$ is not principal in the conclusion of $(S_1)$ and on the r.h.s. of the sequent it is a context formula, and thus of the form  $A=?A'$. As $?A'$ is not principal in the conclusion of $(S_2)$, it is thus a context formula on the l.h.s. of sequent, and therefore $(S_2)$ is not a rule $(R)$. So $(S_2)$ is a logical rule. If it is not an $(\rigrul{!})$ or an $(\lefrul{?})$ it admits commutation with the cut, and we are done. If it is equal to $(\rigrul{!})$ or $(\lefrul{?})$ it cannot have $?A'$ as a context formula in the l.h.s. of its conclusion, so these subcases do not occur.  

%   \end{itemize}

% 

%   

%    \item \textbf{Third case}: the cut-formulas on the l.h.s. and r.h.s. of  $c$ are both  hereditarily principal.

%     

%    By assumption $c$ is non anchored, so none of the two cut-formulas is hereditarily principal for a non-logical rule $(R)$. We can deduce from that

%    that the l.h.s. cut-formula is principal for $(S_1)$ and the r.h.s. cut-formula is principal for $(S_2)$. Call $\pi_1$ (resp. $\pi_2$) the subderivation

%    of last rule $(S_1)$ (resp. $(S_2)$).

%     

%    Then we consider the following sub-cases, in order:

%     \begin{itemize}

%         \item \textbf{weakening sub-case}: this is the case  when one of the premises of $c$ is a $wk$ rule. W.l.o.g. assume that it is the left premise of $c$ which is conclusion of $\rigrul{\wk}$, with principal formula $A$. We eliminate the cut by keeping only the l.h.s. proof $\pi_1$, removing the last cut $c$ and last    $\rigrul{\wk}$ rule    on $A$, and by adding enough

%        $\rigrul{\wk}$, $\lefrul{\wk}$ rules to introduce all the new formulas in the final sequent.  The degree has decreased.

%

%      \item \textbf{exponential sub-case}: this is when one of the premises of $c$ is conclusion of a $cntr$, $\rigrul{?}$ or $\lefrul{!}$ rule on a formula $?A$ or $!A$, and the other one is not a conclusion of $\wk$.

%      

%       Assume w.l.o.g. that it is the right premise which is conclusion of $\lefrul{\cntr}$ or $\lefrul{!}$ on $!A$, and thus the only possibility for the left premise is to  be conclusion of $\rigrul{!}$.  This is rule $(S_1)$ on the picture, last rule of the subderivation $\pi_1$, and we denote its conclusion as $!\Gamma' \seqar ?\Delta', !A$. We will use here a global rewriting step. For that consider in $\pi_2$ all the top-most direct ancestors of the cut-formula $!A$, that is to say direct ancestors which do not have any more direct ancestors above. Let us denote them as $!A^{j}$ for $1\leq j \leq k$. Observe that each $!A^{j}$ is principal formula of a rule $\lefrul{!}$ or $\lefrul{wk}$. Denote by $\rho$ the subderivation

%       of $\pi_2$ which has as leaves the sequents premises of these  $\lefrul{!}$ or $\lefrul{wk}$ rules with conclusion containing $!A^{j}$.

%       Let $\rho'$ be a derivation obtained from $\rho$ by renaming if necessary eigenvariables occurring in premises of rules $\lefrul{\exists}$, $\rigrul{\forall}$, $(R)$  so that none of them belongs to $FV(!\Gamma', ?\Delta')$, where we recall that $!\Gamma' \seqar ?\Delta',!A$ is the l.h.s. premise of the cut $c$.

%  Now, let $\pi'_1$ be the immediate subderivation of $\pi_1$, of conclusion       $!\Gamma' \seqar ?\Delta',A$.  We then define the derivation 

%  $\rho''$ obtained from   $\rho'$ in the following way:

%  \begin{itemize}

%  \item add a cut $c_j$ with (a copy) of $\pi'_1$ on $A^j$ at each leaf which is premise of a rule  $\lefrul{!}$;

%  \item add to each sequent coming from $\rho'$  an additional context $!\Gamma'$ on the l.h.s. and an additional context $?\Delta'$ on the r.h.s., and additional $wk$ rules to introduce these formulas below the $\lefrul{wk}$ rules on formulas $!A^{j}$;

%  \item introduce suitable $\lefrul{cntr}$ and $\rigrul{cntr}$ rules after multiplicative binary rules $\rigrul{\land}$, $\lefrul{\lor}$  in such a way to replace $!\Gamma', !\Gamma'$ (resp. $?\Delta', ?\Delta'$) by  $!\Gamma'$ (resp. $?\Delta'$). 

%  \end{itemize}

%  

%  It can be checked that  $\rho''$ is a valid derivation, because all the conditions for context-sensitive rules $(\rigrul{\forall})$, $(\lefrul{\exists})$, $(\rigrul{!})$, $(\lefrul{?})$, $(R)$ are satisfied. In particular the rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$ are satisfied because the contexts have been enlarged with $!$ formulas on the l.h.s. of the sequents ($!\Gamma'$) and ?  formulas on the r.h.s. of the sequents ($?\Gamma'$).  

%  

%  Now, let $\pi'$ be the derivation obtained from $\pi$ by removing the cut $c$ and replacing the subderivation $\rho$ by $\rho''$. The derivation $\pi'$ is a valid one, it has the same conclusion $!\Gamma', \Sigma \seqar ?\Delta', \Pi$ and with respect to $\pi$ we have replaced one non-anchored cut $c$ with at most $k$ ones $c_j$, but which are of strictly lower degree. So $\deg(\pi')<\deg(\pi)$ and we are done.

%

%      

%      \item \textbf{logical sub-case}: we are now left with the case where both premises of $c$ are conclusions of rules others than $?$, $!$, $wk$, $cntr$. We can thus apply Lemma \ref{lem:logical steps}.

%         If one of the premises is an axiom $\lefrul{\bot}$, $\id$ or $\rigrul{\bot}$, then $\pi$ can be rewritten to a suitable proof $\pi'$ by removing $c$ and the axiom rule. Otherwise both premises introduce the same connective, either  $\land$, $\lor$, $\laor$, $\laand$, $\forall$ or $\exists$. In each case a specific rewriting rule replaces the cut $c$ with one cut of strictly lower degree. 

%      %See the Appendix.

%           \end{itemize}

%     \end{itemize}

%     \end{proof}

\section{A variant of arithmetic in linear logic}

\label{sect:arithmetic}

For the remainder of this article we will consider an implementation of arithmetic in the sequent calculus based on the theory $\bharith$ of Bellantoni and Hofmann in \cite{BelHof:02}. The axioms that we present are obtained from $\bharith$ by using linear logic connectives in place of their classical analogues, calibrating the use of additives or multiplicatives in order to be compatible with the completeness and witnessing arguments that we present in Sects.~\ref{sect:bc-convergence} and \ref{sect:wfm}. We also make use of free variables and the structural delimiters of the sequent calculus to control the logical complexity of nonlogical rules.

We will 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 does not have much effect on complexity while also creating a more robust proof theory. For example it induces the equivalence:

\(

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

\).\footnote{Notice that 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.

\newcommand{\lang}{\mathcal L}

\subsection{Axiomatisation and an equivalent rule system}

%\begin{definition}

%[Language]

We consider the language $\lang$ consisting of the constant symbol $\epsilon$, unary function symbols $\succ_0 , \succ_1$ and the predicate symbol  $\word$, together with function symbols $f,g,h$ etc.

%\end{definition}

$\lang$-structures are typically extensions of $\Word = \{ 0,1 \}^*$, in which $\epsilon, \succ_0, \succ_1$ are intended to have their usual interpretations. The $\word$ predicate is intended to indicate those elements of the model that are binary words (in the same way as Peano's $N$ predicate indicates those elements that are natural numbers).

As an abbreviation, we write $\word (\vec t)$ for $\bigotimes^{|\vec t|}_{i=1} \word(t_i)$.

\begin{remark}

	[Interpretation of natural numbers]

	Notice that the set $\Nat^+$ of positive integers is $\lang$-isomorphic to $\Word$ under the interpretation $\{ \epsilon \mapsto 1 , \succ_0 (x) \mapsto 2x , \succ_1 (x) \mapsto 2x+1 \}$, so we could equally consider what follows as theories over $\Nat^+$.

\end{remark}

The `basic' axioms are essentially the axioms of Robinson arithmetic (or Peano Arithmetic without induction) without axioms for addition and multiplication.

%\footnote{They are also similar to the `generative' axioms of Leivant's intrinsic theories [cite] for this signature.} 

Let us write $\forall x^\word . A$ for $\forall x . ( \word(x) \limp A )$ and $\exists x^\word . A$ for $\exists x . ( \word(x) \land A )$. We use the abbreviations $\forall x^{!\word}$ and $\exists x^{!\word}$ similarly.

\newcommand{\wordcntr}{\word_\cntr}

\newcommand{\natcntr}{\nat_\cntr}

\newcommand{\geneps}{\word_{\epsilon}}

\newcommand{\genzer}{\word_{0}}

\newcommand{\genone}{\word_{1}}

\newcommand{\sepeps}{\epsilon}

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

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

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

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

\newcommand{\basic}{\mathit{BASIC}}

\begin{definition}

	[Basic axioms]

	The theory $\basic$ consists of the following axioms:

	\[

	\small

	\begin{array}{rl}

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

	%\geneps 

	& \word(\epsilon) \\

	%\genzer 

	& \forall x^\word . \word(\succ_0 x) \\

	%\genone 

	& \forall x^\word . \word(\succ_1 x) \\

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

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

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

	%\inj & \forall x^\word . \succ_0 x \neq \succ_1 x \\

	%\surj & \forall x^\word . (x = \epsilon \laor \exists y^\word . x = \succ_0 y \laor \exists y^\word . x = \succ_1 y ) \\

	%\noalign{\smallskip}

	%\wordcntr & \forall x^\word . (\word(x) \land \word(x)) 

	\end{array}

	%\quad

	\begin{array}{rl}

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

	%\geneps & \word(\epsilon) \\

	%\genzer & \forall x^\word . \word(\succ_0 x) \\

	%\genone & \forall x^\word . \word(\succ_1 x) \\

	%\sepeps 

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

	%\sepzer 

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

	%\sepone 

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

	%\inj & \forall x^\word . \succ_0 x \neq \succ_1 x \\

	%\surj & \forall x^\word . (x = \epsilon \laor \exists y^\word . x = \succ_0 y \laor \exists y^\word . x = \succ_1 y ) \\

	%\noalign{\smallskip}

	%\wordcntr & \forall x^\word . (\word(x) \land \word(x)) 

	\end{array}

	%\quad

	\begin{array}{rl}

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

	%\geneps & \word(\epsilon) \\

	%\genzer & \forall x^\word . \word(\succ_0 x) \\

	%\genone & \forall x^\word . \word(\succ_1 x) \\

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

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

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

	%\inj 

	& \forall x^\word . \succ_0 x \neq \succ_1 x \\

	%\surj 

	& \forall x^\word . (x = \epsilon \laor \exists y^\word . x = \succ_0 y \laor \exists y^\word . x = \succ_1 y ) \\

	%\noalign{\smallskip}

	%\wordcntr 

	& \forall x^\word . (\word(x) \land \word(x)) 

	\end{array}

	\]

\end{definition}

These axioms insist that, in any model, the set induced by $\word (x)$ has the free algebra $\Word$ as an initial segment. 

Importantly, there is also a form of contraction for the $\word$ predicate.

We will consider theories over $\basic$ extended by induction schemata:

\begin{definition}

	[Induction]

	The \emph{(polynomial) induction} axiom schema, $\ind$, consists of the following axioms,

	\[

	%\begin{array}{rl}

	%& A(\epsilon) \\

	%\limp & !(\forall x^{!\word} . ( A(x) \limp A(\succ_0 x) ) ) \\

	%\limp & !(\forall x^{!\word} . ( A(x) \limp A(\succ_1 x) ) ) \\

	%\limp & \forall x^{!\word} . A(x)

	%\end{array}

	A(\epsilon) 

	\limp !(\forall x^{!\word} . ( A(x) \limp A(\succ_0 x) ) ) 

	\limp  !(\forall x^{!\word} . ( A(x) \limp A(\succ_1 x) ) ) 

	\limp  \forall x^{!\word} . A(x)

	\]

	for each formula $A(x)$.

	For a class $\Xi$ of formulae, $\cax{\Xi}{\ind}$ denotes the set of induction axioms when $A(x) \in \Xi$. 

	We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.

\end{definition}

We use the terminology `polynomial induction' to maintain consistency with the bounded arithmetic literature, e.g.\ in \cite{Buss86book}, where it is distinguished from induction on the \emph{value} of a string (construed as a natural number). The two forms have different computational behaviour, specifically with regards to complexity, but we will restrict attention to $\ind$ throughout this work, and thus may simply refer to it as `induction'.

%\anupam{in fact just give general case for a universal closed formula. Then remark about invertibility of negation giving purely positive initial steps. These occur in section 6 so no need to write them out here.}

\begin{proposition}

	[Equivalent rules]

	\label{prop:equiv-rules}

	$\basic$ is equivalent to the following set of rules,

	\[

	\small

	\begin{array}{l}

	\begin{array}{cccc}

	\vlinf{\geneps}{}{\seqar \word (\epsilon)}{}&

	\vlinf{\genzer}{}{\word(t) \seqar \word(\succ_0 t)}{}&

	\vlinf{\sepeps_0}{}{ \word (t)   \seqar \epsilon \neq \succ_0 t}{} &

	\vlinf{\sepzer}{}{\word (s) , \word (t)  , \succ_0 s = \succ_0 t\seqar s = t }{}\\

	\vlinf{\inj}{}{\word(t) \seqar\succ_0 t \neq \succ_1 t}{}&

	\vlinf{\genone}{}{\word(t) \seqar \word(\succ_1 t)}{}&

	\vlinf{\sepeps_1}{}{ \word (t)   \seqar \epsilon \neq \succ_1 t }{}&

	\vlinf{\sepone}{}{\word (s) , \word (t)  , \succ_1 s = \succ_1 t\seqar s = t }{}

	\end{array}

	\\

	\vlinf{\surj}{}{\word (t) \seqar t = \epsilon \laor \exists y^\word . t = \succ_0 y \laor \exists y^\word . t = \succ_1 y }{}

	\qquad

	\vlinf{\wordcntr}{}{\word(t) \seqar \word(t) \land \word(t) }{}

	\end{array}

	\]

	%\[

	%\vlinf{}{}{\seqar \word (\epsilon)}{}

	%\quad

	%\vlinf{}{}{\word(t) \seqar \word(\succ_0 t)}{}

	%\quad

	%\vlinf{}{}{\word(t) \seqar \word(\succ_1 t)}{}

	%\qquad \qquad 

	%\vlinf{}{}{\word(t) \seqar \word(t) \land \word(t) }{}

	%\]

	%\[

	%\vlinf{}{}{ \word (t)  , \epsilon = \succ_0 t \seqar }{} 

	%\quad

	%\vlinf{}{}{ \word (t)  , \epsilon = \succ_1 t \seqar }{}

	%\quad

	%\vlinf{}{}{\word (s) , \word (t)  , \succ_0 s = \succ_0 t\seqar s = t }{}

	%\quad

	%\vlinf{}{}{\word (s) , \word (t)  , \succ_1 s = \succ_1 t\seqar s = t }{}

	%\]

	%\[

	%\vlinf{}{}{\word(t), \succ_0 t = \succ_1 t \seqar}{}

	%\quad

	%\vlinf{}{}{\word (t) \seqar t = \epsilon \laor \exists y^\word . t = \succ_0 y \laor \exists y^\word . t = \succ_1 y }{}

	%\]

	%\vspace{1em}

	and $\ind$ is equivalent to,

	\begin{equation}

	\label{eqn:ind-rule}

	\small

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

	\end{equation}

	where, in all cases, $t$ varies over arbitrary terms and the eigenvariable $a$ does not occur in the lower sequent of the $\ind$ rule.

\end{proposition}

Note, in particular, that since this system of rules is closed under substitution of terms for free variables, free-cut elimination, Thm.~\ref{thm:free-cut-elim}, applies.

When converting from a $\ind$ axiom instance to a rule instance (or vice-versa) the induction formula remains the same. For this reason when we consider theories that impose logical restrictions on induction we can use either interchangeably.

\begin{remark}

	%\anupam{Mention that two induction rules are not the same. This is crucial in, e.g.\ the completeness section for the case of PRN.}

	Usually the induction axiom is also equivalent to a formulation with a designated premise for the base case:

	\begin{equation}

	\label{eqn:ind-rul-base-prem}

	\vliiinf{}{}{ !\word(t) , !\Gamma  \seqar A(t), ?\Delta }{!\Gamma \seqar A(\epsilon)}{ !\word(a) , !\Gamma, A(a) \seqar A(\succ_0 a) , ?\Delta }{ !\word(a) , !\Gamma, A(a) \seqar A(\succ_1 a) , ?\Delta  }

	\end{equation}

	However, 

	%but 

	this is not true in the linear logic setting since the proof that \eqref{eqn:ind-rul-base-prem} simulates \eqref{eqn:ind-rule} above relies on contraction on the formula $A(\epsilon)$, which is not in general available. Therefore \eqref{eqn:ind-rul-base-prem} is somewhat weaker than \eqref{eqn:ind-rule}, and is in fact equivalent to a version of the induction axiom with $!A(\epsilon)$ in place of $A(\epsilon)$. This distinction turns out to be crucial in Sect.~\ref{sect:bc-convergence}, namely when proving the convergence of functions defined by predicative recursion on notation.

\end{remark}

%

%\subsection{Equivalent rule systems}

%Instead of weakening and induction axioms, we consider the following rules, which are provably equivalent:

%

%\[

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

%\quad

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

%\quad

%\vliinf{\pind}{}{ !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{provable equivalence, if necessary.}

%

%The inclusion of the first two rules places us in an \emph{affine} setting, whereas the induction rule allows better proof theoretic manipulation.

%

%Finally, for each universally quantified axiom, we consider instead the schema of initial rules with unbound terms in place of universally quantified variables, again for proof theoretic reasons:

%\[

%\vlinf{\natcntr}{}{\nat(t) \seqar \nat(t) \land \nat(t) }{}

%\quad

%\vlinf{\nat_\epsilon}{}{\seqar \nat (\epsilon)}{}

%\quad

%\vlinf{\nat_0}{}{\nat(t) \seqar \nat(\succ_0 t)}{}

%\quad

%\vlinf{\nat_1}{}{\nat(t) \seqar \nat(\succ_1 t)}{}

%\]

%\[

%\vlinf{\epsilon^0}{}{ \nat (t)  , \epsilon = \succ_0 t \seqar }{} 

%\quad

%\vlinf{\epsilon^1}{}{ \nat (t)  , \epsilon = \succ_1 t \seqar }{}

%\quad

%\vlinf{\succ_0}{}{\nat (s) , \nat (t)  , \succ_0 s = \succ_0 t\seqar s = t }{}

%\quad

%\vlinf{\succ_1}{}{\nat (s) , \nat (t)  , \succ_1 s = \succ_1 t\seqar s = t }{}

%\]

%\[

%\vlinf{\inj}{}{\nat(t), \succ_0 t = \succ_1 t \seqar}{}

%\quad

%\vlinf{\surj}{}{\nat (t) \seqar t = \epsilon , \exists y^\nat . t = \succ_0 y , \exists y^\nat . t = \succ_1 y }{}

%\]

%%in place of their corresponding axioms.

%

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

%

%

%\anupam{

%NEW INDUCTION STEP:

%\[

%\vliiinf{\pind}{}{!\Gamma, !\nat(t) , \nat (\vec x) \seqar A(t, \vec x) }{!\Gamma , \nat (\vec x) \seqar A(\epsilon, \vec x) }{ !\Gamma, !\nat (a) , \nat (\vec x) , A(a, \vec x) \seqar A(\succ_i a, \vec x) }{!\Gamma, !\nat (a) , \nat (\vec x) , A(a, \vec x) \seqar A(\succ_i a, \vec x)}

%\]

%

%Need to examine strength of this: somewhat weaker since needs actual premiss for base case (only significant because of linear logic), but somewhat stronger because of use of $\nat(\vec x)$ on the left in context.

%}

\subsection{Provably convergent functions}

%

%\anupam{Herbrand-G\"odel equational programs from Kle52, cited in Lei94b.}

%

%\anupam{`coherent' programs, defined by Leivant. = consistent so has a model.}

As in the work of Bellantoni and Hofmann \cite{BelHof:02} and Leivant before \cite{Leivant94:found-delin-ptime}, our model of computation is that of Herbrand-G\"odel style \emph{equational specifications}. These are expressive enough to define every partial recursive function, which is the reason why we also need the $\word$ predicate to have a meaningful notion of `provably convergent function'.

\begin{definition}

	[Equational specifications and convergence]

	An \emph{equational specification} (ES) is a set of equations between terms. We say that an ES is \emph{coherent} if the equality between any two distinct ground terms cannot be proved by equational logic.

	%	\footnote{This is the quantifier-free fragment of first-order logic with equality and no other predicate symbols.}

	The \emph{convergence statement} $\conv (f , \eqspec)$ for an equational specification $\eqspec$ and a function symbol $f$ (that occurs in $\eqspec$) is the following formula:

	\[

	\bigotimes_{A \in \eqspec} ! \forall \vec x . A

	\ \limp \ 

	\forall \vec x^{! \word} .  \word (f (\vec x) )

	\]

\end{definition}

The notion of coherence appeared in \cite{Leivant94:found-delin-ptime} and it is important to prevent a convergence statement from being a vacuous implication. In this work we will typically consider only coherent ESs, relying on the following result which is also essentially in \cite{Leivant94:found-delin-ptime}:

\begin{proposition}

	\label{prop:eq-spec-model}

	%	For every equational specification $\eqspec$, its universal closure has a model.

	The universal closure of a coherent ES $\eqspec$ has a model satisfying $\basic + \ind$.

\end{proposition}

%\begin{proof}

%%\todo{ take $\Word \cup \{\bot\}$ or use completeness? Omit if no time. }

%Consider the standard model $\Word $ extended by an element $\infty$ with $\succ_0 \infty = \succ_1 \infty = \infty$. Setting $\word = \Word$ means this model satisfies $\basic$. Now, for each function symbol $f$, define $f(\sigma) = \tau$ for every $\sigma, \tau \in \Word$ for which this equation is forced by $\eqspec$. Otherwise define $f(\sigma) = f(\infty) = \infty$.

%\todo{replace with argument using completeness.}

%\end{proof}

One issue is that a convergence statement contains universal quantifiers, which is problematic for the extraction of functions by the witness function method later on.

%	\footnote{Intuitively universal quantifiers can be interpreted by type 1 functions. From here, in an intuitionistic setting, a $\forall$-right step can be directly realised, but in the classical setting the presence of side-formulae on the right can cause issues for constructivity.}

We avoid this problem by appealing to the deduction theorem and further invertibility arguments:

Let us write $\closure{\eqspec}$ for the closure of a specification $\eqspec$ under substitution of terms for free variables.

\begin{lemma}

	\label{lemma:spec-norm-form}

	A system $\system$ proves $\conv (f , \eqspec)$ if and only if $\system \cup \closure{\eqspec}$ proves $!\word (\vec a) \seqar \word ( f (\vec a) )$.

\end{lemma}

\begin{proof}[Proof sketch]

	By deduction, Thm.~\ref{thm:deduction}, and invertibility arguments.

\end{proof}	

Notice that the initial rules from $ \closure{\eqspec}$ are also closed under term substitution, and so compatible with free-cut elimination, and that $\closure{\eqspec}$ and $\word (\vec a) \seqar \word ( f (\vec a) )$ are free of negation and universal quantifiers.

\subsection{$\word$-guarded quantifiers, rules and cut-reduction cases}

We consider a quantifier hierarchy here analogous to the arithmetical hierarchy, where each class is closed under positive multiplicative operations. In the scope of this work we are only concerned with the first level:

%We now introduce a quantifier hierarchy of formulae so we can identify the theories that we will be concerned with for the remainder of this article.

%

%

\begin{definition}

	%[Quantifier hierarchy]

	We define $\sigzer $ as the class of multiplicative formulae that are free of quantifiers where $\word$ occurs positively.\footnote{Since our proof system is in De Morgan normal form, this is equivalent to saying that there is no occurrence of $\word^\bot$.}

	The class $\sigone$ is the closure of $\sigzer$ by $\exists$, $\lor$ and $\land$.

	%	For $i> 0$ we define $\Sigma^\word_i$ and $\Pi^\word_i$ as follows:

	%	\begin{itemize}

	%		\item If $A \in \Sigma^\word_{i-1} \cup \Pi^\word_{i-1}$ then $A \in \Sigma^\word_i$ and $A \in \Pi^\word_i$.

	%		\item If $A \in \Sigma^\word_i$ then $\exists x^\word . A \in \Sigma^\word_i$.

	%		\item If $A \in \Pi^\word_i$ then $\forall x^\word . A \in \Pi^\word_i$.

	%		\item If $A,B \in \Sigma^\word_i$ then $A \lor B$ and $A\land B \in \Sigma^\word_i$.

	%		\item If $A,B \in \Pi^\word_i$ then $A \lor B$ and $A\land B \in \Pi^\word_i$.

	%	\end{itemize}

	%	We add $+$ in superscript to a class to restrict it to formulae where $\word$ occurs in only positive context.

\end{definition}

For the remainder of this article we mainly work with the theory $\arith$, i.e.\ $\basic + \cax{\sigone}{\ind}$.

%\vspace{1em}

It will be useful for us to work with proofs using the `guarded' quantifiers $\forall x^\word$ and $\exists x^\word$ in place of their unguarded counterparts, in particular to carry out the argument in Sect.~\ref{sect:wfm}. 

%To this end we introduce rules for these guarded quantifiers and show that they are compatible with free-cut elimination.

%

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

%For the quantifiers $\exists x^\word $ and $\forall x^\word$ we 

Therefore we define the following rules, which are already derivable:

\[

%\begin{array}{cc}

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

%\quad & \quad

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

%\\

%\noalign{\bigskip}

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

%\quad &\quad 

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

%\end{array}

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

\quad

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

\quad 

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

\quad

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

\]

%\begin{proposition}

%	Any principal cut between the quantifier rules above and a logical step is reducible.

%	\end{proposition}

We now show that these rules are compatible with free-cut elimination.

\begin{proposition}\label{prop:logicalstepguardedquantifer}

	Any cut between the principal formula of a quantifier rule above and the principal formula of  a logical step is reducible.

\end{proposition}

\begin{proof}

	For a cut on $\forall x^\word . A(x)$, the reduction is obtained by performing successively the two reduction steps for the $\forall$ and $\limp$ connectives. The case of $\exists x^\word A(x)$ is similar. 

\end{proof}	

\begin{corollary}

	[Free-cut elimination for guarded quantifiers]

	\label{cor:free-cut-elim-guarded-quants}

	Given a system  $\system$, any  $\system$-proof $\pi$ using $\exists x^\word $ and $\forall x^\word$  rules can be transformed into free-cut free form.

\end{corollary}

%\begin{proof}

%  First translate the proof $\pi$ into the proof $\pi_0$ where all guarded quantifiers rules have been replaced by their derivation, and say that two rule instances in $\pi_0$ are \textit{siblings} if they come from the same derivation of a guarded quantifier rule. So in $\pi_0$ any two sibling rules are consecutive. Now observe that in the free-cut elimination procedure:

%  \begin{itemize}

%  \item when we do a commutation step of a cut with a $\forall$ (resp. $\exists$ rule) that has a sibling, we can follow it by another commutation of cut with its sibling,

%  \item when we do a logical cut-elimination step on a $\forall$ (resp. $\exists$ rule) that has a sibling, we can follow it by a logical cut-elimination step on its sibling, as illustrated by Prop. \ref{prop:logicalstepguardedquantifer}.

%  \end{itemize}

%  In this way sibling rules remain consecutive in the proof-tree throughout the reduction, and the procedure transforms the proof into one with only anchored cuts.

%\end{proof}

As a consequence of this Corollary observe that any $I\Sigma^{\word^+}_{1}$-proof can be transformed into a proof which is free-cut free and whose formulas contain only $\exists x^\word$ quantifiers.   

\section{Bellantoni-Cook characterisation of polynomial-time functions}

We recall the Bellantoni-Cook  algebra BC of functions defined by \emph{safe} (or \emph{predicative}) recursion on notation \cite{BellantoniCook92}. These will be employed for proving both the completeness   (all polynomial time functions are provably convergent) and the soundness result (all provably total functions are polynomial time) of $\arith$. We consider function symbols $f$ over the domain  $\Word$ with sorted arguments $(\vec u ; \vec x)$, where the inputs $\vec u$ are called \textit{normal} and $\vec x$ are called \textit{safe}. 

%Each symbol is given with an arity $m$ and a number $n\leq m$ of normal arguments, and will be denoted as $f(\vec{u};\vec{x})$ where $\vec{u}$ (resp. $\vec{x}$) are the normal (resp. safe) arguments.

%We say that an expression is well-sorted if the arities of function symbols in it is respected.

%\patrick{Note that below I used the terminology 'BC programs', to distinguish them from 'functions' in the extensional sense, which I find clearer. But if you prefer to keep 'BC functions' it is all right for me.}

\begin{definition}

	[BC programs]

	BC is the set of functions generated as follows:

	%	\paragraph{Initial functions}

	%	The initial functions are:

	\begin{enumerate}

		\item The constant functions $\epsilon^k$ which takes $k$ arguments and outputs $\epsilon \in \Word$.

		\item The projection functions $\pi^{m,n}_k ( x_1 , \dots , x_m ; x_{m+1} , \dots, x_{m+n} )  := x_k$ for $n,m \in \Word$ and $1 \leq k \leq m+n$.

		\item The successor functions $\succ_i ( ; x) := xi$ for $i = 0,1$.

		\item The predecessor function $\pred (; x) := \begin{cases}

		\epsilon &  \mbox{ if }  x = \epsilon \\

		x' &  \mbox{ if }  x = x'i

		\end{cases}$.

		\item The conditional function 

		\[

		%\begin{array}{rcl}

		%C (; \epsilon, y_\epsilon , y_0, y_1  ) & = & y_\epsilon \\

		%C(; x0 , y_\epsilon , y_0, y_1) & = & y_0 \\

		%C(; x1 , y_\epsilon , y_0, y_1) & = & y_1 

		%\end{array}

		C (; \epsilon, y_\epsilon , y_0, y_1  ) := y_\epsilon 

		\quad

		C(; x0 , y_\epsilon , y_0, y_1) := y_0 

		\quad

		C(; x1 , y_\epsilon , y_0, y_1) := y_1 

		\]

		%		$\cond (;x,y,z) := \begin{cases}

		%		y & \mbox{ if } x=x' 0 \\

		%		z & \text{otherwise}

		%		\end{cases}$.

	\end{enumerate}

	%	One considers the following closure schemes:

	\begin{enumerate}

		\setcounter{enumi}{5}

		\item Predicative recursion on notation (PRN). If $g, h_0, h_1 $ are in BC then so is $f$ defined by,

		\[

		\begin{array}{rcl}

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

		f (\succ_i u , \vec v ; \vec x ) & := & h_i ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) )

		\end{array}

		\]

		for $i = 0,1$,  so long as the expressions are well-formed. % (i.e.\ in number/sort of arguments).

		\item Safe composition. If $g, \vec h, \vec h'$ are in BC then so is $f$ defined by,

		\[

		f (\vec u ; \vec x) \quad := \quad g ( \vec h(\vec u ; ) ; \vec h' (\vec u ; \vec x) )

		\]

		so long as the expression is well-formed.

	\end{enumerate}

\end{definition}

%Note that the  programs of this class can be defined by equational specifications in a natural way, and in the following we will thus silently identify a BC program with the corresponding equational specification.

We will implicitly identify a BC function with the equational specification it induces.

The main property of BC programs is:

\begin{theorem}[\cite{BellantoniCook92}]

	The class of functions representable by BC programs is $\FP$.

\end{theorem}	

Actually this property remains true if one replaces the PRN scheme by the following more general simultaneous PRN scheme \cite{BellantoniThesis}:

$(f^j)_{1\leq j\leq n}$ are defined by simultaneous PRN scheme  from $(g^j)_{1\leq j\leq n}$, $(h^j_0, h^j_1)_{1\leq j\leq n}$ if for $1\leq j\leq n$ we have:

\[

\begin{array}{rcl}

f^j(0, \vec v ; \vec x) & := & g^j(\vec v ; \vec x) \\

f^j(\succ_i u , \vec v ; \vec x ) & := & h^j_i ( u , \vec v ; \vec x , \vec{f} (u , \vec v ; \vec x) )

\end{array}

\]

for $i = 0,1$,  so long as the expressions are well-formed.

%\anupam{simultaneous recursion?}

%\anupam{also identity, hereditarily safe, expressions, etc.}

%\anupam{we implicitly associate a BC program with its equational specification} 

Consider a well-formed expression $t$ built from function symbols and variables. We say that a variable $y$ occurs \textit{hereditarily safe} in $t$ if, for every subexpression $f(\vec{r}; \vec{s})$ of $t$, the terms in $\vec{r}$ do not contain $y$.

For instance $y$ occurs hereditarily safe in $f(u;y,g(v;y))$, but not in $f(g(v;y);x)$.

\begin{proposition}

	[Properties of BC programs]

	\label{prop:bc-properties}

	We have the following properties:

	\begin{enumerate}

		\item The identity function is in BC.

		\item Let $t$ be a well-formed expression built from BC functions and variables, denote its free variables as $\{u_1,\dots, u_n,x_1,\dots, x_k\}$, and assume for each $1\leq i\leq k$, $x_i$ is hereditarily safe in $t$. Then the function $f(u_1,\dots, u_n; x_1,\dots, x_k):=t$ is in BC.

		\item If $f$ is a BC function, then the function $g(\vec{u},v;\vec{x})$ defined as $f(\vec{u};v,\vec{x})$

		is also a BC program.

	\end{enumerate}

	%\begin{proposition}

	%[Properties of BC programs]

	%\label{prop:bc-properties}

	%We have the following properties:

	%\begin{enumerate}

	%\item Hereditarily safe expressions over BC programs are BC definable.

	%\item Can pass safe input to normal input.

	%\end{enumerate}

\end{proposition}

\section{Convergence of Bellantoni-Cook programs in $\arith$}

\label{sect:bc-convergence}

%\anupam{In this section, use whatever form of the deduction theorem is necessary and reverse engineer precise statement later.}

In this section we show that $I\sigzer$, and so also $\arith$, proves the convergence of any equational specification induced by a BC program, hence any function in $\FP$. 

%Since BC programs can compute any polynomial-time function, we obtain a completeness result. In the next section we will show the converse, that any provably convergent function of $\arith$ is polynomial-time computable.

%

The underlying construction of the proof here is similar in spirit to those occurring in \cite{Cantini02} and \cite{Leivant94:found-delin-ptime}. In fact, like in those works, only quantifier-free positive induction is required, but here we moreover must take care to respect additive and multiplicative behaviour of linear connectives.

We will assume the formulation of BC programs with regular PRN, not simultaneous PRN.

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

%We first want to show that the system ${\Sigma^{\word}_1}-{\pind}$ is expressive enough, that is to say that all polynomial-time functions can be represented by some equational specifications that are provably total. To do so   we consider equational specifications of BC-programs.

\begin{theorem}

	%	[Convergence]

	\label{thm:arith-proves-bc-conv}

	If $\eqspec$ is a BC program defining a function $f$, then $I\sigzer$ proves $\conv(f, \eqspec)$.

\end{theorem}

%\anupam{Consider informalising some of these arguments under (some version of) the deduction theorem. Formal stuff can be put in an appendix. Maybe add a remark somewhere about arguing informally under deduction, taking care for non-modalised formulae.}

\begin{proof}[Proof sketch]

	%	We write function symbols in $\arith$ with arguments delimited by $;$, as for BC-programs. 

	We appeal to Lemma~\ref{lemma:spec-norm-form} and show that $\closure{\eqspec} \cup I\sigzer$ proves $\forall \vec{u}^{!\word} . \forall \vec{x}^\word . \word(f(\vec u ; \vec x))$.

	%	\begin{equation}

	%	\label{eqn:prv-cvg-ih}

	%\forall \vec{u}^{!\word} . \forall \vec{x}^\word . \word(f(\vec u ; \vec x))

	%	\end{equation}

	We proceed by induction on the structure of a BC program for $f$, and sketch only the key cases here.

	%	We give some key cases in what follows.

	Suppose $f(u, \vec v ; \vec x)$ is defined by PRN from functions $g(\vec v ; \vec x), h_i ( u , \vec v ; \vec x , y )$.

	%	\[

	%	\begin{array}{rcl}

	%	f(\epsilon,\vec v ; \vec x) & = & g(\vec v ; \vec x) \\

	%	f(\succ_i u , \vec v; \vec x) & = & h_i (u, \vec v ; \vec x , f(u , \vec v ; \vec x))

	%	\end{array}

	%	\]

	%	By the inductive hypothesis we have \eqref{eqn:prv-cvg-ih} for $g,h_0,h_1$ in place of $f$. 

	From the inductive hypothesis for $g$, we construct the following proof,

	\begin{equation}

	\label{eqn:prn-cvg-base}

	\small

	\vlderivation{

		\vliq{\beta}{}{!\word(\vec v) , \word (\vec x) \seqar \word(f (\epsilon , \vec v ; \vec x)) }{

			\vliq{\alpha}{}{!\word (\vec v) , \word (\vec x) \seqar \word (g (\vec v ; \vec x) ) }{

				%					\vltr{\IH}{\seqar \forall \vec v^{!\word} . \forall \vec x^\word . \word (g (\vec v ; \vec x)) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

				%				\vliq{}{}{\seqar \forall \vec v^{!\word} . \forall \vec x^\word . \word (g (\vec v ; \vec x))}{\vlhy{}}

				\vlhy{\seqar \forall \vec v^{!\word} . \forall \vec x^\word . \word (g (\vec v ; \vec x))}

			}

		}

	}

	\end{equation}

	where $\alpha $ is purely logical and $\beta$ is obtained from $\closure{\eqspec}$ and equality.	

	%	We first prove,

	%	\begin{equation}

	%	!\word (a) , !\word (\vec v) , \word (\vec x) \land \word (f( a , \vec v ; \vec x ) )

	%	\seqar

	%	\word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) )

	%	\end{equation}

	%	for $i=0,1$, whence we will apply $\ind$. We construct the following proofs:

	We also construct the proofs,

	\begin{equation}

	\label{eqn:prn-cvg-ind}

	%\vlderivation{

	%	\vlin{\rigrul{\limp}}{}{ \word(\vec x) \limp \word ( f(u, \vec v ; \vec x) )  \seqar \word (\vec x) \limp \word( f(\succ_i u , \vec v ; \vec x) ) }{

	%	\vliq{\gamma}{}{\word(\vec x), \word(\vec x) \limp \word ( f(u, \vec v ; \vec x) )  \seqar \word( f(\succ_i u , \vec v ; \vec x) )   }{

	%		\vliin{\lefrul{\limp}}{}{\word(\vec x), \word(\vec x), \word(\vec x) \limp \word ( f(u, \vec v ; \vec x) )  \seqar \word( f(\succ_i u , \vec v ; \vec x) )    }{

	%			\vlin{\id}{}{\word(\vec x) \seqar \word (\vec x) }{\vlhy{}}

	%			}{

	%			\vliq{\beta}{}{  \word (\vec x) , \word (f(u , \vec v ; \vec x) ) \seqar \word ( f(\succ_i u , \vec v ; \vec x) ) }{

	%				\vliq{\alpha}{}{ \word (\vec x) , \word (f(u , \vec v ; \vec x) ) \seqar \word ( h_i( u , \vec v ; \vec x , f( u, \vec v ; \vec x )) ) }{

	%					\vltr{IH}{ \seqar \forall  u^{!\word}, \vec v^{!\word} . \forall \vec x^\word , y^\word . \word( h_i (u, \vec v ; \vec x, y) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

	%					}

	%				}

	%			}

	%		}

	%	}

	%	}

	\small

	\vlderivation{

		\vlin{\lefrul{\land}}{}{ !\word (a) , !\word (\vec v) , \word (\vec x) \land \word (f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) ) }{

			\vlin{\lefrul{\cntr}}{}{  !\word (a) , !\word (\vec v) , \word (\vec x) , \word (f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) )}{

				\vliin{\rigrul{\land}}{}{   !\word (a) , !\word (\vec v) , \word(\vec x),  \word (\vec x) , \word (f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) )}{

					\vlin{\id}{}{\word (\vec x) \seqar \word (\vec x)}{\vlhy{}}

				}{

				\vliq{\beta}{}{ !\word (u) , !\word(\vec v)  , \word (\vec x) , \word (f ( u , \vec v ; \vec x ) ) \seqar \word (f (\succ_i u , \vec{v} ; \vec x ) )  }{

					\vliq{\alpha}{}{  !\word (u) , !\word (\vec v)  , \word (\vec x) , \word (f ( u , \vec v ; \vec x ) ) \seqar \word ( h_i ( u , \vec v ; \vec x , f( u , \vec v ; \vec x ) ) )   }{

						%					\vltr{\IH}{ \seqar \forall u^{!\word} , \vec v^{!\word} . \forall \vec x^\word , y^\word  .  \word ( h_i ( u, \vec v ; \vec x, y ) ) }{ \vlhy{\quad} }{\vlhy{}}{\vlhy{\quad}}

						%\vliq{}{}{ \seqar \forall u^{!\word} , \vec v^{!\word} . \forall \vec x^\word , y^\word  .  \word ( h_i ( u, \vec v ; \vec x, y ) ) }{\vlhy{}}

						\vlhy{\seqar \forall u^{!\word} , \vec v^{!\word} . \forall \vec x^\word , y^\word  .  \word ( h_i ( u, \vec v ; \vec x, y ) )}

					}

				}

			}

		}

	}

}

\end{equation}

from the inductive hypotheses for $h_i$, where $\alpha$ and $\beta$ are similar to before.

%%	so let us suppose that $\word(\vec v)$ and prove,

%	\begin{equation}

%% \forall u^{!\word} .  (\word(\vec x) \limp \word(f(u , \vec v ; \vec x)  )

%!\word (u) , !\word (\vec v) , \word (\vec x) \seqar \word ( f(u, \vec v ; \vec x) )

%	\end{equation}

%	by $\cax{\Sigma^N_1}{\pind}$ on $u$. After this the result will follow by $\forall$-introduction for $u, \vec v , \vec x$.

%	In the base case we have the following proof,

%	\[

%	\vlderivation{

%	\vlin{\rigrul{\limp}}{}{ \seqar \word (\vec x) \limp \word (f(\epsilon , \vec v ; \vec x )) }{

%		\vliq{\beta}{}{ \word (\vec x) \seqar \word ( f( \epsilon , \vec v ; \vec x) ) }{

%			\vliq{\alpha}{}{ \word (\vec x) \seqar \word ( g (\vec v ; \vec x) ) }{

%				\vltr{IH}{\seqar \forall v^{!\word} . \forall x^\word . \word( g(\vec v ; \vec x) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

%				}

%			}

%		}		

%		}

Finally we compose these proofs as follows:

\[

\small

\vlderivation{

	\vliq{\rigrul{\forall}}{}{ \seqar \forall u^{!\word} , \vec v^{!\word} . \forall \vec x^\word . \word ( f(u , \vec v ;\vec x)  ) }{

		\vliq{\lefrul{\cntr}}{}{ !\word (u), !\word (\vec v) , \word (\vec x) \seqar  \word ( f(u , \vec v ;\vec x)  )  }

		{

			\vliin{\cut}{}{  !\word (u), !\word(\vec v), !\word (\vec v) , \word (\vec x) , \word (\vec x) \seqar  \word ( f(u , \vec v ;\vec x)  )   }{

				%\vltr{\pi_\epsilon}{ !\word (\vec v) , \word (\vec x) \seqar \word ( f( \epsilon , \vec v ; \vec x ) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

				\vlhy{ !\word (\vec v) , \word (\vec x) \seqar \word ( f( \epsilon , \vec v ; \vec x ) ) }

			}

			{

				\vliq{\wk}{}{ !\word (u), !\word (\vec v) , \word (\vec x), \word ( f( \epsilon , \vec v ; \vec x ) ) \seqar \word ( f( u , \vec v ; \vec x ) ) }{

					\vliq{\land\text{-}\mathit{inv}}{}{  !\word (u), !\word (\vec v) , \word (\vec x) ,\word ( f( \epsilon , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( u , \vec v ; \vec x ) )  }{

						\vlin{\ind}{}{   !\word (u), !\word (\vec v) , \word (\vec x) \land \word ( f( \epsilon , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( u , \vec v ; \vec x ) )  }

						{

							\vlhy{

								\left\{

								%\vltreeder{\pi_i}{   !\word (a), !\word (\vec v) , \word (\vec x) \word ( f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( \succ_i u , \vec v ; \vec x ) )  }{\quad}{}{}

								!\word (a), !\word (\vec v) , \word (\vec x) \word ( f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( \succ_i u , \vec v ; \vec x ) )  

								\right\}_i

							}

						}

					}

				}

			}

		}

	}

}

\]

for $i=0,1$, where the steps $\inv{\land}$ are obtained from invertibility of $\lefrul{\land}$.

%For the inductive step, we suppose that $\word (u)$ and the proof is as follows,

%

%where the steps indicated $\alpha$ and $\beta$ are analogous to those for the base case.

%%, and $\gamma$ is an instance of the general scheme:

%%\begin{equation}

%%\label{eqn:nat-cntr-left-derivation}

%%\vlderivation{

%%	\vliin{\cut}{}{ \word (t) , \Gamma \seqar \Delta }{

%%		\vlin{\wordcntr}{}{ \word (t) \seqar \word (t) \land \word (t) }{\vlhy{}}

%%		}{

%%		\vlin{\lefrul{\land}}{}{\word (t)  \land \word (t) , \Gamma \seqar \Delta}{ \vlhy{\word (t)  ,\word (t) , \Gamma \seqar \Delta} }

%%		}

%%	}

%%\end{equation}

%

%%

%%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

Safe compositions are essentially handled by many cut steps, using $\alpha$ and $\beta$ like derivations again and, crucially, left-contractions on both $!\word$ and $\word $ formulae.\footnote{In the latter case, strictly speaking, we mean cuts against $\wordcntr$.} The initial functions are routine.

%We also give the case of the conditional initial function $C (; x, y_\epsilon , y_0, y_1)$, to exemplify the use of additives. 

%%The conditional is defined equationally as:

%%\[

%%\begin{array}{rcl}