A note on the strength of paraconsistent arithmetic

In several papers [6–8], Beall argues that, since we can add to non-classical (including paraconsistent) arithmetics rules that restore classicality, we can effectively recover classical arithmetical reasoning in non-classical systems. According to Halbach and Nicolai [18], however, the move to non-classical arithmetic comes at the expense of proof-theoretic strength, undermining Beall’s claims. Then how can paraconsistent arithmetics be said to recover classical strength? It is not sufficient to prove classical arithmetical consequences in a fragment of the language, as done e.g. by Friedman and Meyer [14], since this would yield strictly weaker theorems. In this paper, I provide a so-called classical recapture result for Zach Weber’s paraconsistent arithmetic $\textsf{subDLQ-A}$, based on the logic $\texttt{subDLQ}$ [43]. I reconstruct a notion of coding and recursion for this paraconsisent arithmetic, and show that the theory, if supplemented with additional forms of induction and classical axioms for identity, supports Gentzen’s classical lower bound proof for transfinite induction up to any ordinal less than $\varepsilon _{0}$.