Robinson arithmetic

<h2 id="axioms">Axioms</h2>
The <a href="/facts/Formal_system/KaeDAjK7">background logic</a> of Q is <a href="/facts/First-order_logic/lcISqWIg">first-order logic with identity</a>, denoted by infix '='. The individuals, called <a href="/facts/Natural_number/u65og8JE">natural numbers</a>, are members of a <a href="/facts/Set_(mathematics)/BfucfHMq">set</a> called N with a distinguished member 0, called <a href="/facts/Zero/4NBRtKHc">zero</a>. There are three <a href="/facts/Operation_(mathematics)/Yplv602Q">operations</a> over N:

<ul><li>A <a href="/facts/Unary_operation/kb6CkgsX">unary operation</a> called <a href="/facts/Successor_function/R1hhkSEG">successor</a> and denoted by <a href="/facts/Prefix_notation/dUzpf2Ys">prefix</a> S;</li>
<li>Two <a href="/facts/Binary_operation/CYtow0bz">binary operations</a>, <a href="/facts/Addition/apFWJBFB">addition</a> and <a href="/facts/Multiplication/VtcUjpNv">multiplication</a>, denoted by infix + and ·, respectively.</li></ul>
The following <a href="/facts/Axiom/mLjP14Mc">axioms</a> for Q are Q1–Q7 in Burgess (2005, p. 42) (cf. also the axioms of <a href="/facts/First-order_arithmetic/DhhDnNug">first-order arithmetic</a>). <a href="/facts/Variable_(mathematics)/VbQlrvKz">Variables</a> not bound by an <a href="/facts/Existential_quantifier/hHveaBYo">existential quantifier</a> are bound by an implicit <a href="/facts/Universal_quantifier/agNmvJKN">universal quantifier</a>.

<ol><li>Sx ≠ 0
<ul><li>0 is not the successor of any number.</li></ul></li>
<li>(Sx = Sy) → x = y
<ul><li>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 <a href="/facts/Infinite_set/9rTN0xGH">infinite set</a> bounded by 0) and S (it is an <a href="/facts/Injective_function/5ES6tqf5">injective function</a> whose <a href="/facts/Domain_of_a_function/FQvoeUpX">domain</a> is N) needed for non-triviality. The <a href="/facts/Conversion_(logic)/VhlUrxxx">converse</a> of (2) follows from the properties of identity.</li></ul></li>
<li>y=0 ∨ ∃x (Sx = y)
<ul><li>Every number is either 0 or the successor of some number. The <a href="/facts/Axiom_schema/vKNTz5IT">axiom schema</a> of <a href="/facts/Mathematical_induction/KxAPqNrH">mathematical induction</a> present in arithmetics stronger than Q turns this axiom into a theorem.</li></ul></li>
<li>x + 0 = x</li>
<li>x + Sy = S(x + y)
<ul><li>(4) and (5) are the <a href="/facts/Recursive_definition/9RfhFw0R">recursive definition</a> of <a href="/facts/Addition/apFWJBFB">addition</a>.</li></ul></li>
<li>x·0 = 0</li>
<li>x·Sy = (x·y) + x
<ul><li>(6) and (7) are the <a href="/facts/Recursive_definition/9RfhFw0R">recursive definition</a> of <a href="/facts/Multiplication/VtcUjpNv">multiplication</a>.</li></ul></li></ol>
<h3>Variant axiomatizations</h3>
The axioms in Robinson (1950) are (1)–(13) in Mendelson (2015, pp. 202–203). The first 6 of Robinson's 13 axioms are required only when, unlike here, the background logic does not include identity.
The usual strict <a href="/facts/Total_order/xnTtmuYJ">total order</a> on N, "less than" (denoted by "<"), can be defined in terms of addition via the rule x < y ↔ ∃z (Sz + x = y). 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, Burgess & Jeffrey (2002, Sec 16.4).
A 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:

