%\documentclass[a4paper]{article}
\documentclass[a4paper,UKenglish]{lipics-v2016}
%This is a template for producing LIPIcs articles. 
%See lipics-manual.pdf for further information.
%for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
%for british hyphenation rules use option "UKenglish", for american hyphenation rules use option "USenglish"
% for section-numbered lemmas etc., use "numberwithinsect"
 
\usepackage{microtype}%if unwanted, comment out or use option "draft"

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

\bibliographystyle{plainurl}% the recommended bibstyle




\usepackage[lutzsyntax]{virginialake}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{times}
%\usepackage{sans}
\usepackage{cmll}
\usepackage{bm}



%\newtheorem{theorem}{Theorem}    %% 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)}


\begin{document}

% Author macros::begin %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{Free-cut elimination in linear logic and an application to a feasible arithmetic\footnote{
This work was supported by by the ANR Project ELICA ANR-14-CE25-0005 and by the LABEX MILYON (ANR-10-LABX-0070) of Universit\'e de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-
0007) operated by the French National Research Agency (ANR).}
}
%\titlerunning{A Sample LIPIcs Article} %optional, in case that the title is too long; the running title should fit into the top page column

%% Please provide for each author the \author and \affil macro, even when authors have the same affiliation, i.e. for each author there needs to be the  \author and \affil macros
\author{Patrick Baillot}
\author{Anupam Das}
\affil{Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP
%	\\
%	\texttt{open@dummyuniversity.org}
	}
%\affil[1]{Dummy University Computing Laboratory, Address/City, Country\\
%  \texttt{open@dummyuniversity.org}}
%\affil[2]{Department of Informatics, Dummy College, Address/City, Country\\
%  \texttt{access@dummycollege.org}}
\authorrunning{P.\ Baillot and A.\ Das} %mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et. al.'

\Copyright{Patrick Baillot and Anupam Das}%mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/

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

%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\EventEditors{John Q. Open and Joan R. Acces}
%\EventNoEds{2}
%\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
%\EventShortTitle{CVIT 2016}
%\EventAcronym{CVIT}
%\EventYear{2016}
%\EventDate{December 24--27, 2016}
%\EventLocation{Little Whinging, United Kingdom}
%\EventLogo{}
%\SeriesVolume{42}
%\ArticleNo{23}
% Editor-only macros::end %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\maketitle

\begin{abstract}
We prove a general form of `free-cut elimination' for first-order theories in linear logic, yielding normal forms of proofs where cuts are anchored to nonlogical steps. To demonstrate the usefulness of this result, we consider a version of arithmetic in linear logic, based on a previous axiomatisation by Bellantoni and Hofmann. We prove a witnessing theorem for a fragment of this arithmetic via the `witness function method', showing that the provably convergent functions are precisely the polynomial-time functions. The programs extracted are implemented in the framework of `safe' recursive functions, due to Bellantoni and Cook, where the ! modality of linear logic corresponds to normal inputs of a safe recursive program. 
%We conclude with some comments for further applications of the free-cut elimination result. 
 \end{abstract}



\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}
%%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{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}) & \\
	%									\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}
	\]
	where $\type(A)  = (\vec u ; \vec x)$,  $\type(B)=(\vec v ;  \vec y)$  and $\star \in \{ \lor , \land, \laor, \laand \}$.
	%	where $\nu$ designates that the inputs are normal.
\end{definition}


%		\anupam{need to account for normality and safety somewhere. Attempting inlined and leaving types without this decoration.}
%		
%		\begin{remark}
%			[Distribution of $!$]
%			There is a potential issue that the $!$ contains $\lor$ symbols in its scope, whence we do not in general have $!(A \lor B) \cong !A \lor !B$. However this will not be a problem here by inspection of a convergence statement: there are no $\lor$ symbols in the scope of a $!$. Therefore, after free-cut elimination, no formula in the proof will have this property either.
%			
%			On the other hand, since we are working in affine logic, we do in general have $!(A \land B) \cong !A \land !B$.
%		\end{remark}

For a sorted tuple $(u_1 , \dots u_m ; x_1 , \dots ,x_n )$ we write $|(\vec u ; \vec x)|$ to denote its length, i.e.\ $m+n$. This sorted tuple corresponds to input variables, normal and safe respectively.
%		\footnote{It becomes important here that we are considering proofs of a convergence statement, since a free-cut free $\arith$-proof of a convergence statement cannot contain any $\lor$ symbols in the scope of a $!$. This could cause an issue in the above definition since we do not in general have the equivalence $!(A \lor B) \equiv !A \lor !B$. On the other hand, the equivalence $!(A\land B) \equiv !A \land !B$ follows since we are in the affine setting.}


Let us fix a particular (coherent) equational specification $\eqspec(f)$. Rather than directly considering $\arith$-proofs of $\conv ( f , \eqspec )$, we will consider a $\closure{\eqspec} \cup \arith $ sequent proof of $!\word (\vec x) \seqar \word (f (\vec x) )$, under Lemma~\ref{lemma:spec-norm-form}. 
%		
Free-cut elimination crucially yields strong regularity properties for proofs:

\begin{proposition}
	[Freedom]
	\label{prop:freedom}
	A free-cut free $\closure{\eqspec} \cup \arith $ sequent proof of $!\word (\vec x) \seqar \word (f (\vec x) )$ is:
	\begin{enumerate}
		\item\label{item:no-neg-word} Free of any negative occurrences of $\word$.
		\item\label{item:no-forall} Free of any $\forall$ symbols.
		\item\label{item:no-quest} Free of any $?$ symbols.
		\item\label{item:no-laor-step} Free of any $\laor$ or $\laand$ steps.\footnote{Because of the $\surj$ rule, the proof may still contain $\laor$ symbols, but these must be direct ancestors of some cut-step by free-cut freeness.}
	\end{enumerate}
