Robinson arithmetic


In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic, first set out by R. M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is weaker than PA but it has the same language, and both theories are incomplete. Q is important and interesting because it is a finitely axiomatized fragment of PA that is recursively incompletable and essentially undecidable.

Axioms

The background logic of Q is first-order logic with identity, denoted by infix '='. The individuals, called natural numbers, are members of a set called N with a distinguished member 0, called zero. There are three operations over N:
The following axioms for Q are Q1–Q7 in Burgess . Variables not bound by an existential quantifier are bound by an implicit universal quantifier.
  1. Sx ≠ 0
  2. *0 is not the successor of any number.
  3. → x = y
  4. * If the successor of x is identical to the successor of y, then x and y are identical. and yield the minimum of facts about N and S needed for non-triviality. The converse of follows from the properties of identity.
  5. y=0 ∨ ∃x
  6. * Every number is either 0 or the successor of some number. The axiom schema of mathematical induction present in arithmetics stronger than Q turns this axiom into a theorem.
  7. x + 0 = x
  8. x + Sy = S
  9. * and are the recursive definition of addition.
  10. x·0 = 0
  11. x·Sy = + x
  12. * and are the recursive definition of multiplication.

    Variant axiomatizations

The axioms in Robinson are – in Mendelson. The first 6 of Robinson's 13 axioms are required only when, unlike here, the background logic does not include identity.
The usual strict total order on N, "less than", can be defined in terms of addition via the rule. Equivalently, we get a definitional conservative extension of Q by taking "<" as primitive and adding this rule as an eighth axiom; this system is termed "Robinson arithmetic R" in Boolos et al..
A different extension of Q, which we temporarily call Q+, is obtained if we take "<" as primitive and add the following three axioms to axioms – of Q:
Q+ is still a conservative extension of Q, in the sense that any formula provable in Q+ not containing the symbol "<" is already provable in Q.
Among the axioms – of Q, axiom needs an inner existential quantifier. Shoenfield gives an axiomatization that has only outer universal quantifiers, by dispensing with axiom of Q but adding the above three axioms with < as primitive. That is, Shoenfield's system is Q+ minus axiom, and is strictly weaker than Q+, since axiom is independent of the other axioms. Shoenfield's system also appears in Boolos et al., where it is called the "minimal arithmetic". A closely related axiomatization, that uses "≤" instead of "<", may be found in Machover.

Metamathematics

On the metamathematics of Q, see Boolos et al., Tarski, Mostowski, and Robinson, Smullyan, Mendelson, and Burgess. The intended interpretation of Q is the natural numbers and their usual arithmetic in which addition and multiplication have their customary meaning, identity is equality, and 0 is the natural number zero.
Any model that satisfies all axioms of Q except possibly axiom has a unique submodel isomorphic to the standard natural numbers. need not be satisfied; for example the polynomials with non-negative integer coefficients forms a model that satisfies all axioms except
Q, like Peano arithmetic, has nonstandard models of all infinite cardinalities. However, unlike Peano arithmetic, Tennenbaum's theorem does not apply to Q, and it has computable non-standard models. For instance, there is a computable model of Q consisting of integer-coefficient polynomials with positive leading coefficient, plus the zero polynomial, with their usual arithmetic.
A notable characteristic of Q is the absence of the axiom scheme of induction. Hence it is often possible to prove in Q every specific instance of a fact about the natural numbers, but not the associated general theorem. For example, 5 + 7 = 7 + 5 is provable in Q, but the general statement x + y = y + x is not. Similarly, one cannot prove that Sx ≠ x. A model of Q that fails many of the standard facts is obtained by adjoining two distinct new elements a and b to the standard model of natural numbers and defining Sa = a, Sb = b, x + a = b and x + b = a for all x, a + n = a and b + n = b if n is a standard natural number, x·0 = 0 for all x, a·n = b and b·n = a if n is a non-zero standard natural number, x·a = a for all x except x = a, x·b = b for all x except x = b, a·a = b, and b·b = a.
Q is interpretable in a fragment of Zermelo's axiomatic set theory, consisting of extensionality, existence of the empty set, and the axiom of adjunction. This theory is S' in Tarski et al. and ST in Burgess. See general set theory for more details.
Q is fascinating because it is a finitely axiomatized first-order theory that is considerably weaker than Peano arithmetic, and whose axioms contain only one existential quantifier, yet like PA is incomplete and incompletable in the sense of Gödel's incompleteness theorems, and essentially undecidable. Robinson derived the Q axioms – above by noting just what PA axioms are required to prove that every computable function is representable in PA. The only use this proof makes of the PA axiom schema of induction is to prove a statement that is axiom above, and so, all computable functions are representable in Q. The conclusion of Gödel's second incompleteness theorem also holds for Q: no consistent recursively axiomatized extension of Q can prove its own consistency, even if we additionally restrict Gödel numbers of proofs to a definable cut.
The first incompleteness theorem applies only to axiomatic systems defining sufficient arithmetic to carry out the necessary coding constructions. The axioms of Q were chosen specifically to ensure they are strong enough for this purpose. Thus the usual proof of the first incompleteness theorem can be used to show that Q is incomplete and undecidable. This indicates that the incompleteness and undecidability of PA cannot be blamed on the only aspect of PA differentiating it from Q, namely the axiom schema of induction.
Gödel's theorems do not hold when any one of the seven axioms above is dropped. These fragments of Q remain undecidable, but they are no longer essentially undecidable: they have consistent decidable extensions, as well as uninteresting models.