<ul><li>¬(x < 0)</li>
<li>x < Sy ↔ (x < y ∨ x = y)</li>
<li>x < y ∨ x = y ∨ y < x</li></ul>
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. (Adding only the first two of the above three axioms to Q gives a conservative extension of Q that is equivalent to what Burgess (2005, p. 56) calls Q*. See also Burgess (2005, p. 230, fn. 24), 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).)
Among the axioms (1)–(7) of Q, axiom (3) needs an inner existential quantifier. Shoenfield (1967, p. 22) gives 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. That 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 
 
 
 
 
 ω
 
 ω
 
 
 
 
 {\displaystyle \omega ^{\omega }}
 
 forms a model for all axioms except (3) when Sv is interpreted as v + 1). Shoenfield's system also appears in Boolos, Burgess & Jeffrey (2002, Sec 16.2), where it is called the "minimal arithmetic" (also denoted by Q). A closely related axiomatization, that uses "≤" instead of "<", may be found in Machover (1996, pp. 256–257).

<h2 id="metamathematics">Metamathematics</h2>
On the metamathematics of Q see Boolos, Burgess & Jeffrey (2002, chpt. 16), Tarski, Mostowski & Robinson (1953), Smullyan (1991), Mendelson (2015, pp. 202–203) and Burgess (2005, §§1.5a, 2.2). The <a href="/facts/Intended_interpretation/goPmjjQG">intended interpretation</a> of Q is the <a href="/facts/Natural_numbers/u65og8JE">natural numbers</a> and their usual arithmetic in which <a href="/facts/Addition/apFWJBFB">addition</a> and <a href="/facts/Multiplication/VtcUjpNv">multiplication</a> have their customary meaning, identity is <a href="/facts/Equality_(mathematics)/AQCuumLg">equality</a>, Sx = x + 1, and 0 is the natural number <a href="/facts/0_(number)/4NBRtKHc">zero</a>. 
Any 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). (Axiom (3) need not be satisfied; for example the <a href="/facts/Polynomial/Lzak8VVx">polynomials</a> with non-negative integer coefficients forms a model that satisfies all axioms except (3).)
Q, like <a href="/facts/Peano_arithmetic/DhhDnNug">Peano arithmetic</a>, has <a href="/facts/Non-standard_model_of_arithmetic/e3EktWqv">nonstandard models</a> of all infinite <a href="/facts/Cardinality/m6VPojwT">cardinalities</a>. However, unlike Peano arithmetic, <a href="/facts/Tennenbaum%27s_theorem/jnDXC24R">Tennenbaum's theorem</a> 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 <a href="/facts/Mathematical_induction/KxAPqNrH">induction</a>. 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 class="footnote-ref" id="fnref:2" href="#fn:2">2</a> 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.<a class="footnote-ref" id="fnref:3" href="#fn:3">3</a> 
Q is interpretable in a fragment of <a href="/facts/Zermelo_set_theory/o3fzd9nl">Zermelo's</a> <a href="/facts/Axiomatic_set_theory/1ptfsvUP">axiomatic set theory</a>, consisting of <a href="/facts/Extensionality/CwPNkVTW">extensionality</a>, existence of the <a href="/facts/Empty_set/ffEk3eA6">empty set</a>, and the <a href="/facts/Axiom_of_adjunction/KIYns85C">axiom of adjunction</a>. This theory is S' in Tarski, Mostowski & Robinson (1953, p. 34) and ST in Burgess (2005, pp. 90–91, 223). See <a href="/facts/General_set_theory/JPoRgzd7">general set theory</a> for more details.
Q is a finitely axiomatized <a href="/facts/List_of_first-order_theories/HAse4SIg">first-order theory</a> that is considerably weaker than <a href="/facts/Peano_arithmetic/DhhDnNug">Peano arithmetic</a> (PA), and whose axioms contain only one <a href="/facts/Existential_quantifier/hHveaBYo">existential quantifier</a>. Yet like PA it is incomplete and incompletable in the sense of <a href="/facts/G%C3%B6del%27s_incompleteness_theorems/du8PRu8g">Gödel's incompleteness theorems</a>, and essentially undecidable. Robinson (1950) derived the Q axioms (1)–(7) above by noting just what PA axioms are required <a class="footnote-ref" id="fnref:4" href="#fn:4">4</a> to prove that every <a href="/facts/Computable_function/dzwBlLGn">computable function</a> is representable in PA.<a class="footnote-ref" id="fnref:5" href="#fn:5">5</a> The only use this proof makes of the PA axiom schema of <a href="/facts/Mathematical_induction/KxAPqNrH">induction</a> is to prove a statement that is axiom (3) above, and so, all computable functions are representable in Q.<a class="footnote-ref" id="fnref:6" href="#fn:6">6</a><a class="footnote-ref" id="fnref:7" href="#fn:7">7</a><a class="footnote-ref" id="fnref:8" href="#fn:8">8</a> 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.<a class="footnote-ref" id="fnref:9" href="#fn:9">9</a><a class="footnote-ref" id="fnref:10" href="#fn:10">10</a><a class="footnote-ref" id="fnref:11" href="#fn:11">11</a>
The first incompleteness theorem applies only to axiomatic systems defining sufficient arithmetic to carry out the necessary coding constructions (of which <a href="/facts/G%C3%B6del_numbering/36BpTK1g">Gödel numbering</a> 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 <a href="/facts/Axiom_schema/vKNTz5IT">axiom schema</a> of <a href="/facts/Mathematical_induction/KxAPqNrH">induction</a>. 
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 that are not end-extensions of the standard natural numbers).

