In mathematics, Robinson arithmetic, or Q, is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out in R. M. Robinson (1950). Q is essentially PA without the axiom schema of 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.
The background logic[clarification needed] 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:
- A unary operation called successor and denoted by prefix S;
- Two binary operations, addition and multiplication, denoted by infix + and by concatenation, respectively.
The following axioms for Q are Q1–Q7 in Burgess (2005: 56), and are also the first seven axioms of first-order arithmetic. Variables not bound by an existential quantifier are bound by an implicit universal quantifier.
- Sx ≠ 0
- 0 is not the successor of any number.
- (Sx = Sy) → x = y
- If the successor of x is identical to the successor of y, then x and y are identical. (1) and (2) yield the minimum of facts about N (it is an infinite set bounded by 0) and S (it is an injective function whose domain is N) needed for non-triviality. The converse of (2) follows from the properties of identity.
- y=0 ∨ ∃x (Sx = y)
- x + 0 = x
- x + Sy = S(x + y)
- x·0 = 0
- x·Sy = (x·y) + x
The axioms in Robinson (1950) are (1)–(13) in Mendelson (1997: 201). The first 6 of Robinson's 13 axioms are required only when, unlike here, the background logic does not include identity. Machover (1996: 256–57) dispenses with axiom (3).
The usual strict total order on N, "less than" (denoted by "<"), can be defined in terms of addition via the rule x < y ↔ ∃z (Sz + x = y) (Burgess 2005:230, fn. 24).
Taking "<" as primitive requires adding four axioms to (1)–(7) above:
- ¬(x < 0)
- 0 = x ∨ 0 < x
- x < y ↔ (Sx < y ∨ Sx = y)
- x < Sy ↔ (x < y ∨ x = y).
Another axiomatization using < may be found in Shoenfield (1967: 22).
On the metamathematics of Q, see Boolos et al. (2002: chpt. 14), Tarski, Mostowski, and Robinson (1953), Smullyan (1991), Mendelson (1997: 201–03), and Burgess (2005: §§1.5a, 2.2). 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, Sx = x + 1, and 0 is the natural number zero.
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 (Burgess 2005:56).
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. (1953: 34) and ST in Burgess (2005: 90–91; 223). 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 (PA), 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 (1950) derived the Q axioms (1)–(7) above by noting just what PA axioms are required to prove (Mendelson 1997: Th. 3.24) that every computable function is representable[clarification needed] in PA. The only use this proof makes of the PA axiom schema of induction is to prove a statement that is axiom (3) above, and so, all computable functions are representable in Q (Mendelson 1997: Th. 3.33, Rautenberg 2010: 246). 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 (Bezboruah and Shepherdson 1976; Pudlák 1985; Hájek & Pudlák 1993:387).
The first incompleteness theorem applies only to axiomatic systems defining sufficient arithmetic to carry out the necessary coding constructions (of which Gödel numbering forms a part). 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 (i.e., models which are not end-extensions of the standard natural numbers).
- General set theory
- Gentzen's consistency proof
- Gödel's incompleteness theorem
- List of first-order theories
- Peano axioms
- Second-order arithmetic
- Set-theoretic definition of natural numbers
- A. Bezboruah and John C. Shepherdson, 1976. "Gödel's Second Incompleteness Theorem for Q". Journal of Symbolic Logic v. 41 n. 2, pp. 503–512.
- George Boolos, John P. Burgess, and Richard Jeffrey, 2002. Computability and Logic, 4th ed. Cambridge University Press.
- Burgess, John P., 2005. Fixing Frege. Princeton University Press.
- Petr Hájek and Pavel Pudlák (1998) . Metamathematics of first-order arithmetic, 2nd ed. Springer-Verlag.
- Lucas, J. R., 1999. Conceptual Roots of Mathematics. Routledge.
- Machover, Moshe, 1996. Set Theory, Logic, and Their Limitation. Cambridge University Press.
- Mendelson, Elliott, 1997. Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
- Pavel Pudlák, 1985. "Cuts, consistency statements and interpretations". Journal of Symbolic Logic v. 50 n. 2, pp. 423–441.
- W. Rautenberg (2010), A Concise Introduction to Mathematical Logic (3rd ed.), New York: Springer Science+Business Media, doi:10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6.
- R. M. Robinson, 1950, "An Essentially Undecidable Axiom System" in Proceedings of the International Congress of Mathematics 1950, pp. 729–730.
- Joseph R. Shoenfield, 1967. Mathematical logic. Addison Wesley. (Reprinted by Association for Symbolic Logic and A K Peters in 2000.)
- Raymond Smullyan, 1991. Gödel's Incompleteness Theorems. Oxford University Press.
- Alfred Tarski, A. Mostowski, and R. M. Robinson, 1953. Undecidable theories. North Holland.