Robinson arithmetic

Inmathematics,Robinson arithmeticis a finitely axiomatized fragment of first-orderPeano arithmetic(PA), first set out byRaphael M. Robinsonin 1950.^[1]It is usually denotedQ.Qis almost^{[clarification needed]}PA without theaxiom schemaofmathematical induction.Qis weaker than PA but it has the same language, and both theories areincomplete.Qis important and interesting because it is a finitely axiomatized fragment of PA that is recursively incompletable andessentially undecidable.

Axioms[edit]

Thebackground logicofQisfirst-order logic with identity,denoted by infix '='. The individuals, callednatural numbers,are members of asetcalledNwith a distinguished member0,calledzero.There are threeoperationsoverN:

Aunary operationcalledsuccessorand denoted byprefixS;
Twobinary operations,additionandmultiplication,denoted by infix+and·,respectively.

The followingaxiomsforQare Q1–Q7 inBurgess (2005,p. 42) (cf. also the axioms offirst-order arithmetic).Variablesnot bound by anexistential quantifierare bound by an implicituniversal quantifier.

Sx≠0
- 0is not the successor of any number.
(Sx=Sy) →x=y
- If the successor ofxis identical to the successor ofy,thenxandyare identical. (1) and (2) yield the minimum of facts aboutN(it is aninfinite setbounded by0) andS(it is aninjective functionwhosedomainisN) needed for non-triviality. Theconverseof (2) follows from the properties of identity.
y=0∨ ∃x(Sx=y)
- Every number is either0or the successor of some number. Theaxiom schemaofmathematical inductionpresent in arithmetics stronger thanQturns this axiom into a theorem.
x+0=x
x+Sy=S(x+y)
- (4) and (5) are therecursive definitionofaddition.
x·0=0
x·Sy= (x·y) +x
- (6) and (7) are therecursive definitionofmultiplication.

Variant axiomatizations[edit]

The axioms inRobinson (1950)are (1)–(13) inMendelson (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 stricttotal orderonN,"less than" (denoted by "<" ), can be defined in terms of addition via the rulex<y↔ ∃z(Sz+x=y).Equivalently, we get a definitional conservative extension ofQby taking "<" as primitive and adding this rule as an eighth axiom; this system is termed "Robinson arithmeticR"inBoolos, Burgess & Jeffrey (2002,Sec 16.4).

A different extension ofQ,which we temporarily callQ+,is obtained if we take "<" as primitive and add (instead of the last definitional axiom) the following three axioms to axioms (1)–(7) ofQ:

¬(x< 0)
x<Sy↔ (x<y∨x=y)
x<y∨x=y∨y<x

Q+is still a conservative extension ofQ,in the sense that any formula provable inQ+not containing the symbol "<" is already provable inQ.(Adding only the first two of the above three axioms toQgives a conservative extension ofQthat is equivalent to whatBurgess (2005,p. 56) callsQ*.See alsoBurgess (2005,p. 230, fn. 24), but note that the second of the above three axioms cannot be deduced from "the pure definitional extension" ofQobtained by adding only the axiomx<y↔ ∃z(Sz+x=y).)

Among the axioms (1)–(7) ofQ,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) ofQbut adding the above three axioms with < as primitive. That is, Shoenfield's system isQ+minus axiom (3), and is strictly weaker thanQ+,since axiom (3) is independent of the other axioms (for example, the ordinals less than $\ Omega ^{\ Omega }$ forms a model for all axioms except (3) whenSvis interpreted asv+ 1). Shoenfield's system also appears inBoolos, Burgess & Jeffrey (2002,Sec 16.2), where it is called the "minimal arithmetic"(also denoted byQ). A closely related axiomatization, that uses "≤" instead of "<", may be found inMachover (1996,pp. 256–257).

Metamathematics[edit]

On the metamathematics ofQseeBoolos, Burgess & Jeffrey (2002,chpt. 16),Tarski, Mostowski & Robinson (1953),Smullyan (1991),Mendelson (2015,pp. 202–203) andBurgess (2005,§§1.5a, 2.2). Theintended interpretationofQis thenatural numbersand their usual arithmetic in whichadditionandmultiplicationhave their customary meaning, identity isequality,Sx=x+ 1,and0is the natural numberzero.

Any model (structure) that satisfies all axioms ofQexcept 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 thepolynomialswith non-negative integer coefficients forms a model that satisfies all axioms except (3).)

Q,likePeano arithmetic,hasnonstandard modelsof all infinitecardinalities.However, unlike Peano arithmetic,Tennenbaum's theoremdoes not apply toQ,and it has computable non-standard models. For instance, there is a computable model ofQconsisting of integer-coefficient polynomials with positive leading coefficient, plus the zero polynomial, with their usual arithmetic.

A notable characteristic ofQis the absence of the axiom scheme ofinduction.Hence it is often possible to prove inQevery specific instance of a fact about the natural numbers, but not the associated general theorem. For example, 5 + 7 = 7 + 5 is provable inQ,but the general statementx+y=y+xis not. Similarly, one cannot prove thatSx≠x.^[2]A model ofQthat fails many of the standard facts is obtained by adjoining two distinct new elementsaandbto the standard model of natural numbers and definingSa=a,Sb=b,x+a=bandx+b=afor allx,a+n=aandb+n=bifnis a standard natural number,x·0 = 0 for allx,a·n=bandb·n=aifnis a non-zero standard natural number,x·a=afor allxexceptx=a,x·b=bfor allxexceptx=b,a·a=b,andb·b=a.^[3]

Qis interpretable in a fragment ofZermelo's axiomatic set theory,consisting ofextensionality,existence of theempty set,and theaxiom of adjunction.This theory is S' inTarski, Mostowski & Robinson (1953,p. 34) and ST inBurgess (2005,pp. 90–91, 223). Seegeneral set theoryfor more details.