\end{proposition}


For this reason we can assume that $\type$ is well-defined for all formulae occurring in a free-cut free proof of convergence, and so we can proceed with the translation from proofs to BC programs.

\begin{definition}
	[Translation]
	\label{dfn:translation-of-proofs}
	We give a translation from a free-cut free $\closure{\eqspec} \cup \arith $ proof $\pi$, satisfying properties \ref{item:no-neg-word}, \ref{item:no-forall}, \ref{item:no-quest}, \ref{item:no-laor-step} of Prop.~\ref{prop:freedom} above, of a sequent $\Gamma \seqar \Delta$ to BC programs for a tuple of functions $\vec f^\pi$ with arguments $\type \left(\bigotimes\Gamma\right)$ such that $|\vec f^\pi | = | \type\left(\bigparr\Delta\right)|$.
	
	
	The translation is by induction on the structure of $\pi$, so we proceed by inspection of its final step.
	
	If $\pi$ is an instance of the initial rules $\geneps, \sepeps^0 , \sepeps^1, \sepzer, \sepone$ or $\inj$ then $\vec f^\pi$ is simply the constant function $\epsilon$ (possibly with dummy inputs as required by $\type$).
	%			\footnote{This is because proofs of (in)equalities can be seen to carry no computational content.}
	If $\pi$ is an $\closure{\eqspec}$ or $=$ initial step it is also translated simply to $\epsilon$.
	%			
	The initial steps $\genzer, \genone , \surj$ and $\wordcntr$ are translated to $\succ_0( ; x) , \succ_1 (; x), ( \epsilon , \pred ( ;x) , \pred (; x) )$ and $(\id (;x) , \id(;x))$ respectively.
	%		
	Finally, suppose $\pi$ is a logical initial step. If $\pi $ is an instance of $\id$, i.e.\ $p \seqar p$, then we translate it to $\id$. Notice that, if $\pi$ is an instance of $\lefrul{\bot}$ (i.e.\ $p, p^\bot \seqar $ ) or $\rigrul{\bot}$ (i.e.\ $\seqar p, p^\bot$) then $p$ must be an equality $s=t$ for some terms $s,t$, since $p$ must be atomic and, by assumption, $\word$ does not occur negatively. Therefore $\pi$ is translated to tuples of $\epsilon$ as appropriate.
	
	
	
	
	Now we consider the inductive cases.
	%	
	%		We will continue with similar notational conventions in the remainder of this argument.
	%		
	%		%	\anupam{bad notation since need to include free variables of sequent too. (also of theory.) Reconsider.}
	%		
	If $\pi$ ends with a $\rigrul{\land}$ or $\lefrul{\lor}$ step then we just rearrange the tuple of functions obtained from the inductive hypothesis.
	%		The case when $\pi$ ends with a $\lefrul{\lor}$ step is analogous to the $\rigrul{\land}$ case above.		
	If $\pi$ consists of a subproof $\pi'$ ending with a $\lefrul{\land}$ or $\rigrul{\lor}$-step, then $\vec f^\pi$ is exactly $\vec f^{\pi'}$.
	By assumption, there are no $\laor$, $\laand$, $?$ or $\forall$ steps occurring in $\pi$, and if $\pi$ consists of a subproof $\pi'$ followed by a $\lefrul{\exists}$ step then $\vec f^\pi$ is exactly the same as $\vec f^{\pi'}$, under possible reordering of the tuple.
	
	Suppose $\pi$ consists of a subproof $\pi'$ followed by a $\rigrul{\exists}$ step,
	\[
	\vlderivation{
		\vlin{\rigrul{\exists}}{}{ \Gamma, \word(t) \seqar \Delta , \exists x^\word . A(x) }{
			%						\vltr{\pi'}{ \Gamma \seqar \Delta , A(t) }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
			\vlhy{ \Gamma \seqar \Delta , A(t) }
		}
	}
	\]
	so by the inductive hypothesis we have functions $\vec f^\Delta , \vec f^{A(t)}$ with arguments $(\vec u ; \vec x )= \type(\bigotimes \Gamma)$. We define 
	%				$\vec f^\pi$ as follows:
	%				\[
	$
	\vec f^\pi (\vec u ; \vec x , y)
	%				\quad := \quad
	$ as $
	\left( 
	\vec f^\Delta (\vec u ; \vec x) ,
	{\id (;y)},
	\vec f^{A(t)} (\vec u; \vec x)  
	\right)
	$.				
	%\]
	%		(The identity function on $y$ is defined from successor, predecessor and safe composition).
	
	
	%Suppose we have functions $\vec f^X (\vec x ; \vec y)$ from $\pi'$ for $X = \Delta$ or $ X=A$. 
	%\[
	%\vec f(\vec x ; \vec y , z) \quad := \quad ( \vec f^\Delta (\vec x ; \vec y)   ,  z , \vec f^A ( \vec x ; \vec y ) )
	%\]
	
	
	
	%
	%Suppose we have functions $\vec f' (\vec u , \vec v ; x , \vec y , \vec z)$ from $\pi'$ with $(\vec u ; \vec x )$ corresponding to $\Gamma$, $(;x)$ corresponding to $N(a)$ and $(\vec v ; \vec z)$ corresponding to $A(a)$. We define:
	%\[
	%\vec f ( \vec u , \vec v ;  )
	%\]
	
	%				\anupam{should just be same? Consider variable naming, just in case.}
	%				\anupam{This is probably where the consideration for free variables is.}
	
	%Suppose we have functions $\vec g (\vec v  , \vec w ; \vec x , y , \vec z)$ where $(\vec v ; \vec x) $ corresponds to $\Gamma$, $y$ corresponds to $\word(a)$ and $(\vec w ; \vec z) $ corresponds to $A(a)$. Then we define:
	%\[
	%\vec f ( \vec v , \vec w ; \vec x , y , \vec z )
	%\]
	
	
	
	%	\[
	%	\vlderivation{
	%	\vliin{\rigrul{\laand}}{}{\Gamma \seqar \Delta, A \laand B}{
	%	\vltr{\pi_1}{  \Gamma \seqar \Delta, A}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
	%	}{
	%	\vltr{\pi_2}{  \Gamma \seqar \Delta, B}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
	%	}
	%	}
	%	\]
	%	
	%	Suppose we have $\vec f^i (\vec x , \vec a ; \vec y , \vec b)$ from $\pi_i$.
	%	
	%	\anupam{problem: does this require many tests, just like for contraction? Can we isolate a different complexity class? e.g.\ PH or Grzegorzyck?}
	%	\anupam{skip this case and consider later.}
	
	%		\anupam{commented stuff on additives. To remark later perhaps.}
	
	
	If $\pi$ consists of a subproof $\pi'$ followed by a $\rigrul{!}$ step then $\vec f^\pi$ is exactly the same as $\vec f^{\pi'}$. If $\pi$ ends with a $\lefrul{!}$ step then we just appeal to Prop.~\ref{prop:bc-properties} to turn a safe input into a normal input.		
	
	Since there are no $?$ symbols in $\pi$, we can assume also that there are no $\rigrul{\cntr}$ steps in $\pi$.\footnote{Again, this is crucially important, since we cannot test the equality between arbitrary terms in the presence of nonlogical function symbols.}
	
	%		\anupam{This is important, so expand on this here or in a remark before/after.}
	
	If $\pi$ ends with a $\lefrul{\cntr}$ step then we duplicate some normal inputs of the functions obtained by the inductive hypothesis.			
	
	%		(Notice that this is obtainable in BC by a trivial instance of safe composition.)
	
	
	%	cntr right
	%	\[
	%	\vlderivation{
	%	\vlin{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, ?A}{
	%	\vltr{\pi'}{  \Gamma \seqar \Delta, ?A, ?A}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
	%	}
	%	}
	%	\]
	%	(need test function against witness predicate?)
	%	
	%	\anupam{problem: how to test even equality of two terms? Maybe treat $?$ as $!$ on left?}
	%	
	%	\anupam{Not a problem by free-cut elimination! Can assume there are no $?$ in the proof! Is this equivalent to treaing $?$ as $!$ on left?}
	%	
	%	\anupam{Yes I think so. We can work in a left-sided calculus. only problem is for induction. But this can never be a problem for modalities since induction formulae are modality-free.}
	%	
	%	\anupam{this is actually the main point.}
	
	
	If $\pi$ ends with a $\cut$ step whose cut-formula is free of modalities, then it can be directly translated to a safe composition of functions obtained by the inductive hypothesis, by relying on Prop.~\ref{prop:bc-properties}. Otherwise, the cut-formula must be of the form $!\word (t)$ since it must directly descend from the left-hand side of an induction step, by free-cut freeness.
	%	 or axiom on one side. The only such occurrence of a modality is in the conclusion of an induction step, whence such a formula has the form $!\word (t)$. 
	Since the cut is anchored, we can also assume that the cut formula is principal on the other side, i.e.\ $\pi$ ends as follows:	
	%	\anupam{need to check this assumption against free-cut elimination conditions. To discuss.}
	\[
	\vlderivation{
		\vliin{\cut}{}{!\Gamma , \Sigma  \seqar \Delta }{
			\vlin{\rigrul{!}}{}{!\Gamma \seqar  !\word(t)}{
				%			\vltr{\pi_1'}{!\Gamma \seqar  \word(t)}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
				\vlhy{!\Gamma \seqar  \word(t)}
			}
		}{
		%		\vltr{\pi_2}{ !\word(t), \Sigma\seqar \Delta}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
		\vlhy{ !\word(t), \Sigma\seqar \Delta}
	}
}
\]
where 
% $\pi_2$ ends with a $\ind$ step for which  $A(x)$ is the induction formula, and 
we assume there are no side-formulae on the right of the end-sequent of the left subproof for the same reason as $\rigrul{\cntr}$: $\pi$ does not contain any occurrences of $?$. By the inductive hypothesis we have functions $ g( \vec u ; )$ and $\vec h (  v , \vec w ; \vec x)$ where $\vec u$, $ v$ and $(\vec w ; \vec x)$ correspond to $!\Gamma$,  $!\word(t)$ and $\Sigma$ respectively. We construct the functions $\vec f^\pi $ as follows:
\[
\vec f^\pi (\vec u , \vec w ; \vec x)
\quad := \quad
\vec h (   g(\vec u ; ), \vec w  ; \vec x)
\]
Notice, again, that all safe inputs on the left occur hereditarily safe on the right, and so these expressions are definable in BC by Prop.~\ref{prop:bc-properties}.



%	Suppose $\pi$ ends with a $\lefrul{!}$ step:
%	\[
%	\vlderivation{
%		\vlin{!}{}{\Gamma, !A \seqar \Delta}{
%			\vltr{\pi'}{ \Gamma , A \seqar \Delta  }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
%		}
%	}
%	\]
%	\todo{finish this case, just passing a safe input to a normal input.}
%	
%	
%	Suppose $\pi$ ends with a $\rigrul{!}$ step:
%	
%	\todo{finish this case, should not change function at all, but maybe there is a consideration.}

If $\pi$ ends with a $\rigrul{\wk}$ step then we just add a tuple of constant functions $\vec \epsilon$ of appropriate length as dummy functions. If $\pi$ ends with a $\lefrul{\wk}$ step then we just add dummy inputs of appropriate length.

%	Suppose $\pi$ ends with a $\lefrul{\wk}$ step:
%	
%	\todo{finish this case, just add a dummy input.}
%	
%	Suppose $\pi$ ends with a $\rigrul{\wk}$ step:
%	
%	\todo{finish this case, just add a dummy function.}
%	


Finally, suppose $\pi$ ends with a $\ind$ step. Since there are no occurrences of $?$ in $\pi$ we can again assume that there are no side formulae on the right of any induction step. Thus $\pi$ ends as follows:
\[
\vlderivation{
	\vliin{\ind}{}{ !\word (t), !\Gamma  ,  A(\epsilon) \seqar A(t) }{
		%			\vltr{\pi_0}{!\word(a) , !\Gamma ,  A(a) \seqar A(\succ_0 a)}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
		\vlhy{!\word(a) , !\Gamma ,  A(a) \seqar A(\succ_0 a)}
	}{
	%		\vltr{\pi_1}{!\word(a), !\Gamma ,  A(a)\seqar A(\succ_1 a) }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
	\vlhy{!\word(a), !\Gamma ,  A(a)\seqar A(\succ_1 a)}
}
}
\]
%\anupam{is this better with a premiss for the base case?}

By the inductive hypothesis we have functions $\vec g^0 (u , \vec v ; \vec x)$ and $\vec g^1 (u , \vec v ; \vec x)$ with $u$, $\vec v$ and $\vec x$ corresponding to $!\word(a)$, $!\Gamma$ and $A(a)$ respectively. We define $\vec f^\pi$ by simultaneous predicative recursion on notation as follows:
\[
\begin{array}{rcll}
\vec f^\pi ( \epsilon, \vec v ; \vec x ) & := & \vec x & \\
\vec f^\pi ( \succ_i u , \vec v ; \vec x) & := & \vec g^i ( u, \vec v ; \vec f^\pi ( u, \vec v ; \vec x ) )
\end{array}
%\vec f^\pi ( \epsilon, \vec v ; \vec x ) := \vec x  \qquad
%\vec f^\pi ( \succ_i u , \vec v ; \vec x) :=  \vec g^i ( u, \vec v ; \vec f^\pi ( u, \vec v ; \vec x ) )
\]

%\anupam{check this}
%
%\todo{simultaneous PRN.}


\end{definition}

The induction step above is the reason why we enrich the usual BC framework with a simultaneous version of PRN.

\newcommand{\qfindth}{\mathit{IQF}}

\subsection{Witness predicate and extensional equivalence of functions}

%\anupam{need to mention that this predicate is similar to realisability predicate in absence, and indeed is presented like that for applicative theories, which also rely on free-cut elimination.}

Now that we have seen how to extract BC functions from proofs, we show that these functions satisfy the appropriate semantic properties, namely the equational program $\eqspec$ we started with. For this we turn to a quantifier-free \emph{classical} theory, in a similar fashion to $\mathit{PV}$ for $S^1_2$ in \cite{Buss86book} or system $T$ in G\"odel's Dialectica interpretation. This is adequate since we only care about extensional properties of extracted functions at this stage.

We could equally use a realisability approach, as done in e.g.\ \cite{Cantini02} and other works in applicative theories: since the formulae we deal with are essentially positive there is not much difference between the two approaches. Indeed here the witness predicate plays the same role as the realisability predicate in other works.
%, the complexity properties already handled by the BC programs we just constructed.



%The witness predicate of the WFM is similar to the realisability predicate, and this is even more true in out setting

Let $\qfindth$ be the classical theory over the language $\{ \epsilon, \succ_0, \succ_1 , (f^k_i )\}$ obtained from the axioms $\sepeps, \sepzer, \sepone, \inj, \surj$ and $\ind$ by dropping all relativisations to $\word$ (or $!\word$), replacing all linear connectives by their classical counterparts, and restricting induction to only quantifier-free formulae.

%For this we work in a quantifier-free classical logic whose atoms are equations between terms of our arithmetic and whose (sound) rules are simply the axioms of our arithmetic.
%
%(This is similar to the role of PV in the witnessing argument for $S^1_2$ and system $T$ for witnessing $I\Sigma_1$.)


%	\todo{add cases for $\laor$ and $\neq$.}

\newcommand{\witness}[2]{\mathit{Wit}^{#1}_{#2}}
\begin{definition}
	[Witness predicate]
	\label{dfn:wit-pred}
	For formulae $A, B$ of $\arith$ satisfying properties \ref{item:no-neg-word}, \ref{item:no-forall}, \ref{item:no-quest} of Prop.~\ref{prop:freedom}, we define the following `witness' predicate as a quantifier-free formula of $\qfindth$:
	%			 $A$ with free variables amongst $\vec a$:
	
	\renewcommand{\sigma}{a}
	\[
	%			\begin{array}{rcll}
	%			\witness{}{A} (\sigma) & := & \sigma = t & \text{if $A$ is $\word (t)$.} \\
	%			\witness{}{A} (\sigma) & := & s=t & \text{if $A$ is $s=t$.} \\
	%						\witness{}{A} (\sigma) & := & s\neq t & \text{if $A$ is $s\neq t$.} \\
	%			\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A) \cor \witness{}{B} (\vec \sigma^B) & 
	%						\text{for $\star \in \{ \lor,\laor\}$.} 
	%			\\
	%			\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A ) \cand \witness{}{B} (\vec \sigma^B ) & 
	%						\text{for $\star \in \{ \land, \laand \}$.} 
	%			\\
	%			\witness{}{\exists x^\word A} ( \sigma, \vec \sigma^A  ) & := & \witness{}{A}(\vec \sigma^A , \sigma ) & \\
	%			\witness{}{!A} (\vec \sigma^A) & := & \witness{}{A} (\vec \sigma^A)
	%			\end{array}
	\begin{array}{rcl}
	\witness{}{\word (t)} (\sigma) & := & \sigma = t 
	%			\text{if $A$ is $\word (t)$.} 
	\\
	\witness{}{s=t} (\sigma) & := & s=t 
	%			\text{if $A$ is $s=t$.} 
	\\
	\witness{}{s \neq t} (\sigma) & := & s\neq t 
	%			\text{if $A$ is $s\neq t$.} 
	\\
	%			\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A) \cor \witness{}{B} (\vec \sigma^B) & 
	%			\text{for $\star \in \{ \lor,\laor\}$.} 
	%			\\
	%			\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A ) \cand \witness{}{B} (\vec \sigma^B ) & 
	%			\text{for $\star \in \{ \land, \laand \}$.} 
	%			\\
	%			\witness{}{\exists x^\word A} ( \sigma, \vec \sigma^A  ) & := & \witness{}{A}(\vec \sigma^A , \sigma ) & \\
	\witness{}{!A} (\vec \sigma^A) & := & \witness{}{A} (\vec \sigma^A)
	\end{array}
	\quad
	\begin{array}{rcl}
	%						\witness{}{\word (t)} (\sigma) & := & \sigma = t & \text{if $A$ is $\word (t)$.} \\
	%						\witness{}{s=t} (\sigma) & := & s=t & \text{if $A$ is $s=t$.} \\
	%						\witness{}{s \neq t} (\sigma) & := & s\neq t & 
	%						\text{if $A$ is $s\neq t$.} 
	%						\\
	\witness{}{A \bullet B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A) \cor \witness{}{B} (\vec \sigma^B) 
	%						\text{for $\star \in \{ \lor,\laor\}$.} 
	\\
	\witness{}{A \circ B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A ) \cand \witness{}{B} (\vec \sigma^B )  
	%						\text{for $\star \in \{ \land, \laand \}$.} 
	\\
	\witness{}{\exists x^\word A} ( \sigma, \vec \sigma^A  ) & := & \witness{}{A}(\vec \sigma^A , \sigma ) 
	%						 \\
	%						\witness{}{!A} (\vec \sigma^A) & := & \witness{}{A} (\vec \sigma^A)
	\end{array}
	%						\begin{array}{rcl}
	%%						\witness{}{\word (t)} (\sigma) & := & \sigma = t & \text{if $A$ is $\word (t)$.} \\
	%%						\witness{}{s=t} (\sigma) & := & s=t & \text{if $A$ is $s=t$.} \\
	%%						\witness{}{s \neq t} (\sigma) & := & s\neq t & \text{if $A$ is $s\neq t$.} \\
	%%						\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A) \cor \witness{}{B} (\vec \sigma^B) & 
	%%						\text{for $\star \in \{ \lor,\laor\}$.} 
	%%						\\
	%%						\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A ) \cand \witness{}{B} (\vec \sigma^B ) & 
	%%						\text{for $\star \in \{ \land, \laand \}$.} 
	%%						\\
	%						\witness{}{\exists x^\word A} ( \sigma, \vec \sigma^A  ) & := & \witness{}{A}(\vec \sigma^A , \sigma )  \\
	%						\witness{}{!A} (\vec \sigma^A) & := & \witness{}{A} (\vec \sigma^A)
	%						\end{array}			
	\]
	where $\bullet \in \{ \lor, \laor \}$, $\circ \in \{ \land,\laand \}$, $|\vec \sigma^A| = |\type (A)|$ and $|\vec \sigma^B| = |\type (B)| $.
\end{definition}
%	\todo{problem: what about complexity of checking equality? }

%		\begin{remark}
Notice that, unlike in the bounded arithmetic setting where the $\word$ predicate is redundant (since variables are tacitly assumed to range over $\word$), we do not parametrise the witness predicate by an assignment to the free variables of a formula. Instead these dependencies are taken care of by the explicit occurrences of the $\word$ predicate in $\arith$.
%		\end{remark}

%		\todo{Reformulate above later if necessary.}

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

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

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

%		\anupam{to consider/remark: formally, is witness predicate checked in model or some logical theory?}




\begin{lemma}
	\label{lemma:witness-invariant}
	Let $\pi$ be a free-cut free proof in $\closure{\eqspec}\cup \arith$, satisfying properties \ref{item:no-neg-word}, \ref{item:no-forall}, \ref{item:no-quest}, \ref{item:no-laor-step} of Prop.~\ref{prop:freedom}, of a sequent $\Gamma \seqar \Delta $. Let $\eqspec^\pi$ denote the BC program for $\vec f^\pi$.\footnote{We assume that the function symbols occurring in $\eqspec^\pi$ are distinct from those occurring in $\eqspec$.} Then $\qfindth$ proves:
	\[
	\left(\forall \eqspec \cand \forall \eqspec^\pi \cand \witness{}{\bigotimes \Gamma} (\vec a)\right) \cimp \witness{}{\bigparr \Delta } (\vec f^\pi(\vec a))
	\]
	where $\forall \eqspec$ and $\forall \eqspec^\pi$ denote the universal closures of $\eqspec$ and $\eqspec^\pi$ respectively.
	%Suppose $\pi$ is a free-cut free $\Sigma^\nat_1$-$\pind$ proof of a sequent $\Gamma (\vec a) \seqar \Delta (\vec a)$, with $\vec f^\pi$ defined as above. Then:
	%	\[
	%			\witness{\vec a}{\bigotimes \Gamma} (\vec w , \vec b) \implies \witness{\vec a}{\bigparr \Delta } (\vec f^\pi(\vec w , \vec b), \vec b)
	%			\]
\end{lemma}


%			\anupam{to consider: do we need parameters $\vec a$ in argument of $f$? Or does $\nat$ predicate take care of this?}
%			
%			%	We will be explicit about normal and safe inputs when necessary, for the most part we will simply rearrange inputs into lists $(\vec u; \vec a)$ as in BC framework.
%			
%%			We often suppress the parameters $\vec a$ when it is not important.	
%			
%			\anupam{Is this implication provable in Bellantoni's version of PV based on BC?}

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


\begin{proof}[Proof sketch]
	By structural induction on $\pi$, again, following the definition of $\vec f^\pi$.\footnote{Notice that, since we are in a classical theory, the proof of the above lemma can be carried out in an arbitrary model, by the completeness theorem, greatly easing the exposition.}
\end{proof}	


Finally, we arrive at our main result, providing a converse to Thm.~\ref{thm:arith-proves-bc-conv}.

\begin{theorem}
	\label{thm:main-result}
	For any coherent equational specification $\eqspec$, if $\arith $ proves $\conv (f , \eqspec)$ then there is a polynomial-time function $g $ on $\Word$ (of same arity as $f$) satisfying $\eqspec [  g/ f ]$.
	
	%		If we can prove a convergence statement for a function $f$ under a specification $\Phi(f)$ then there is a BC-program for a function $\mathbf f$ such that:
	%		\begin{equation}
	%		\label{eqn:spec-implies-program}
	%\Phi(f) \implies f (\vec x) = \mathbf{f} (\vec x)
	%		\end{equation}
	%		\begin{equation}
	%		\label{eqn:program-satisfies-spec}
	%		\Phi(\mathbf f)
	%		\end{equation}
\end{theorem}
\begin{proof}
	[Proof sketch]
	%		By Thm.~\ref{thm:free-cut-elim} and Lemma~\ref{lemma:spec-norm-form} we have a free-cut free proof $\pi$ in $\closure{\eqspec} \cup \arith$ of $!\word (\vec x ) \seqar \word (f (\vec x))$. By Lemma~\ref{lemma:witness-invariant} above this means that $\vec a = \vec x \cimp f^\pi (\vec a) = f(\vec x)$ is true in any model of $\qfindth$ satisfying $\eqspec$ and $\eqspec^\pi$. 
	%%		Since some model must exist by coherence (cf.\ Prop.~\ref{prop:eq-spec-model}), we have that 
	%		Using the fact that $\eqspec \cup \eqspec^\pi$ is coherent we can construct such a model, similarly to Prop.~\ref{prop:eq-spec-model}, which will contain $\Word$ as an initial segment, in which we must have $f^\pi (\vec x) = f (\vec x)$ for every $\vec x \in \Word$, as required.\todo{polish}
	Follows from Lemmas~\ref{lemma:spec-norm-form} and \ref{lemma:witness-invariant}, Dfn.~\ref{dfn:wit-pred} and coherence of $\eqspec$, cf.~\ref{prop:eq-spec-model}.
\end{proof}

%			\begin{proof}
%			Notice that a convergence statement has the following form:
%			\[
%			!\Phi(f) , !\nat(\vec a) \seqar \nat(f (\vec a) )
%			\]
%			By the lemma above, and by inspection of the definition of the witness predicate, this means we have that,
%			\[
%			(\Phi(f) \cand \vec x = \vec a ) \implies \mathbf f (\vec x) = f(\vec a)
%			\]
%			whence we arrive at \eqref{eqn:spec-implies-program}.
%			
%			Finally, notice that $\Phi(f)$ has \emph{some} model, since it is a monotone inductive definition so some fixed point must exist. Therefore we obtain \eqref{eqn:program-satisfies-spec} as well.
%			\end{proof}
%			
%			\anupam{rephrase above proof to make more sense.}
%			
%%
%\newcommand{\concat}{\mathit{concat}}
%\paragraph{Some points on concatenation \anupam{if necessary}}
%We can define the concatenation operation by PRN:
%\[
%\begin{array}{rcl}
%\concat (\epsilon ; y) & : = & x \\
%\concat (\succ_i x ; y) & := & \succ_i \concat (x ; y)
%\end{array}
%\]
%
%From here we can define iterated concatenation:
%\[
%\concat (x_1 , \dots x_n ; y) \quad := \quad \concat (x_n ; \concat (x_{n-1} ; \vldots \concat (x_1 ; y) \vldots ) )
%\]
%
%(notice all safe inputs are hereditarily to the right of $;$ so this is definable by safe composition and projection.)




\section{Conclusions}
\label{sect:conclusions}

As mentioned in the introduction, our motivation for this work is to commence a proof-theoretic study of first-order theories in linear logic, in particular from the point of view of complexity.
To this end we proved a general form of `free-cut elimination' that generalises forms occurring in prior works, e.g.\ \cite{LincolnMSS92}. We adapted an arithmetic of Bellantoni and Hofmann in \cite{BelHof:02} to the linear logic setting, and used the free-cut elimination result, via the witness function method \cite{Buss86book}, to prove that a fragment of this arithmetic characterises $\FP$.

%. Our starting point was an axiomatisation proposed by Bellantoni and Hofmann in \cite{BelHof:02}, adapted to the linear logic setting. We identified a fragment, $\arith$, of the arithmetic that is sound and complete with respect to polynomial-time functions, using the free-cut elimination theorem and witness function method that is common in bounded arithmetic and applicative theories.

% To see if analogues of various results can be useful for the construction of theories corresponding to various complexity classes. In particular we are interested in the following conventions:




%An alternative to \ref{item:crit-implicit-complexity} is the use of, say, bounded quantifiers, as done in bounded arithmetic \cite{Buss86book}.
%
%Regarding \ref{item:crit-ground-type}, almost all approaches 

%\subsection{Related work}
From the point of view of constructing theories for complexity classes, the choice of linear logic and witness function method satisfies two particular desiderata:

\begin{enumerate}
	\item\label{item:crit-implicit-complexity} Complexity is controlled by `implicit' means, not explicit bounds.
	%, e.g.\ modalities or ramification, as in \cite{Leivant94:found-delin-ptime}. 
	\item\label{item:crit-ground-type} Extraction of programs relies on functions of only ground type.
\end{enumerate}

From this point of view, a relevant related work is that of Cantini \cite{Cantini02}, based on an \emph{applicative theory}, which we recently became aware of. The main difference here is the choice of model of computation: Cantini uses terms of combinatory logic, whereas we use equational specifications (ESs). 
As we have mentioned, this choice necessitates a different proof-theoretic treatment, in particular since equality between terms is not decidable in the ES framework, hindering any constructive interpretation of the right-contraction rule. This is why Bellantoni and Hofmann require a double-negation translation into intuitionistic logic and the use of functionals at higher types, and why Leivant disregards classical logic altogether in \cite{Leivant94:found-delin-ptime}. Notice that this is precisely why our use of linear logic is important: the control of $?$ occurrences in a proof allows us to sidestep this problem. At the same time we are able to remain in a classical linear setting. We do not think that either model of computation is better, but rather that it is interesting to observe how such a choice affects the proof-theoretic considerations at hand.

%Our use of linear logic can, in some sense, be seen as a refinement of Leivant's result in \cite{Leivant94:found-delin-ptime}, where positive existential comprehension in intuitionistic second-order logic is found to correspond to polynomial time. The necessity of intuitionistic logic is since any double-negation translation from classical logic would break the positivity criterion. In this work we have observed that the further restriction to non-modal formulae in nonlogical rules is sufficient to carry out a witnessing argument directly from a classical setting, while remaining complete for polynomial-time functions. \todo{comprehension vs induction. Check this is not bullshit!}
%\patrick{hmm, I am not sure I understand how our use of linear logic can be viewed as a refinement of this work.}



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 \emph{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 the propositional fragment of the 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.
The status of first-order theories is more developed for other substructural logics, for instance \emph{relevant logic} \cite{FriedmanM92}, although we do not know of any works connecting such logics to computational complexity.

%Most works on the relationships between linear logic and complexity concern the construction of \emph{type systems}, e.g.\ bounded linear logic \cite{GirardSS92:bounded-ll}, light linear logic and elementary linear logic \cite{Girard94:lll}, soft linear logic \cite{Lafont04}. However, Terui considers a na\"ive set theory \cite{Terui04} that is also sound and complete for polynomial time and is based on light linear logic. His approach relies on functionals at higher type, using light linear logic to type the extracted functionals.\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 axiom. 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.} The status of first-order theories is more developed for other substructural logics, for instance \emph{relevant logic} [cite?], although we do not know of any works connecting such logics to computational complexity.

Concerning the relationship between linear logic and safe recursion, we 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 nonlinear treatment of safe arguments which here we manage by including in our theory an explicit contraction axiom for $W$. 

We have already mentioned the work of Bellantoni and Hofmann \cite{BelHof:02}, which was somewhat the inspiration behind this work. Our logical setting is very similar to theirs, under a certain identification of symbols, but there is a curious disconnect in our use of the additive disjunction for the $\surj$ axiom. They rely on just one variant of disjunction. As we said, they rely on a double-negation translation and thus functionals at higher-type.


%\anupam{mention bounded arithmetic?}
%
%Finally, the approach of bounded arithmetic 
%
%In summary, as far we
%
%
%******
%
%
%
%As far as we know no approach to  has combined a basis in linear (or a related) logic with a solely proof theoretic witnessing argument, such as the witness function method. 
%
%
%
%         
%In summary, it is promising that free-cut elimination and the witness function method can be used to extract similar complexity results to those obtained in bounded arithmetic. 



%\subsection{Further work}
%\todo{finish!}

%
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 witness function method 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, e.g.\ the polynomial hierarchy, might be easier to obtain.
%
%Say something about minimisation and the polynomial hierarchy. Could be achieved by controlling contraction/additives, since this requires a notion of tests.
%
%As we mentioned in the context section, there are many choices of model of computation when constructing theories. Applicative theories use combinatory algebra and in this work we have used equational specifications. Theories of bounded arithmetic, however, use arithmetic formulae to code computation sequences. The advantage of this is that any closed formula can be evaluated, and so equality is decidable. 
%
%We think the true power of the witness function method lies in an approach such as this, although we 
%
%

The problem of right-contraction seems to also present in work by Leivant \cite{Leivant94:found-delin-ptime}, which uses equational specifications, where the restriction to positive comprehension to characterise polynomial-time only goes through in an intuitionistic setting. It would be interesting to see if a linear logic refinement could reproduce that result in the classical setting, as we did here.
%
%Polynomial hierarchy? Cite Reinhard/Isobel and their cited works.
%
%\newpage
%
%
%
%
%
%
%
%
%
%
%*******************************************
%\todo{words or integers?}
%% % % % % % % % % % Bullet points % % % % % % %
%
%Some points, either here or in body of paper:
%
%\begin{itemize}
%\item Application of free-cut elimination to witnessing arguments: proof of concept.
%\item Examine differences between our arithmetic and Bellantoni and Hofmann: (a) our induction rule, is it equivalent? Maybe not. (b) point about their surjectivity axiom: we do not think it works unless they add another axiom, like Leivant's, for the completeness in the conditional case. We can remark that linear logic solves this problem neatly by use of the additives.
%\item Point about contraction on right: this is what free-cut elimination + linear logic adequately restricts. This is a problem for any classical theory that uses equational specifications.
%\item Regarding Leivant's intrinsic theories: his result about polynomial-time functions being exactly the provably convergent functions of positive existential induction is necessarily in intuitionistic logic. In classical logic he cannot avoid contraction on the right without the linear logic refinement that we have. \anupam{This can be seen as another contribution of our work?}
%\item On the other hand, our completeness argument can be seen as more-or-less what he had in mind, refined to linear logic.
%\item Discuss different approaches to arithmetics for complexity/witnessing. Namely:
%\begin{itemize}
%\item Programs: terms of combinatory logic vs. formulae of arithmetic vs. equational specifications.
%\item Convergence: N predicate vs. $\Pi^0_2$ sentence.
%\end{itemize}
%Remark: use of equational specifications necessitates N predicate. Hence contraction problems present, no problem for first two types of programs since there is a notion of execution (either via a well-typing or by seeing formula as a circuit), and so closed programs can be run and we can conduct equality tests for right-contraction steps.
%
%Remark: another variant in the equational specifications category is when equations are given on lambda-terms, e.g. as in
%
%Marc Lasson. Controlling Program Extraction in Light Logics. TLCA 2011: 123-137
%
%\item We should mention future line of work in bounded-arithmetic style, i.e. using formulas as programs.
%\patrick{In particular mention that we conjecture that in this setting induction on Sigma1 formulas (not only positive) would be Ptime sound, if I understand well?}
%
%\item Related works:
%\begin{itemize}
% \item Discuss differences with line of work on Curry-Howard style implicit complexity, e.g. light linear logic. Mention work of Murawski to relate safe recursion
% and LLL:
% 
%Andrzej S. Murawski, C.-H. Luke Ong:
%On an interpretation of safe recursion in light affine logic. Theor. Comput. Sci. 318(1-2): 197-223 (2004)
%\item related works on free-cut elimination style results in LL (David Baelde?)
%\end{itemize}
%\end{itemize}
%
%\medskip
%
%A proposal of organization (Patrick):
%\begin{enumerate}
%\item Introduction:
%  \begin{itemize}
%        \item motivate and explain:
%                 \begin{itemize}
%                      \item free-cut elimination: mention use in bounded arithmetic
%                      \item linear logic: say mainly used for structural proof-theory, proofs-as-programs, proof search ?
%                      \item free cut-elimination for linear logic
%                  \end{itemize}  
%          \item application in this paper: arithmetic systems for Ptime computability
%                 \begin{itemize}
%                   \item present Bellantoni-Hofmann's system and Leivant's ramified theory $RT_0$
%                   \item explain their relationships with implicit computational complexity on the one hand, bounded arithmetic on the other. some words about witnessing method in bounded arithmetic
%                   \item describe our contribution: re-prove a weak version of Bellantoni-Hofmann, by using the witnessing method.
%                 \end{itemize}        
%   \end{itemize}
%\item Related works section (by the end?):
%        \begin{itemize}
%             \item about complexity:
%               \begin{itemize}
%                  \item overview of different approaches to arithmetics for complexity
%                  \item technical comparison of our contribution w.r.t. Bellantoni-Hofmann and w.r.t. Leivant
%                  \item short comparison with Murawski-Ong's study of safe recursion vs. LLL
%                 \end{itemize}
%             \item about linear logic:
%                \begin{itemize}
%                    \item if not done in the introduction, comparison with free-cut elimination like results by Baelde or others
%                \end{itemize}
%         \end{itemize}
%\item Conclusion and future work:
%
%mention something about prenexing if needed.
%
% future work on bounded arithmetic style
% \end{enumerate}
% \medskip
% 
% *************************************
%
%
%Comments:
%
%\vspace{2em}
%
%Related works section (by the end?):
%        \begin{itemize}
%             \item about complexity:
%               \begin{itemize}
%                  \item overview of different approaches to arithmetics for complexity
%                  \item technical comparison of our contribution w.r.t. Bellantoni-Hofmann and w.r.t. Leivant
%                  \item short comparison with Murawski-Ong's study of safe recursion vs. LLL
%                 \end{itemize}
%             \item about linear logic:
%                \begin{itemize}
%                    \item if not done in the introduction, comparison with free-cut elimination like results by Baelde or others
%                \end{itemize}
%         \end{itemize}
%         
%         
%         
%                 
%                  % % % % % % % % % % % % % % % % % % % % % % % %
%                  \subsubsection{Parameters}
%                  \begin{itemize}
%                  \item Programs. Equational specifications vs lambda terms vs formulae.
%                  \item Convergence statement. Designated predicate vs $\Pi^0_2$ formula.
%                  \item Source of complexity. Bounded quantifiers (induces Cobham limited recursive programs) vs modalities (induces ramified/safe recursive programs).
%                  \item Proof method. Realisability/Dialectica (higher types) vs Proof theoretic (ground type).
%                  \end{itemize}
%                  
%                  
%                  \subsubsection{Linear logic and complexity}
%                  \begin{itemize}
%                  \item Mostly type systems, e.g.\ bounded/light/soft/elementary linear logic. (Girard, Girard (?), Lafont, ? resp.)
%                  \item Girard/Terui/Grishin naive set theory. Uses realisability.
%                  
%                  
%                  \end{itemize}
%                  
%                  \subsubsection{Modal systems}
%                  Modal systems usually model the notion of ramification from Leivant's intrinsic theories.
%                  
%                  \subsection{Witnessing argument}
%                  Almost all works use a 
%                  
%                  refinement of Leivant 94.


\bibliographystyle{plain}
\bibliography{biblio}

%\newpage
%
%\input{appendix}

\end{document}