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

\item\label{item:crit-implicit-complexity} Complexity controlled by `implicit' means, not explicit bounds.

Most works on the relationships between linear logic and complexity fit in the approach of the proofs-as-programs correspondence and study variants of linear logic with weak exponential modalities \cite{GirardSS92:bounded-ll} \cite{Girard94:lll} \cite{Lafont04}. However, Terui considers a na\"ive set theory \cite{Terui04} that also characterises $\FP$ and is based on light linear logic.\footnote{He also presents a cut-elimination result but, interestingly, it is entirely complementary to that which we present here: he obtains full cut-elimination since he works in a system without full exponentials and with Comprehension as the only nonlogical rule. Since the latter admits a cut-reduction step, the former ensures that cut-elimination eventually terminates by a \emph{height-based} argument, contrary to our argument that analyses the \emph{degrees} of cut-formulae.} His approach relies on functionals at higher type, using light linear logic to type the extracted functionals. Another work using linear logic to characterize  complexity classes by using convergence proofs is \cite{Lasson11} but it is tailored for second-order logic.

Concerning the relationship between linear logic and safe recursion, note that an embedding of a variant of safe recursion into light linear logic has been carried studied in \cite{Murawski04}, but this is in the setting of functional computation and is quite different from the present approach. Observe however that a difficulty in this setting  was the non-linear treatment of safe arguments which here we manage by including in our theory a duplication axiom for $W$. 

In further work we would like to apply the free-cut elimination theorem to theories based on other models of computation, namely the formula model employed in bounded arithmetic \cite{Buss86book}. We believe that the WFM could be used at a much finer level in this setting,\footnote{One reason for this is that atomic formulae are decidable, and so we can have more freedom with the modalities in induction steps.} and extensions of the theory for other complexity classes, for instance the polynomial hierarchy, might be easier to obtain.

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

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

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

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

%%\end{array}

%%\]

%Let $\vec y = ( y_\epsilon , y_0, y_1 )$ and construct the required proof as follows:

%\[

%\small

%\vlderivation{

%\vliq{}{}{ \word (x) , \word (\vec y) \seqar \word ( C(; x ,\vec y) )}{

%\vliin{2\cdot \laor}{}{ x = \epsilon \laor \exists z^\word . x = \succ_0 z \laor \exists z^\word x = \succ_1 z , \word (\vec y) \seqar \word ( C(;x \vec y) ) }{

%\vliq{}{}{ x = \epsilon , \word (\vec y) \seqar \word ( C(; x , \vec y) ) }{

%\vliq{}{}{ \word (\vec y) \seqar \word ( C( ; \epsilon , \vec y ) ) }{

%\vlin{\wk}{}{ \word (\vec y) \seqar \word (y_\epsilon) }{ 

%\vlin{\id}{}{\word (y_\epsilon) \seqar \word ( y_\epsilon )}{\vlhy{}}

%}

%}

%}

%}{

%\vlhy{

%\left\{ 

%\vlderivation{

%\vlin{\lefrul{\exists}}{}{ \exists z^\word . x = \succ_i z , \word (\vec y) \seqar \word ( C(;x , \vec y) ) }{

%\vliq{}{}{ x = \succ_i a , \word (\vec y ) \seqar \word (C(; x ,\vec y)) }{

%\vliq{}{}{ \word (\vec y) \seqar \word ( C(; \succ_i a , \vec y ) ) }{

%\vlin{\wk}{}{ \word (\vec y) \seqar \word (y_i) }{

%\vlin{\id}{}{\word (y_i) \seqar \word (y_i)}{\vlhy{}}

%}

%}

%}

%}

%}

%\right\}_{i = 0,1}

%}

%}

%}

%}

%\]

%whence the result follows by $\forall$-introduction.

%%The other initial functions are routine.

\end{proof}

\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} can be seen as a decomposition of both intuitionistic and classical logic, based on a careful analysis of duplication and erasure of formulas in proofs (i.e.\ the structural rules), and has been particularly 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, leading to 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, and in particular to understand the effect of substructural restrictions on nonlogical rules, e.g.\ induction, in mathematical theories. Some related works exist, in particular 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}, will be to provide general sufficient conditions on nonlogical axioms and rules for a first-order linear logic system to admit free-cut elimination.

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

    We illustrate the usefulness of such a result by proving a witnessing theorem for a fragment of 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 based on a modal logic due to Bellantoni and Hofmann \cite{BelHof:02}, called $\mathcal{A}_2^1$, 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 in that it does not employ bounds on quantifiers, but rather restricts nonlogical rules by substructural features of the modality \cite{BelHof:02} or by a \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.}

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

There is an extended version \cite{BaiDas} of this paper with appendices containing further proof details.

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

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

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

\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{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{Witness function method}

\label{sect:wfm}

We now prove the converse to the last section: any provably convergent function in $\arith$ is polynomial-time computable,

%.

%To this end we use the \emph{witness function method} (WFM), a common technique in {bounded arithmetic} \cite{Buss86book}.

using the witness function method (WFM) \cite{Buss86book}.

The WFM differs from realisability and Dialectica style witnessing arguments mainly since it does not require functionals at higher type. Instead a translation is conducted directly from a proof in De Morgan normal form, i.e.\ with negation pushed to the atoms, relying on classical logic. 

%Free-cut elimination is employed to control the quantifer complexity of formulae occurring in a proof, although here we furthermore use it to control the presence of \emph{contraction} in a proof, to which we have access via the modalities of linear logic. This

%Free-cut elimination is employed to control the logical complexity of formulae occurring in a proof, and a formal `witness' predicate plays a similar role to the realisability predicate.

