Underlying numerical reasoning is the formal theory of arithmetic, and if the reasoning is to be carried out in a nonclassical logic then this will be a correspondingly nonclassical arithmetic. The relevant arithmetic R ♯ was proposed around 50 years ago and is one of the few theories based on substructural logic to have been investigated in much detail. This paper surveys some old results concerning R ♯ and recent attempts to extend it to deal with the rational numbers as well as the naturals. While the formal results here are not new, it is worthwhile to put them together and to present the topic as one of interest for contemporary research into nonclassical reasoning.
In almost every domain of genuine importance, reasoning needs to encompass not only pure logic but also numerical inferences. From the number of timesteps in a computation to the cost of an action or the state of a stockpile, quantitative as well as qualitative reasoning is everywhere in practice. At the root of such reasoning is elementary arithmetic-primitively, as a theory about natural numbers, extending to integers and to rational number theory, and eventually to analysis.
Arithmetic has of course been studied intensively as part of mathematical logic in the classical and constructivist traditions. In the history of more radically nonclassical logics, however, the literature on arithmetic is relatively sparse. This is unfortunate, as the question of which numerical inferences are available, and with what kind of logical guarantee, is sensitive to the choice of logic and is therefore of importance in the nonclassical setting. The purpose of the present paper is to note some results, ancient and modern, concerning theories of arithmetic in substructural logics.
One of the few such theories to have been seriously investigated is the arithmetic R ♯ , put forward by R.K. Meyer in the 1970s. R ♯ has the proper axioms of Peano arithmetic, but the underlying logic is the relevant logic R rather than classical logic.
The propositional logic R and its first order extension RQ are usually specified by means of a Hilbert system. The language has the unary connective ¬, binary connectives ∧ and → , and quantifiers ∀x. It is usual to define
The pure implication ( → ) fragment of R extends that of linear logic by the addition of contraction:
ARQNL 2024: Automated Reasoning in Quantified Non-Classical Logics, 1 July 2024, Nancy, France john.slaney@anu.edu.au (J. Slaney) Negation is rather classical, like the "strong negation" in logics of constructible falsity:
Conjunction and disjunction are additive (extensional) connectives satisfying the postulates:
Quantifiers are added by means of very standard axioms, of which r14 is the only postulate of the positive logic which is not intuitionistically valid:
The constructive form of quantifier confinement ∀x(A → B) → (A → ∀xB) (x not free in A)
is derivable using r12 and r15. We note this now, as it will be needed later. For accounts of R, including its semantics and proof theory, see the original presentation by Anderson and Belnap [1], and Mares [2] for instance. R ♯ is a theory in an arithmetical vocabulary with one constant, 0 (zero), the unary operator ′ (successor) and binary operators + and • (addition and multiplication). Its axioms are the universal closures of:
The theorems of R ♯ are the RQ consequences of the axioms-note that a10 is an axiom scheme with infinitely many instances. Briefly, the arithmetic has most of the properties one would expect of a version of Peano arithmetic, including closure under universal generalisation and a fully classical equality relation satisfying all instances of the scheme
Meyer's early work on R ♯ , unpublished in his lifetime, appeared in 2021 [3] prompting a renewal of interest in the topic. While establishing that R ♯ has many classically familiar features, he observed that it has some decidedly unclassical ones too. Most notably, it has finite models! What, for example, if 0 is equal to 5? Classically, the answer is simple: 0 is not 5 and there is no more to say. Relevantly, the answer is more nuanced: if 0 = 5 then numerical equality is indistinguishable from congruence modulo 5. That supposition is inconsistent, of course, but R is a paraconsistent logic and allows models of such inconsistent thoughts to exist.
Even the logic RM3, a very strong 3-valued extension of R which is almost classical, allows this (Figure 1). There are only 5 numbers in the domain. Addition and multiplication are interpreted modulo 5, and the successor of 4 is 0 (despite axiom a5 which says it isn't). There are three possible truth values for propositions: T and F are what you expect, while t is a weak kind of truth which is a fixed point for negation. An equation a = b has the value t if a and b are the same object and the value F if they are different. All theorems of R ♯ all get values T or t on this interpretation-never the value F . Clearly, the construction can be repeated for any modulus, providing a purely finitary proof (Gödel notwithstanding) that R ♯ is reliable in that no false equations are provable in it.
R ♯ permits easy proofs, by induction on z, of:
Note that while the first of these is an equivalence, the second holds in one direction only. In fact, the above theorems together with the models in the integers modulo n suffice for the observation that for any numerals a, b, c and d, the equation a = b relevantly implies c = d according to R ♯ iff |a − b| divides |c − d|. As special cases, 0 = 1 implies all equations, while every equation implies 0 = 0, because 1 divides everything while everything divides 0. Since 0 = 0 provably implies all and only the theorems of R ♯ , we may abbreviate it to 't' and its negation 0 ̸ = 0 to 'f '. The monotonicity of multiplication, as recorded in the theorem noted above, depends crucially on the contraction axiom r4. If that axiom is dropped from the logic, giving a system with the same intensional fragment as linear logic, many of the implications between equations are lost. Slaney, Meyer and Restall [4] showed that in arithmetic based on relevant logics without contraction, a = b implies c = d if and only if |a − b| = |c − d|. In particular, in such arithmetics, no false equation ever implies a true one.
R ♯ indeed provides an interesting view of arithmetical reasoning, but as a theory in the relevant logical tradition it faces some formidable difficulties. Two of these in particular stand out. Firstly, the theory is sadly incomplete, not just because of Gödel's theorems, which apply to every arithmetic, and not just because it was always supposed to be agnostic concerning some intensional formulae (involving the ' → ' connective), but because it misses some of the purely extensional arithmetical facts from the corresponding classical Peano arithmetic. Secondly, R ♯ is a theory of natural numbers only; unlike its classical counterpart, it cannot easily be embedded in a wider mathematical account of number theory. We consider each of these issues in turn.
The theorems of classical Peano arithmetic PA are, by definition, the consequences of the axioms a1 -a10 and suitable axioms for Boolean first order logic by closure under the rule of material detachment. By playing a little with De Morgan's laws and double negation, we may take material detachment in the form of the "disjunctive syllogism" or the rule γ:
This is famously not a derivable rule of R, but for the logic R and also for RQ it is admissible in that there is no counter-example to it: no case in which its premises are theorems while its conclusion is not. This accords well with the world view associated with R on which truth-functional logic is right about truth-functional matters, but stands in need of a better theory of implication and a more sophisticated account of inference. The classical rule γ preserves truth in the intended models of R, but does not preserve satisfacton at arbitrary worlds in those models. Now the axioms of classical logic and of Peano arithmetic are all theorems of R ♯ , so if R ♯ is closed under γ then it exactly agrees with classical PA in its classical (arrow-free) vocabulary. While γ is not a derivable rule of R ♯ , the closely related rule
is easily seen to be derivable, so clearly any formula A in the → -free vocabulary is a theorem of PA iff A ∨ f is a theorem of R ♯ . This embedding of classical arithmetic into R ♯ is enough to secure many results, such as Gödel's theorems, but it falls short of what the R enthusiast would really want. At the time of writing his exposition [3], Meyer expressed the hope that γ would prove to be admissible for R ♯ just as it is for RQ and for R ♯♯ , the exension of R ♯ resulting by closing under the ω rule (if ⊢ A [x←n] for every numeral n then ⊢ ∀xA).
That hope, however, was vain. Friedman and Meyer [5] showed that there are theorems of PA which contain only the positive connectives ∧ and ∨ and quantifiers, but which cannot be proved without using axiom a5. Such formulae likewise have no purely positive (negation-free) proofs in R ♯ ; but R ♯ is a conservative extension of its positive fragment, so there are theorems of PA which are not theorems of R ♯ , and consequently γ fails.
The failure of γ was disappointing for the early proponents of relevant arithmetic, but we could perhaps learn to live with that. There is, however, a more serious issue which is potentially devastating for the entire program. A theory of arithmetic cannot merely be an account of natural numbers (or integers). If it is to be proposed seriously for use in mathematics, it must extend at least to the rational numbers.
Here we consider the non-negative rationals, as the extension to deal with negative ones goes along with the extension from natural numbers to integers, which complicates the theory slightly but not in a fundamental way.
Any extension of a natural number theory to a theory of rational arithmetic is subject to at least three obvious desiderata. A theory of the numbers should be: a) mathematically reasonable-for instance, it should contain all true ground equations, and allow ordinary reasoning steps such as paramodulation (replacement of equals), appeals to the transitivity of equality and the like; b) related to natural number theory at least in that for any natural numbers a, b, c, d (b, d > 0) it should be provable that a b = c d is equivalent to ad = bc; c) a conservative extension of the theory of naturals.
Unfortunately, every extension of R ♯ from natural to rational number theory violates at least one of these desiderata.
The proof of this is very simple: by condition (a) 4 6 is provably equal to 2 3 , and so by either transitivity or replacement it is a theorem that 4 6 = 1 1 implies 2 3 = 1 1 ; but by condion (b) this means that 4 = 6 implies 2 = 3, which is not a theorem of R ♯ because of the models in the integers modulo 2. Any finite model with greater modulus will give rise in this way to similar counter-examples to intuitively well-motivated principles, so in the presence of (a) and (b), desideratum (c) cannot be met.
Leaving aside for the moment the failure of γ, we may note some possible solutions to the problem of extension to rational number theory. One bold solution to the trilemma is to hold onto R ♯ just as it is, to introduce rational number theory by means of contextual definitions, so that the relationship between it and natural number theory is as close as it could be, and simply to let the theorems fall where they will. That is, we regard a term like a b + c d as nothing more than syntactic sugar for the expression ad+bc bd in which the addition function is applied only to naturals. Similarly, when we write a b × c d we really mean ac bd and an equation of the form a b = c d is nothing but another way of saying ac = bd, which is a formula in the primitive language of R ♯ and makes no reference to anything beyond natural numbers. There is a little more to be done, to avoid terms like a 0 , but this can be managed. On this account, rational number theory is by definition part of natural number theory, so desiderata (b) and (c) are met. Desideratum (a) however is comprehensively violated. Any model of R ♯ is a model of rational number theory on this account. That includes the finite models, in which rational equality as just defined looks nothing like an identity relation. It is not even transitive, and does not support the most basic paramodulation inferences. Hence, although R ♯ as a rational arithmetic is an interesting theory, it is hardly convincing as a basis for numerical reasoning.
The alternative to giving up desideratum (a) is, of course, to give up desideratum (b). This might be done in many ways, as there is no unique RQ theory lacking a particular equivalence. The most promising line seems to be to take as axioms the analogues of a1 and a2 for rational equations, together with the postulate ac ′ b ′ c ′ = a b ′ (avoiding division by zero by requiring b and c to be successors) and the monotonicity postulate a = b → a c ′ = b c ′ but not its converse. The effect is that we secure half of desideratum (b), allowing the relevant inference from ad ′ = b ′ c to the rational equation a b ′ = c d ′ , but not the converse except as an admissible rule. This asymmetry is in harmony with the overall style of R ♯ , whereby multiplication is monotonic but not cancellative. This version of relevant arithmetic is another theory worthy of investigation, as it promises a workable account in keeping with the view of numbers embodied in R ♯ .
The finite models in the integers modulo n are still there, of course, and still give us non-trivial information about the natural numbers, but they say nothing about rationals because in those models all rational numbers collapse to a single point. This is easy to see: if 0 = n then n n = 0 n which is to say the rational 1 is the same as the rational 0. But where q is any rational, q • 1 = q while q • 0 = 0, so all rationals are equal to the rational zero and so equal to each other.
The final option is to abandon the goal of staying within R ♯ , and instead to strengthen natural number theory to the point that the three listed desiderata for rational arithmetic can all be satisfied together. The arithmetic R ♮ [6] adds to R ♯ an axiom a11 0 = x ′ → 0 = 1 Since the equation 0 = 1 implies all other equations in R ♯ , this is equivalent to the principle that every incorrect equation implies that all numbers are equal. It is also equivalent to adding cancellation in the form
and in the presence of desideratum (b) above, to transitivity in the form
Hence R ♮ is the minimum supertheory of R ♯ capable of extension to rational arithmetic without violating desiderata (a) and (b).
Of course, the finite models are no longer available, with the sole exception of the most extreme, in which there is only one number. In this model, zero is a fixed point for all arithmetical functions, and the propositional structure is 4-valued (Figure 2). All equations take the value t, which counts as true, so this structure-the only finite model of R ♮ -cannot be used to show reliability in the way this could be done for R ♯ . However, it does show some formulae, such as 0 ̸ = 0 → 2 + 2 = 4 to be non-theorems, so there is still a finitary proof of non-triviality.
The move from R ♯ to R ♮ does more than create a workable theory of rational arithmetic. It also restores the desired relationship between the relevant and classical theories of the naturals. Recall that since classical Peano arithmetic is obtainable from the fragment of R ♯ in the classical (arrow-free) vocabulary by closing under the rule γ or material detachment. The classical fragment of R ♮ therefore coincides with classical arithmetic if it is γ-closed. For the whole of R ♮ , the admissibility of γ is an open question, but the special case for formulae in the classical vocabulary does hold, and this is enough to secure all of the classical theorems.
The first lemma towards this result is due to Dunn, Meyer and Leblanc [7] and is one of the earliest important results on quantified relevant logic. By an RQ theory, we mean a set of formulae closed under adjunction and RQ-provable implication. A theory is prime if it never contains a disjunction unless it contains one of the disjuncts, regular if it contains all theorems of RQ, and rich if every universal ∀xA is in the theory if every ground instance A [x←t] is. Lemma 1. Let θ be a regular RQ theory and B / ∈ θ. Then there is a prime, rich theory θ ′ such that θ ⊆ θ ′ and B / ∈ θ ′ . For proof see the original paper [7]. As a consequence: Lemma 2. Let θ ′ be as above and let A be a ground formula. Then the principal θ ′ -theory of A (i.e.
Lemma 2 is easily proved using lemma 1 and the confinement law
Remember that x is not free in A. Lemma 3. Every quantifier-free ground formula in the extensional vocabulary is equivalent in R ♮ to one of the following 6:
Proof: as in classical Peano arithmetic, every ground equation is provably equivalent either to 0 = 0 or to 0 = 1, and clearly the set of 6 is closed (up to provable equivalence) under the extensional connectives ∧ , ∨ and ¬. Lemma 4. Let θ be a regular, prime, rich RQ theory. Then every ground formula in the extensional vocabulary is θ-equivalent to one of the above 6 formulae.
Proof is by induction on the structure of formulae. All cases are trivial except for those of ∀xA and ∃xA where A is an extensional formula with one free variable x. For the case ∀xA, note that every ground instance of A is equivalent to one of the Extensional Six, so choose one ground instance from each equivalence class and let C be their conjunction. Obviously ∀xA implies C, and C θ-implies every ground instance of A. By lemma 2, therefore, C θ-implies ∀xA, so ∀xA and C are equivalent according to θ. The case ∃xA is immediate from this and the negation case, by quantifier duality.
Theorem. The rule γ is admissible in R ♮ for formulae in the extensional vocabulary.
Proof: Suppose for contradiction that A and B are extensional formulae such that A ∨ B and ¬A are theorems of R ♮ but B is not. By lemma 1, there is a prime, rich supertheory θ of R ♮ which also excludes B. Inside θ is its extensional fragment-the set of extensional formulae in θ-and by lemma 3, this is easily seen to have a model in a homomorphic image of DM6 (figure 3), so B also has a counter-model in DM6. DM6 may be embedded in a prime, consistent algebraic model (a De Morgan monoid [8]) modelling the whole of R ♮ . This model of R ♮ is prime and satisfies A ∨ B, so either it satisfies both A and ¬A or else it satisfies B, contrary to the fact that it is consistent and the supposition that B fails in it.
Such is the state of research in relevant Peano arithmetic. When R ♯ was first proposed in 1974, it was discovered almost immediately that the theory has unintended models including finite ones. At the time, these were certainly startling, but were they a blessing or a curse? The main blessing flowing from them is the finitary proof of reliability. While there can be no finitary proof of freedom from contradiction, it can be shown, by methods representable inside the system, that no derivations exist proving a term to have two different values. Note also that since every relevant proof is also a classical proof, the classical arithmetician can have this same guarantee as long as no irrelevant moves were made during a proof.
To pursue this last point a little further, if γ were to hold for R ♯ , this would show that the whole of classical Peano arithmetic could be derived from its axioms by means incapable of proving an incorrect result for any calculation. Since this would immediately show classical arithmetic to be consistent, it follows that there is no finitary proof of admissibility for γ. In fact, as Meyer and Friedman [5] showed, there is no proof of γ at all, so the point is moot, but it is known [9] that R ♯♯ , the result of extending R ♯ with the ω rule, is closed under γ and still has the finite models. The ω rule is unusable in general, but at least any classical proof using only inferences valid in R ♯♯ enjoys the finitary proof of reliability.
Peano arithmetic does not stand alone, but is essentially a part of number theory, which includes reasoning about rational as well as natural numbers. On stepping up from R ♯ to a theory encompassing rational arithmetic, we must decide how to treat the finite models. There is no unique way to do this-no one approach representing the relevant logical account of rational numbers. One idea is to keep R ♯ itself as the whole theory, defining the operations on fractions and the equations between them as mere abbreviations for the equivalent expressions concerning natural numbers. On such an account, the finite models remain as they always were. Rational number theory is not expected to make sense on its own over such structures, and indeed it does not, with its non-transitive equality relation and failures of substitutivity, but it is still what it is as part of natural number arithmetic and it remains coherent in those terms when the definitions are unpacked. A different approach is to loosen the ties between natural and rational equations, axiomatising the latter so as to ensure transitivity and the like. Now the integers modulo n still provide inconsistent but non-trivial models, but in them there is no interesting rational arithmetic because there is only one rational number (though n different natural ones). The third option is to keep the equivalence between natural and rational equations, and to secure mathematical respectability for the whole theory by strengthening the underlying Peano postulates, taking us from R ♯ to R ♮ . On this account, the finite models are indeed a curse: they show that R ♯ is too weak, so they are banished. The axiom saying that zero is not a successor does not succeed in a paraconsistent logic like R, because nothing prevents zero from being a successor anyway. R ♮ imposes a penalty for violations of the axiom, and this restores mathematical respectability, removes the unwanted models and, as noted, captures the whole of classical number theory as intended.
Important open questions and future work include:
• Is the rule γ admissible in R ♮ ?
• How, if at all, can we make sense of rational number theory as a defined fragment of R ♯ ?
• What is the best way to axiomatise rational arithmetic as a conservative extension of R ♯ with a transitivity postulate for rational equality? • Still weaker logics bring their own perspectives to quantitative inference. Without contraction, for instance, there are models in which numerical equality not even a congruence on the rational field. What else is there to discover by weakening the logical base still further?