Whither relevant arithmetic?

Abstract

Based on the relevant logic R, the system R^# was proposed as a relevant Peano arithmetic. R^# has many nice properties: the most conspicuous theorems of classical Peano arithmetic PA are readily provable therein; it is readily and effectively shown to be nontrivial; it incorporates both intuitionist and classical proof methods. But it is shown here that R^# is properly weaker than PA, in the sense that there is a strictly positive theorem QRF of PA which is unprovable in R^#. The reason is interesting: if PA is slightly weakened to a subtheory P⁺, it admits the complex ring C as a model; thus QRF is chosen to be a theorem of PA but false in C. Inasmuch as all strictly positive theorems of R^# are already theorems of P⁺, this nonconservativity result shows that QRF is also a nontheorem of R^#. As a consequence, Ackermann's rule γ is inadmissible in R^#. Accordingly, an extension of R^# which retains its good features is desired. The system R^##, got by adding an omega-rule, is such an extension. Central question: is there an effectively axiomatizable system intermediate between R^# and R^#, which does formalize arithmetic on relevant principles, but also admits γ in a natural way?