Robinson Arithmetic

Robinson arithmetic is the minimum amount of arithmetic needed for GoedelsIncompletenessTheorem. It consists of the following axioms.

• for all x, Sx =/= 0.
• for all x, y, (Sx = Sy) -> x = y.
• for all x, x + 0 = x.
• for all x, y, x + Sy = S(x + y).
• for all x, x0 = 0.
• for all x, y, xSy = (xy) + x.
• for all x, x = 0 or exists y such that Sy = x.