The combination of De Morgan normalisation and free-cut elimination plays a similar role to the double-negation translation, and this is even more evident in our setting where the transformation of a classical proof to free-cut free form can be seen to be a partial `constructivisation' of the proof. As well as eliminating the (nonconstructive) occurrences of the $\forall$-right rule, as usual for the WFM, the linear logic refinement of the logical connectives means that right-contraction steps are also eliminated. This is important due to the fact that we are in a setting where programs are equational specifications, not formulae (as in bounded arithmetic \cite{Buss86book}) or combinatory terms (as in applicative theories \cite{Cantini02}), so we cannot in general decide atomic formulae.

%Some key features of this method are the following:

%\begin{itemize}

%	\item T

%\end{itemize}

%

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

%

%\todo{compare with applicative theories}

%

%\anupam{in particular, need to point out that this argument is actually something in between, since usually the WFM requires programs to be defined by formulae, not equational specifications.}

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

\newcommand{\norm}{\nu}

\newcommand{\safe}{\sigma}

		\subsection{The translation}

We will associate to each (free-cut free) proof of a convergence statement in $\arith$ a function on $\Word$ defined by a BC program. In the next section we will show that this function satisfies the equational specification of the convergence statement.

%, hence showing that any provably convergent function of $\arith$ is polynomial-time computable.\footnote{Strictly speaking, we will also require the equational specification at hand to be coherent, cf.\ Prop.~\ref{prop:eq-spec-model}.}

		\begin{definition}

			[Typing]

			\label{dfn:typing}

			To each $(\forall, ?)$-free $\word^+$-formula $A$ we associate a sorted tuple of variables $\type (A)$, intended to range over $\Word$, as follows:

			\[

%			\begin{array}{rcll}

%			\type (\word (t)) & := & (;x^{\word (t)} ) & \\

%			\type(s = t) & := & ( ; x^{s = t}) & \\

%			\type (s \neq t) & := & ( ;x^{s\neq t} )\\

%%			\type (A \lor B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$ and $\type(B) = (\vec v ; \vec y)$.} \\

%			\type (A \star B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$, $\type(B) = (\vec v ; \vec y)$ and $\star \in \{ \lor, \land, \laor, \laand \}$.} \\

%			\type (! A) & : = & ( \vec u ,\vec x  ; ) & \text{if $\type(A) = (\vec u ; \vec x )$.} \\

%			\type (\exists x^\word . A) & := & (\vec u ; \vec x , y) & \text{if $\type (A) = (\vec u ; \vec x)$.}

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

%			\end{array}

%

			\begin{array}{rcll}

			\type (\word (t)) & := & (;x^{\word (t)} ) & \\

			\type(s = t) & := & ( ; x^{s = t}) & 

%			\\

%			\type (s \neq t) & := & ( ;x^{s\neq t} )\\

%%			\type (A \lor B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$ and $\type(B) = (\vec v ; \vec y)$.} \\

%			\type (A \star B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$, $\type(B) = (\vec v ; \vec y)$ and $\star \in \{ \lor, \land, \laor, \laand \}$.} \\

%			\type (! A) & : = & ( \vec u ,\vec x  ; ) & \text{if $\type(A) = (\vec u ; \vec x )$.} \\

%			\type (\exists x^\word . A) & := & (\vec u ; \vec x , y) & \text{if $\type (A) = (\vec u ; \vec x)$.}

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

			\end{array}

			\quad

						\begin{array}{rcll}

%						\type (\word (t)) & := & (;x^{\word (t)} ) & \\

%						\type(s = t) & := & ( ; x^{s = t}) & \\

						\type (s \neq t) & := & ( ;x^{s\neq t} )\\

			%			\type (A \lor B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$ and $\type(B) = (\vec v ; \vec y)$.} \\

%						\type (A \star B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$, $\type(B) = (\vec v ; \vec y)$ and $\star \in \{ \lor, \land, \laor, \laand \}$.} \\

						\type (! A) & : = & ( \vec u ,\vec x  ; ) & 

%						\text{if $\type(A) = (\vec u ; \vec x )$.} \\

%						\type (\exists x^\word . A) & := & (\vec u ; \vec x , y) & \text{if $\type (A) = (\vec u ; \vec x)$.}

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

						\end{array}

						\quad

									\begin{array}{rcll}

%									\type (\word (t)) & := & (;x^{\word (t)} ) & \\

%									\type(s = t) & := & ( ; x^{s = t}) & \\