Relevant number theory with cancellation

The arithmetic R is obtained by postulating standard axioms for Peano arithmetic on a basis of the relevant logic R rather than classical logic. It is known that there is no way to extend R from a theory of natural numbers to one of rational numbers meeting “obvious” desiderata. In this paper, we consider one way of obtaining a relevant number theory more congenial to rational arithmetic, by strengthening the postulate “zero is not a successor”, adding that if it is a successor then 0 = 1. We call the resulting theory R. Many properties of R carry over to R. For instance, there is still a finitary proof of absolute consistency, and there are still infinite propositional structures interpreting the relevant implication connective even though the models of equations are simplified down to the classical (bivalent) ones. One important result concerning R that does not apply to R is the Friedman–Meyer proof of the non-admissibility of material detachment and consequent incompleteness for classical Peano arithmetic in the classical vocabulary. While it remains an open question whether material detachment is admissible, it does hold for formulae in the classical vocabulary, so all theorems of classical arithmetic are provable relevantly in R.