Whither relevant arithmetic?
Harvey M. Friedman, Robert K. Meyer · Journal of Symbolic Logic · 1992
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?