{"history":[],"article":{"id":"d7f524e1-a30f-4c12-96b7-b4a502e9967a","title":"Robinson arithmetic","slug":"robinson-arithmetic","content":":::summary\n:::\n\n# \nIn [mathematics](https://bliptext.com/articles/mathematics), **Robinson arithmetic** is a finitely axiomatized fragment of first-order [Peano arithmetic](https://bliptext.com/articles/peano-arithmetic) (PA), first set out by [Raphael M. Robinson](https://bliptext.com/articles/raphael-m-robinson) in 1950.\nIt is usually denoted **Q**.\n**Q** is almost PA without the [axiom schema](https://bliptext.com/articles/axiom-schema) of [mathematical induction](https://bliptext.com/articles/mathematical-induction).\n**Q** is weaker than PA but it has the same language, and both theories are [incomplete](https://bliptext.com/articles/complete-theory).\n**Q** is important and interesting because it is a finitely axiomatized fragment of PA that is recursively incompletable and [essentially undecidable](https://bliptext.com/articles/decidability-logic).\n\n# Axioms\nThe [background logic](https://bliptext.com/articles/formal-system) of **Q** is [first-order logic with identity](https://bliptext.com/articles/first-order-logic), denoted by infix '='.\nThe individuals, called [natural numbers](https://bliptext.com/articles/natural-number), are members of a [set](https://bliptext.com/articles/set-mathematics) called **N** with a distinguished member **0**, called [zero](https://bliptext.com/articles/zero).\nThere are three [operations](https://bliptext.com/articles/operation-mathematics) over **N**:\nThe following [axioms](https://bliptext.com/articles/axiom) for **Q** are **Q**1–**Q**7 in (cf. also the [axioms](https://bliptext.com/articles/axiom) of [first-order arithmetic](https://bliptext.com/articles/first-order-arithmetic)).\n[Variables](https://bliptext.com/articles/variable-mathematics) not bound by an [existential quantifier](https://bliptext.com/articles/existential-quantifier) are bound by an implicit [universal quantifier](https://bliptext.com/articles/universal-quantifier).\n\n## Variant axiomatizations\nThe axioms in are (1)–(13) in.\nThe first 6 of Robinson's 13 axioms are required only when, unlike here, the background logic does not include identity.\nThe usual strict [total order](https://bliptext.com/articles/total-order) on **N**, \"less than\" (denoted by \"<\"), can be defined in terms of addition via the rule x < y ↔ ∃z (Sz + x = y).\nEquivalently, we get a definitional conservative extension of **Q** by taking \"<\" as primitive and adding this rule as an eighth axiom; this system is termed \"**R**obinson arithmetic **R**\" in.\nA different extension of ****Q****, which we temporarily call ****Q****+, is obtained if we take \"<\" as primitive and add (instead of the last definitional axiom) the following three axioms to axioms (1)–(7) of ****Q****:\n******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****.\n(Adding only the first two of the above three axioms to ********Q******** gives a conservative extension of ********Q******** that is equivalent to what calls ********Q*********. See also, but note that the second of the above three axioms cannot be deduced from \"the pure definitional extension\" of ********Q******** obtained by adding only the axiom x < y ↔ ∃z (Sz + x = y).)\nAmong the axioms (1)–(7) of **Q**, axiom (3) needs an inner existential quantifier.\ngives an axiomatization that has only (implicit) outer universal quantifiers, by dispensing with axiom (3) of **Q** but adding the above three axioms with < as primitive.\nThat is, Shoenfield's system is ****Q+**** minus axiom (3), and is strictly weaker than ****Q+****, since axiom (3) is independent of the other axioms (for example, the ordinals less than forms a model for all axioms except (3) when Sv is interpreted as v + 1).\nShoenfield's system also appears in, where it is called the \"minimal arithmetic\" (also denoted by **Q**).\nA closely related axiomatization, that uses \"≤\" instead of \"<\", may be found in.\n\n# Metamathematics\nOn the metamathematics of **Q** see, , , and.\nThe [intended interpretation](https://bliptext.com/articles/intended-interpretation) of **Q** is the [natural numbers](https://bliptext.com/articles/natural-numbers) and their usual arithmetic in which [addition](https://bliptext.com/articles/addition) and [multiplication](https://bliptext.com/articles/multiplication) have their customary meaning, identity is [equality](https://bliptext.com/articles/equality-mathematics), and **0** is the natural number [zero](https://bliptext.com/articles/0-number).\nAny model (structure) that satisfies all axioms of **Q** except possibly axiom (3) has a unique submodel (\"the standard part\") isomorphic to the standard natural numbers (N, +, ·, S, 0).\n(Axiom (3) need not be satisfied; for example the [polynomials](https://bliptext.com/articles/polynomial) with non-negative integer coefficients forms a model that satisfies all axioms except (3).)\n**Q**, like [Peano arithmetic](https://bliptext.com/articles/peano-arithmetic), has [nonstandard models](https://bliptext.com/articles/non-standard-model-of-arithmetic) of all infinite [cardinalities](https://bliptext.com/articles/cardinality).\nHowever, unlike Peano arithmetic, [Tennenbaum's theorem](https://bliptext.com/articles/tennenbaum-s-theorem) does not apply to **Q**, and it has computable non-standard models.\nFor 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.\nA notable characteristic of **Q** is the absence of the axiom scheme of [induction](https://bliptext.com/articles/mathematical-induction).\nHence it is often possible to prove in **Q** every specific instance of a fact about the natural numbers, but not the associated general theorem.\nFor example, 5 + 7 = 7 + 5 is provable in **Q**, but the general statement x + y = y + x is not.\nSimilarly, one cannot prove that Sx ≠ x.\nA 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.\n**Q** is interpretable in a fragment of [Zermelo's](https://bliptext.com/articles/zermelo-set-theory) [axiomatic set theory](https://bliptext.com/articles/axiomatic-set-theory), consisting of [extensionality](https://bliptext.com/articles/extensionality), existence of the [empty set](https://bliptext.com/articles/empty-set), and the [axiom of adjunction](https://bliptext.com/articles/axiom-of-adjunction).\nThis theory is S' in and ST in.\nSee [general set theory](https://bliptext.com/articles/general-set-theory) for more details.\n**Q** is a finitely axiomatized [first-order theory](https://bliptext.com/articles/list-of-first-order-theories) that is considerably weaker than [Peano arithmetic](https://bliptext.com/articles/peano-arithmetic) (PA), and whose axioms contain only one [existential quantifier](https://bliptext.com/articles/existential-quantifier).\nYet like PA it is incomplete and incompletable in the sense of [Gödel's incompleteness theorems](https://bliptext.com/articles/g-del-s-incompleteness-theorems), and essentially undecidable.\nderived the ****Q**** axioms (1)–(7) above by noting just what PA axioms are required to prove that every [computable function](https://bliptext.com/articles/computable-function) is representable in PA. The only use this proof makes of the PA axiom schema of [induction](https://bliptext.com/articles/mathematical-induction) is to prove a statement that is axiom (3) above, and so, all [computable function](https://bliptext.com/articles/computable-function)s are representable in ****Q****.\nThe 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.\nThe first incompleteness theorem applies only to axiomatic systems defining sufficient arithmetic to carry out the necessary coding constructions (of which [Gödel numbering](https://bliptext.com/articles/g-del-numbering) forms a part).\nThe axioms of **Q** were chosen specifically to ensure they are strong enough for this purpose.\nThus the usual proof of the first incompleteness theorem can be used to show that **Q** is incomplete and undecidable.\nThis 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](https://bliptext.com/articles/axiom-schema) of [induction](https://bliptext.com/articles/mathematical-induction).\nGödel's theorems do not hold when any one of the seven axioms above is dropped.\nThese 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 that are not end-extensions of the standard natural numbers).","current_revision":null,"created_by":"kACnuQmH5k9Nr5VNVEpVeg7XpvUmMctD","created_at":"2025-01-25T22:11:37.037Z","updated_at":"2025-01-25T22:11:37.037Z","search_vector":"'arithmet':2 'robinson':1","search_content":" \n \n\n# \nIn [mathematics](https://bliptext.com/articles/mathematics), **Robinson arithmetic** is a finitely axiomatized fragment of first-order [Peano arithmetic](https://bliptext.com/articles/peano-arithmetic) (PA), first set out by [Raphael M. Robinson](https://bliptext.com/articles/raphael-m-robinson) in 1950.\nIt is usually denoted **Q**.\n**Q** is almost PA without the [axiom schema](https://bliptext.com/articles/axiom-schema) of [mathematical induction](https://bliptext.com/articles/mathematical-induction).\n**Q** is weaker than PA but it has the same language, and both theories are [incomplete](https://bliptext.com/articles/complete-theory).\n**Q** is important and interesting because it is a finitely axiomatized fragment of PA that is recursively incompletable and [essentially undecidable](https://bliptext.com/articles/decidability-logic).\n\n# Axioms\nThe [background logic](https://bliptext.com/articles/formal-system) of **Q** is [first-order logic with identity](https://bliptext.com/articles/first-order-logic), denoted by infix '='.\nThe individuals, called [natural numbers](https://bliptext.com/articles/natural-number), are members of a [set](https://bliptext.com/articles/set-mathematics) called **N** with a distinguished member **0**, called [zero](https://bliptext.com/articles/zero).\nThere are three [operations](https://bliptext.com/articles/operation-mathematics) over **N**:\nThe following [axioms](https://bliptext.com/articles/axiom) for **Q** are **Q**1–**Q**7 in (cf. also the [axioms](https://bliptext.com/articles/axiom) of [first-order arithmetic](https://bliptext.com/articles/first-order-arithmetic)).\n[Variables](https://bliptext.com/articles/variable-mathematics) not bound by an [existential quantifier](https://bliptext.com/articles/existential-quantifier) are bound by an implicit [universal quantifier](https://bliptext.com/articles/universal-quantifier).\n\n## Variant axiomatizations\nThe axioms in are (1)–(13) in.\nThe first 6 of Robinson's 13 axioms are required only when, unlike here, the background logic does not include identity.\nThe usual strict [total order](https://bliptext.com/articles/total-order) on **N**, \"less than\" (denoted by \"<\"), can be defined in terms of addition via the rule x < y ↔ ∃z (Sz + x = y).\nEquivalently, we get a definitional conservative extension of **Q** by taking \"<\" as primitive and adding this rule as an eighth axiom; this system is termed \"**R**obinson arithmetic **R**\" in.\nA different extension of ****Q****, which we temporarily call ****Q****+, is obtained if we take \"<\" as primitive and add (instead of the last definitional axiom) the following three axioms to axioms (1)–(7) of ****Q****:\n******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****.\n(Adding only the first two of the above three axioms to ********Q******** gives a conservative extension of ********Q******** that is equivalent to what calls ********Q*********. See also, but note that the second of the above three axioms cannot be deduced from \"the pure definitional extension\" of ********Q******** obtained by adding only the axiom x < y ↔ ∃z (Sz + x = y).)\nAmong the axioms (1)–(7) of **Q**, axiom (3) needs an inner existential quantifier.\ngives an axiomatization that has only (implicit) outer universal quantifiers, by dispensing with axiom (3) of **Q** but adding the above three axioms with < as primitive.\nThat is, Shoenfield's system is ****Q+**** minus axiom (3), and is strictly weaker than ****Q+****, since axiom (3) is independent of the other axioms (for example, the ordinals less than forms a model for all axioms except (3) when Sv is interpreted as v + 1).\nShoenfield's system also appears in, where it is called the \"minimal arithmetic\" (also denoted by **Q**).\nA closely related axiomatization, that uses \"≤\" instead of \"<\", may be found in.\n\n# Metamathematics\nOn the metamathematics of **Q** see, , , and.\nThe [intended interpretation](https://bliptext.com/articles/intended-interpretation) of **Q** is the [natural numbers](https://bliptext.com/articles/natural-numbers) and their usual arithmetic in which [addition](https://bliptext.com/articles/addition) and [multiplication](https://bliptext.com/articles/multiplication) have their customary meaning, identity is [equality](https://bliptext.com/articles/equality-mathematics), and **0** is the natural number [zero](https://bliptext.com/articles/0-number).\nAny model (structure) that satisfies all axioms of **Q** except possibly axiom (3) has a unique submodel (\"the standard part\") isomorphic to the standard natural numbers (N, +, ·, S, 0).\n(Axiom (3) need not be satisfied; for example the [polynomials](https://bliptext.com/articles/polynomial) with non-negative integer coefficients forms a model that satisfies all axioms except (3).)\n**Q**, like [Peano arithmetic](https://bliptext.com/articles/peano-arithmetic), has [nonstandard models](https://bliptext.com/articles/non-standard-model-of-arithmetic) of all infinite [cardinalities](https://bliptext.com/articles/cardinality).\nHowever, unlike Peano arithmetic, [Tennenbaum's theorem](https://bliptext.com/articles/tennenbaum-s-theorem) does not apply to **Q**, and it has computable non-standard models.\nFor 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.\nA notable characteristic of **Q** is the absence of the axiom scheme of [induction](https://bliptext.com/articles/mathematical-induction).\nHence it is often possible to prove in **Q** every specific instance of a fact about the natural numbers, but not the associated general theorem.\nFor example, 5 + 7 = 7 + 5 is provable in **Q**, but the general statement x + y = y + x is not.\nSimilarly, one cannot prove that Sx ≠ x.\nA 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.\n**Q** is interpretable in a fragment of [Zermelo's](https://bliptext.com/articles/zermelo-set-theory) [axiomatic set theory](https://bliptext.com/articles/axiomatic-set-theory), consisting of [extensionality](https://bliptext.com/articles/extensionality), existence of the [empty set](https://bliptext.com/articles/empty-set), and the [axiom of adjunction](https://bliptext.com/articles/axiom-of-adjunction).\nThis theory is S' in and ST in.\nSee [general set theory](https://bliptext.com/articles/general-set-theory) for more details.\n**Q** is a finitely axiomatized [first-order theory](https://bliptext.com/articles/list-of-first-order-theories) that is considerably weaker than [Peano arithmetic](https://bliptext.com/articles/peano-arithmetic) (PA), and whose axioms contain only one [existential quantifier](https://bliptext.com/articles/existential-quantifier).\nYet like PA it is incomplete and incompletable in the sense of [Gödel's incompleteness theorems](https://bliptext.com/articles/g-del-s-incompleteness-theorems), and essentially undecidable.\nderived the ****Q**** axioms (1)–(7) above by noting just what PA axioms are required to prove that every [computable function](https://bliptext.com/articles/computable-function) is representable in PA. The only use this proof makes of the PA axiom schema of [induction](https://bliptext.com/articles/mathematical-induction) is to prove a statement that is axiom (3) above, and so, all [computable function](https://bliptext.com/articles/computable-function)s are representable in ****Q****.\nThe 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.\nThe first incompleteness theorem applies only to axiomatic systems defining sufficient arithmetic to carry out the necessary coding constructions (of which [Gödel numbering](https://bliptext.com/articles/g-del-numbering) forms a part).\nThe axioms of **Q** were chosen specifically to ensure they are strong enough for this purpose.\nThus the usual proof of the first incompleteness theorem can be used to show that **Q** is incomplete and undecidable.\nThis 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](https://bliptext.com/articles/axiom-schema) of [induction](https://bliptext.com/articles/mathematical-induction).\nGödel's theorems do not hold when any one of the seven axioms above is dropped.\nThese 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 that are not end-extensions of the standard natural numbers).","revisionCount":0},"hasMore":false,"nextCursor":null}

History