<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Gentzen%27s_consistency_proof/LTDpe0V8">Gentzen's consistency proof</a></li>
<li><a href="/facts/G%C3%B6del%27s_incompleteness_theorems/du8PRu8g">Gödel's incompleteness theorems</a></li>
<li><a href="/facts/List_of_first-order_theories/HAse4SIg">List of first-order theories</a></li>
<li><a href="/facts/Peano_axioms/DhhDnNug">Peano axioms</a></li>
<li><a href="/facts/Presburger_arithmetic/9R0WMG3h">Presburger arithmetic</a></li>
<li><a href="/facts/Skolem_arithmetic/4DYh7RYP">Skolem arithmetic</a></li>
<li><a href="/facts/Second-order_arithmetic/abBxQsaH">Second-order arithmetic</a></li>
<li><a href="/facts/Set-theoretic_definition_of_natural_numbers/pdr0WSDC">Set-theoretic definition of natural numbers</a></li>
<li><a href="/facts/General_set_theory/JPoRgzd7">General set theory</a></li></ul>

<h2 id="bibliography">Bibliography</h2>

<ul><li>Bezboruah, A.; Shepherdson, John C. (June 1976). "Gödel's Second Incompleteness Theorem for Q". <a href="/facts/Journal_of_Symbolic_Logic/lfXVXcoy">Journal of Symbolic Logic</a>. 41 (2): 503–512. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.2307%2F2272251">10.2307/2272251</a>. <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/2272251">2272251</a>.</li>
<li><a href="/facts/George_Boolos/K969uIhT">Boolos, George</a>; <a href="/facts/John_P._Burgess/vVxaBgbr">Burgess, John P.</a>; <a href="/facts/Richard_Jeffrey/fL2rpek3">Jeffrey, Richard</a> (2002). Computability and Logic (4th ed.). <a href="/facts/Cambridge_University_Press/fgEBSSRq">Cambridge University Press</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 0-521-00758-5.</li>
<li><a href="/facts/John_P._Burgess/vVxaBgbr">Burgess, John P.</a> (July 2005). Fixing Frege. <a href="/facts/Princeton_University_Press/kwvFlKEj">Princeton University Press</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-0691122311.</li>
<li>Hájek, Petr; Pudlák, Pavel (1993). Metamathematics of first-order arithmetic (2nd ed.). <a href="/facts/Springer-Verlag/nAesf6nT">Springer-Verlag</a>.</li>
<li>Jones, James P.; Shepherdson, John C. (1983). "Variants of Robinson's essentially undecidable theoryR". Archiv für mathematische Logik und Grundlagenforschung. 23: 61–64. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2FBF02023013">10.1007/BF02023013</a>. <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:2659126">2659126</a>.</li>
<li><a href="/facts/John_Lucas_(philosopher)/05eF8Gxj">Lucas, John R.</a> Conceptual Roots of Mathematics. Routledge.</li>
<li><a href="/facts/Mosh%C3%A9_Machover/pLb4BkGS">Machover, Moshé</a> (1996). Set Theory, Logic, and Their Limitation. <a href="/facts/Cambridge_University_Press/fgEBSSRq">Cambridge University Press</a>.</li>
<li><a href="/facts/Elliott_Mendelson/S6PpLYGJ">Mendelson, Elliott</a> (2015). Introduction to Mathematical Logic (6th ed.). Chapman & Hall. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 9781482237726.</li>
<li><a href="/facts/Piergiorgio_Odifreddi/oMqgCeTU">Odifreddi, Piergiorgio</a> (1989). Classical recursion theory, Vol. 1 (The Theory of Functions and Sets of Natural Numbers). Studies in Logic and the Foundations of Mathematics. Vol. 125. North-Holland. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 9780444894830.</li>
<li>Pudlák, Pavel (June 1985). "Cuts, consistency statements and interpretations". <a href="/facts/Journal_of_Symbolic_Logic/lfXVXcoy">Journal of Symbolic Logic</a>. 50 (2): 423–441. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.2307%2F2274231">10.2307/2274231</a>. <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/2274231">2274231</a>. <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:30289163">30289163</a>.</li>
<li><a href="/facts/Wolfgang_Rautenberg/bUWpeRmB">Rautenberg, Wolfgang</a> (2010). A Concise Introduction to Mathematical Logic (3rd ed.). New York: <a href="/facts/Springer_Science%2BBusiness_Media/nAesf6nT">Springer Science+Business Media</a>. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2F978-1-4419-1221-3">10.1007/978-1-4419-1221-3</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-1-4419-1220-6..</li>
<li><a href="/facts/Raphael_M._Robinson/c5egdfRe">Robinson, Raphael M.</a> (1950). "An Essentially Undecidable Axiom System". Proceedings of the International Congress of Mathematics: 729–730.</li>
<li><a href="/facts/Joseph_R._Shoenfield/FsWVVyye">Shoenfield, Joseph R.</a> (1967). Mathematical logic. Addison Wesley. (Reprinted by Association for Symbolic Logic and A K Peters in 2000).</li>
<li><a href="/facts/Raymond_Smullyan/UMEI6TgX">Smullyan, Raymond</a> (1991). Gödel's Incompleteness Theorems. <a href="/facts/Oxford_University_Press/CYyTzzWG">Oxford University Press</a>.</li>
<li><a href="/facts/Alfred_Tarski/7h6NySAj">Tarski, Alfred</a>; <a href="/facts/Andrzej_Mostowski/jIYwsCEC">Mostowski, Andrzej</a>; <a href="/facts/Raphael_M._Robinson/c5egdfRe">Robinson, Raphael M.</a> (1953). Undecidable theories. North Holland.</li>
<li>Vaught, Robert L. (1966). "On a Theorem of Cobham Concerning Undecidable Theories". Studies in Logic and the Foundations of Mathematics. 44: 14–25. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2FS0049-237X%2809%2970566-X">10.1016/S0049-237X(09)70566-X</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 9780804700962.</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">Robinson 1950. - Robinson, Raphael M. (1950). "An Essentially Undecidable Axiom System". Proceedings of the International Congress of Mathematics: 729–730. <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Burgess 2005, p. 56. - Burgess, John P. (July 2005). Fixing Frege. Princeton University Press. ISBN 978-0691122311. <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">Boolos, Burgess & Jeffrey 2002, Sec 16.4. - Boolos, George; Burgess, John P.; Jeffrey, Richard (2002). Computability and Logic (4th ed.). Cambridge University Press. ISBN 0-521-00758-5. <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">Mendelson 2015, p. 188, Proposition 3.24. - Mendelson, Elliott (2015). Introduction to Mathematical Logic (6th ed.). Chapman & Hall. ISBN 9781482237726. <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">A function 
 
 
 
 f
 
 
 {\displaystyle f}
 
 is said to be representable in 
 
 
 
 PA
 
 
 {\displaystyle \operatorname {PA} }
 
 if there is a formula 
 
 
 
 ϕ
 
 
 {\displaystyle \phi }
 
 such that for all 
 
 
 
 
 x
 
 1
 
 
 ,
 ⋯
 ,
 
 x
 
 k
 
 
 ,
 y
 
 
 {\displaystyle x_{1},\cdots ,x_{k},y}