Qis a finitely axiomatizedfirst-order theorythat is considerably weaker thanPeano arithmetic(PA), and whose axioms contain only oneexistential quantifier.Yet like PA it is incomplete and incompletable in the sense ofGödel's incompleteness theorems,and essentially undecidable.Robinson (1950)derived theQaxioms (1)–(7) above by noting just what PA axioms are required^[4]to prove that everycomputable functionis representable in PA.^[5]The only use this proof makes of the PA axiom schema ofinductionis to prove a statement that is axiom (3) above, and so, all computable functions are representable inQ.^[6]^[7]^[8]The conclusion of Gödel's second incompleteness theorem also holds forQ:no consistent recursively axiomatized extension ofQcan prove its own consistency, even if we additionally restrict Gödel numbers of proofs to a definable cut.^[9]^[10]^[11]

The first incompleteness theorem applies only to axiomatic systems defining sufficient arithmetic to carry out the necessary coding constructions (of whichGödel numberingforms a part). The axioms ofQwere 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 thatQis incomplete and undecidable. This indicates that the incompleteness and undecidability of PA cannot be blamed on the only aspect of PA differentiating it fromQ,namely theaxiom schemaofinduction.

Gödel's theorems do not hold when any one of the seven axioms above is dropped. These fragments ofQremain 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).^{[citation needed]}

References[edit]

^Robinson 1950.
^Burgess 2005,p. 56.
^Boolos, Burgess & Jeffrey 2002,Sec 16.4.
^Mendelson 2015,p. 188, Proposition 3.24.
^A function $f$ is said to berepresentablein $\operatorname {PA}$ if there is a formula $\phi$ such that for all $x_{1},\cdots,x_{k},y$
$f({\vec {x}})=y\Longleftrightarrow \operatorname {PA} \vdash \phi ({\vec {x}},y),$

$f({\vec {x}})\neq y\Longleftrightarrow \operatorname {PA} \vdash \lnot \phi ({\vec {x}},y).$
^Odifreddi 1989.
^Mendelson 2015,p. 203, Proposition 3.33.
^Rautenberg 2010,p. 246.
^Bezboruah & Shepherdson 1976.
^Pudlák 1985.
^Hájek & Pudlák 1993,p. 387.

Bibliography[edit]

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.
Boolos, George;Burgess, John P.;Jeffrey, Richard(2002).Computability and Logic(4th ed.).Cambridge University Press.ISBN 0-521-00758-5.
Burgess, John P.(July 2005).Fi xing Frege.Princeton University Press.ISBN 978-0691122311.
Hájek, Petr; Pudlák, Pavel (1993).Metamathematics of first-order arithmetic(2nd ed.).Springer-Verlag.
Jones, James P.; Shepherdson, John C. (1983). "Variants of Robinson's essentially undecidable theoryR".Archiv für mathematische Logik und Grundlagenforschung.23:61–64.doi:10.1007/BF02023013.S2CID 2659126.
Lucas, John R.Conceptual Roots of Mathematics.Routledge.
Machover, Moshé(1996).Set Theory, Logic, and Their Limitation.Cambridge University Press.
Mendelson, Elliott(2015).Introduction to Mathematical Logic(6th ed.). Chapman & Hall.ISBN 9781482237726.
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.
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.
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..
Robinson, Raphael M.(1950). "An Essentially Undecidable Axiom System".Proceedings of the International Congress of Mathematics:729–730.
Shoenfield, Joseph R.(1967).Mathematical logic.Addison Wesley. (Reprinted by Association for Symbolic Logic and A K Peters in 2000).
Smullyan, Raymond(1991).Gödel's Incompleteness Theorems.Oxford University Press.
Tarski, Alfred;Mostowski, Andrzej;Robinson, Raphael M.(1953).Undecidable theories.North Holland.
Vaught, Robert L. (1966). "On a Theorem of Cobham Concerning Undecidable Theories".Studies in Logic and the Foundations of Mathematics.44:14–25.doi:10.1016/S0049-237X(09)70566-X.ISBN 9780804700962.

[FOOTNOTERobinson1950-1] Robinson 1950.

[FOOTNOTEBurgess200556-2] Burgess 2005,p. 56.

[FOOTNOTEBoolosBurgessJeffrey2002Sec_16.4-3] Boolos, Burgess & Jeffrey 2002,Sec 16.4.

[FOOTNOTEMendelson2015188Proposition_3.24-4] Mendelson 2015,p. 188, Proposition 3.24.

[5] A function $f$ is said to berepresentablein $\operatorname {PA}$ if there is a formula $\phi$ such that for all $x_{1},\cdots,x_{k},y$
$f({\vec {x}})=y\Longleftrightarrow \operatorname {PA} \vdash \phi ({\vec {x}},y),$

$f({\vec {x}})\neq y\Longleftrightarrow \operatorname {PA} \vdash \lnot \phi ({\vec {x}},y).$

[FOOTNOTEOdifreddi1989-6] Odifreddi 1989.

[FOOTNOTEMendelson2015203Proposition_3.33-7] Mendelson 2015,p. 203, Proposition 3.33.

[FOOTNOTERautenberg2010246-8] Rautenberg 2010,p. 246.

[FOOTNOTEBezboruahShepherdson1976-9] Bezboruah & Shepherdson 1976.

[FOOTNOTEPudlák1985-10] Pudlák 1985.

[FOOTNOTEHájekPudlák1993387-11] Hájek & Pudlák 1993,p. 387.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

Axioms[edit]

Variant axiomatizations[edit]

Metamathematics[edit]

See also[edit]

References[edit]

Bibliography[edit]