An Exploration of Contraction Free Arithmetic
Swapnil Ghosh

Abstract:
This thesis is a proof-theoretic study of Contraction Free Arithmetic (CFA). We introduce CFA as a first order arithmetical theory based on a logic (GQC) which is the multiplicative fragment of LK without the structural rules of contraction. Our investigation starts by showing some basic properties of GQC, before proceeding to establish various properties of CFA. One such interesting property of CFA is that the (omitted) additive connectives become definable in it. A key characteristic of CFA is that it has the Induction Rule, for all formulas, in place of the Induction Schema. We justify this by showing that the presence of the induction schema would reintroduce contraction rules, and subsequently, the arithmetic would collapse to PA. We proceed to establish that induction schema restricted to ∆0 formulas hold for CFA and utilize this to show, among other things, that any Π2 sentence provable in the arithmetical theory I∆0 is also provable in CFA. This thesis culminates in the study of the computational strength of CFA via provably recursive functions of CFA. We establish that the class of provably recursive functions within CFA precisely coincides with the class of primitive recursive functions. Consequently, the essential result of the present work is that CFA not only expands the class of provably recursive functions beyond those of I∆0 , but also establishes its distinctiveness from PA.