Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Robinson arithmetic
Summary
In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), 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.
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:
A unary operation called successor and denoted by prefix S;
Two binary operations, addition and multiplication, denoted by infix + and ·, respectively.
The following axioms for Q are Q1–Q7 in (cf. also the 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)
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.
x + 0 = x
x + Sy = S(x + y)
(4) and (5) are the recursive definition of addition.
x·0 = 0
x·Sy = (x·y) + x
(6) and (7) are the recursive definition of multiplication.
The axioms in are (1)–(13) in . 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" (denoted by "
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.