
Strenge Arithmetic
Robert K. Meyer and Greg Restall
[Robert.MeyerGreg.Restall]@anu.edu.au
Automated Reasoning Project
Australian National University act 0200
April 15, 1996
1 Arithmetics
Consider the traditional Peano axioms for arithmetic.
Identity = 8x8y(x = y ! y = x)
8x8y8z?y = z ! (x = y ! x = z)?
8x8y(x0 = y0 ! x = y)
Successor 8x8y(x = y ! x0 = y0)
8x(0 <> x0)
Addition 8x(x + = x)
8x8y?x + y0 = (x + y)0?
Multiplication 8x(x0 = 0)
8x8y(xy0 = xy + x)
Induction A(0); 8x?A(x) ! A(x0)? ` 8xA(x)
Under the standard interpretation of the language (in which quantifiers range
over natural numbers1) these axioms ring true. In fact, they ring true independently
of the theory of the conditional `!' is read. If ! is a merely material
conditional, then we have traditional Peano arithmetic. If ! is the conditional
of the relevant logic R, then we have relevant arithmetic, studied by the first
author [2, 3, 4]. If ! is the conditional of a contraction free logic, then we have
contraction free arithmetics, studied by the second author [5, 6]. So, for any
predicate logic X, we'll call X] the theory given by adding the axioms and rules
of X] to those of X.
G?odel has shown us that X] is not complete. One way to complete TV]
(where TV is classical two valued logic) is to add the ! rule.
A(0), A(00), A(000), : : : ` 8xA(x)
The arithmetic given by replacing the induction rule of X] by the ! rule is named X]].2 TV]] is complete. Here's why: One can prove by induction on the complexity of A that A is provable or ?A is provable. The crucial steps are the base case  that s = t is provable iff the terms s and t denote the same number, and s <> t is provable iff the terms denote a different number. The cases for conjunction, disjunction and negation are trivial. The ! rule means that we can show that if A(n) is provable for every n, then 8xA is provable. And similarly, if A(n) is not provable for every n, then ?A(n) is provable for some n, and hence ?8xA is probable. Hence we have completeness for all formulae.
So, if you think that TV is a good account of the logic of quantifiers and connectives, then you have reason to believe that TV]] is true arithmetic. It is a complete theory, giving you a definite answer for every arithmetic question.
1We don't worry about the difference between a number and its canonical name. 2It's simple to show that given the ! rule the induction rule follows.