Towards feasibility in arithmetic via linear logic

In this work-in-progress we intend to extend the scope of linear logic to first-order theories, i.e. with nonlogical axioms and inference rules, in particular for fragments of arithmetic. The aim is to use the restrictions on contraction in substructural logics to model resource usage in an interpretation of first-order proofs, e.g. via realisability/Dialectica interpretations or via proof-theoretic means, such as the witness function method. At the same time, we would like to draw parallels between substructural approaches to implicit computational complexity and bounded arithmetic, by linking structural restrictions in the former to quantifier restrictions in the latter.