f
        (
        
          
            
              x
              →
            
          
        
        )
        =
        y
        ⟺
        PA
        ⊢
        ϕ
        (
        
          
            
              x
              →
            
          
        
        ,
        y
        )
        ,
      
    
    {\displaystyle f({\vec {x}})=y\Longleftrightarrow \operatorname {PA} \vdash \phi ({\vec {x}},y),}

f
 (
 
 
 
 x
 →
 
 
 
 )
 ≠
 y
 ⟺
 PA
 ⊢
 ¬
 ϕ
 (
 
 
 
 x
 →
 
 
 
 ,
 y
 )
 .
 
 
 {\displaystyle f({\vec {x}})\neq y\Longleftrightarrow \operatorname {PA} \vdash \lnot \phi ({\vec {x}},y).}
 <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
<li id="fn:6">Odifreddi 1989. - Odifreddi, Piergiorgio (1989). Classical recursion theory, Vol. 1 (The Theory of Functions and Sets of Natural Numbers). Studies in Logic and the Foundations of Mathematics. Vol. 125. North-Holland. ISBN 9780444894830. <a href="#fnref:6" class="footnote-back-ref">↩</a></li>
<li id="fn:7">Mendelson 2015, p. 203, Proposition 3.33. - Mendelson, Elliott (2015). Introduction to Mathematical Logic (6th ed.). Chapman & Hall. ISBN 9781482237726. <a href="#fnref:7" class="footnote-back-ref">↩</a></li>
<li id="fn:8">Rautenberg 2010, p. 246. - Rautenberg, Wolfgang (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. <a href="https://doi.org/10.1007%2F978-1-4419-1221-3" target="_blank">https://doi.org/10.1007%2F978-1-4419-1221-3</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></li>
<li id="fn:9">Bezboruah & Shepherdson 1976. - Bezboruah, A.; Shepherdson, John C. (June 1976). "Gödel's Second Incompleteness Theorem for Q". Journal of Symbolic Logic. 41 (2): 503–512. doi:10.2307/2272251. JSTOR 2272251. <a href="https://doi.org/10.2307%2F2272251" target="_blank">https://doi.org/10.2307%2F2272251</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></li>
<li id="fn:10">Pudlák 1985. - Pudlák, Pavel (June 1985). "Cuts, consistency statements and interpretations". Journal of Symbolic Logic. 50 (2): 423–441. doi:10.2307/2274231. JSTOR 2274231. S2CID 30289163. <a href="https://doi.org/10.2307%2F2274231" target="_blank">https://doi.org/10.2307%2F2274231</a> <a href="#fnref:10" class="footnote-back-ref">↩</a></li>
<li id="fn:11">Hájek & Pudlák 1993, p. 387. - Hájek, Petr; Pudlák, Pavel (1993). Metamathematics of first-order arithmetic (2nd ed.). Springer-Verlag. <a href="#fnref:11" class="footnote-back-ref">↩</a></li>
</ol>

Robinson arithmetic open-in-new

Robinson arithmetic