Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic.

We prove a general form of u0027free-cut eliminationu0027 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 u0027witness function methodu0027, showing that the provably convergent functions are precisely the polynomial-time functions. The programs extracted are implemented in the framework of u0027safeu0027 recursive functions, due to Bellantoni and Cook, where the ! modality of linear logic corresponds to normal inputs of a safe recursive program.