=Paper=
{{Paper
|id=Vol-3875/ARQNL2024_paper1
|storemode=property
|title=A Fresh Look at Relevant Number Theory
|pdfUrl=https://ceur-ws.org/Vol-3875/ARQNL2024_paper1.pdf
|volume=Vol-3875
|authors=John Slaney
|dblpUrl=https://dblp.org/rec/conf/arqnl/Slaney24
}}
==A Fresh Look at Relevant Number Theory==
https://ceur-ws.org/Vol-3875/ARQNL2024_paper1.pdf
A Fresh Look at Relevant Number Theory
John Slaney1
1
Australian National University, Canberra, ACT 2601, Australia
Abstract
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.
1. The logic RQ and R♯
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
A ∨ B = ¬(¬A ∧ ¬B)
A ↔ B = (A → B) ∧ (B → A)
A ∘ B = ¬(A → ¬B)
∃xA = ¬∀x¬A
The pure implication ( → ) fragment of R extends that of linear logic by the addition of contraction:
Axioms:
r1 A→A
r2 A → ((A → B) → B)
r3 (A → B) → ((C → A) → (C → B))
r4 (A → (A → B)) → (A → B)
Rule:
A → B, A =⇒ B
ARQNL 2024: Automated Reasoning in Quantified Non-Classical Logics, 1 July 2024, Nancy, France
$ john.slaney@anu.edu.au (J. Slaney)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
ceur-ws.org
ISSN 1613-0073 ARQNL 2024 6 P ROCEEDINGS
Proceedings
Negation is rather classical, like the “strong negation” in logics of constructible falsity:
Axioms:
r5 (A → ¬B) → (B → ¬A)
r6 ¬¬A → A
Conjunction and disjunction are additive (extensional) connectives satisfying the postulates:
Axioms:
r7 (A ∧ B) → A
r8 (A ∧ B) → B
r9 ((A → B) ∧ (A → C)) → (A → (B ∧ C))
r10 (A ∧ (B ∨ C)) → ((A ∧ B) ∨ C)
Rule:
A, B =⇒ A ∧ B
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:
Axioms:
r11 ∀xA → A[x←t] (t free for x in A)
r12 ∀x(A → B) → (∀xA → ∀xB)
r13 (∀xA ∧ ∀xB) → ∀x(A ∧ B)
r14 ∀x(A ∨ B) → (A ∨ ∀xB) (x not free in A)
r15 A → ∀xA (x not free in A)
r16 ∀xA (A an axiom)
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:
a1 x=x
a2 x = y → (x = z → y = z)
a3 x = y → x′ = y ′
a4 x′ = y ′ → x = y
a5 0 ̸= x′
a6 x+0=x
a7 x + y ′ = (x + y)′
a8 x·0=0
a9 x · y ′ = (x · y) + x
a10 (A[x←0] ∧ ∀x(A → A[x←x′ ] )) → A
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
7
tT → T t F = 0 1 2 3 4
T T F F 0 t F F F F
t t
t T t F 1 F t F F F
tF F T T T 2 F F t F F
3 F F F t F
4 F F F F t
Figure 1: Inconsistent model in the integers modulo 5
a = b → (A[x←a] → A[x←b] )
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:
x=y ↔ x+z =y+z
x = y → xz = yz
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.
2. Difficulties
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
8
classical counterpart, it cannot easily be embedded in a wider mathematical account of number theory.
We consider each of these issues in turn.
2.1. Problem: the classical sub-theory
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 γ:
A ∨ B, ¬A =⇒ B
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 γf
A ∨ B ∨ f, ¬A ∨ f =⇒ B ∨ f
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.
2.2. Problem: rational extension
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 al-
low 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 ab = dc is equivalent to ad = bc;
c) a conservative extension of the theory of naturals.
9
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) 46 is provably equal to 23 , and so by either transitivity
or replacement it is a theorem that 46 = 11 implies 23 = 11 ; 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.
3. Possible solutions within R♯
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 ab + dc 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 ab × dc we really
mean ac a c
bd and an equation of the form b = 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 a0 , 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 bac′ c′ = ba′ (avoiding division by zero by requiring b and c to be successors) and the
monotonicity postulate a = b → ca′ = cb′ 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 ba′ = dc′ , 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 nn = n0 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.
4. Extending R♯
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
10
tT → T f t F T : f ∘f
T T F F F
tf f: 0 ̸= 0
f T t F F
t t t T f t F t: 0=0
F T T T T F : f →t
tF
Figure 2: Arithmetic modulo 1
ax′ = bx′ → a = b
and in the presence of desideratum (b) above, to transitivity in the form
a c c e a e
b′ = d ′ → ( d ′ = f ′ → b ′ = f ′ )
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.
5. Classical arithmetic regained
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.
{C : A → C ∈ θ′ }) is rich.
Lemma 2 is easily proved using lemma 1 and the confinement law
∀x(A → C) → (A → ∀xC)
Remember that x is not free in A.
11
t⊤ ⊤: 0 ̸= 1
tα α: 0 = 0 ∨ 0 ̸= 0
❅
❅
❅t f t: 0=0
t t
❅ f: 0 ̸= 0
❅
❅t β
β: 0 = 0 ∧ 0 ̸= 0
t⊥
⊥: 0=1
Figure 3: The De Morgan lattice DM6
Lemma 3. Every quantifier-free ground formula in the extensional vocabulary is equivalent in R♮ to
one of the following 6:
0=0 0=1 0=0 ∧ 0=1
0 ̸= 0 0 ̸= 1 0=0 ∨ 0=1
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.
6. Summary
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
12
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?
References
[1] A. R. Anderson, N. D. Belnap, Entailmant: The Logic of Relevance and Necessity, Vol. 1, Princeton
University Press, Princeton, 1975.
[2] E. Mares, Relevant Logic: A Philosophical Interpretation, Cambridge University Press, Cambridge,
2004.
[3] R. K. Meyer, Arithmetic formulated relevantly, Australasian Journal of Logic 18 (2021) 154–288.
[4] J. Slaney, R. K. Meyer, G. Restall, Linear arithmetic desecsed, Logique et Analyse 39 (1998) 379–388.
[5] H. Friedman, R. K. Meyer, Whither relevant arithmetic, Journal of Symbolic Logic 57 (1992) 824–831.
[6] J. Slaney, Relevant number theory with cancellation, Journal of the IGPL (forthcoming).
[7] R. K. Meyer, J. M. Dunn, H. Leblanc, Completeness of relevant quantification theories, Notre Dame
Journal of Formal Logic 15 (1974) 97–121.
[8] T. Moraschini, J. Raftery, J. Wannenburg, Varieties of De Morgan monoids: Minimality and reducible
algebras, Journal of Pure and Applied Algebra 223 (2019) 2780–2803.
[9] R. K. Meyer, ⊃E is admissible in “true” Relevant arithmetic, Journal of Philosophical Logic 27 (1998)
327–351.
13