\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 the \textit{witness function method} \cite{Buss86book}. 
  
   Linear logic \cite{Girard87} can be seen as a decomposition of both intuitionistic and classical logic, based on a thorough analysis of duplication and erasure of formulas in proofs (i.e.\ the structural rules), and has been particularly useful in proofs-as-programs correspondences, proof search \cite{Andreoli92} and logic programming \cite{Miller04}. By controlling  structural rules with designated modalities, the \textit{exponentials}, linear logic has allowed for a fine study of complexity bounds in the Curry-Howard interpretation, leading to variants with polynomial-time complexity \cite{GirardSS92:bounded-ll} \cite{Girard98} \cite{Lafont04}. 
%   However most of this work has been done for 'purely logical' linear logic, or at least for variants with full cut elimination procedure. 
   
    In this work we explore how the finer granularity of linear logic can be used to control complexity in \emph{first-order theories}, restricting the provably convergent functions rather than the typable terms as in the propositional setting.
%     aim at exploring in which way the complementary techniques of free-cut elimination and linear logic can be combined to analyze properties of first-order theories in which structural rules play a critical r\^ole. 
    We believe this to be of general interest, and in particular to understand the effect of substructural restrictions on nonlogical rules, e.g.\ induction, in mathematical theories. Some related works exist, in particular the na\"ive set theories of Girard and Terui \cite{Girard94:lll} \cite{Terui04}, but overall it seems that the first-order proof theory of linear logic is still rather undeveloped; in particular, to our knowledge, there seems to be no general form of free-cut elimination available in the literature (although special cases occur in \cite{LincolnMSS92} and \cite{Baelde12}). Thus our first contribution, in Sect.~\ref{sect:free-cut-elim}, will be to provide general sufficient conditions on nonlogical axioms and rules for a first-order linear logic system to admit free-cut elimination.
    
    \newcommand{\FP}{\mathbf{FP}}
    
    We illustrate the usefulness of such a result by proving a witnessing theorem for a fragment of arithmetic in linear logic, showing that the provably convergent functions are precisely the polynomial-time computable functions (Sects.~\ref{sect:bc-convergence} and \ref{sect:wfm}), henceforth denoted $\FP$. Our starting point is an axiomatisation based on a modal logic due to Bellantoni and Hofmann \cite{BelHof:02}, called $\mathcal{A}_2^1$, already known to characterise $\FP$.
%    In this system ,following Leivant \cite{Leivant94:intrinsic-theories} functions are defined by first-order equational specifications. 
%    The main result of $\mathcal{A}_2^1$ is then that the provably total functions are exactly the polynomial time class. 
    This approach, and that of \cite{Leivant94:found-delin-ptime} before, differs from the bounded arithmetic approach in that it does not employ bounds on quantifiers, but rather restricts nonlogical rules by substructural features of the modality \cite{BelHof:02} or by a \emph{ramification} of formulas  \cite{Leivant94:intrinsic-theories}. The proof technique employed in both cases is a realisability argument, for which \cite{Leivant94:found-delin-ptime} operates directly in intuitionistic logic, whereas \cite{BelHof:02} obtains a result for a classical logic via a double-negation translation, relying on a higher-type generalisation of \emph{safe recursion}
%     which is applied to an intuitionistic version of the theory. In  \cite{BelHof:02} the target language of the realizability argument is a higher-order language \cite{Hofmann00}, SLR, based on safe recursion 
     \cite{BellantoniCook92}. 
%     In a second step the result is extended to the classical variant $\mathcal{A}_2^1$ by using the Friedman A translation.
    
    We show that Buss' witness function method can be employed to extract functions directly for classical systems similar to $\mathcal{A}_2^1$ based in linear logic, by taking advantage of free-cut elimination. The De Morgan normal form available in classical (linear) logic means that the functions we extract remain at ground type, based on the usual safe recursive programs of \cite{BelHof:02}. A similar proof method was used by Cantini in \cite{Cantini02}, who uses combinatory terms as the model of computation as opposed to the equational specifications in this work.\footnote{This turns out to be important due to the handling of right-contraction steps in the witnessing argument.}
   
   Our result holds for an apparently weaker theory than $\mathcal{A}_2^1$, with induction restricted to positive existential formulas in a way similar to Leivant's $\mathit{RT}_0$ system in \cite{Leivant94:intrinsic-theories}, 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. 

A version of this article with full proofs is available at \cite{BaiDas}.
   

