Robinson arithmetic

The Robinson arithmetic (including Q) is a finitely axiomatisiertes fragment of Peano arithmetic, a system of axioms of arithmetic, ie, the natural numbers, within the first order predicate logic. It was introduced in 1950 by Raphael Robinson and substantially corresponds to the Peano arithmetic without the axiom schema induction. The importance of Robinson arithmetic is because it is finite, but it is still not recursive vervollständigbar and even much undecidable. This means that there is no consistent decidable extension Robinson arithmetic. There are also specifically not a complete recursively enumerable extension, as it already recursive ( decidable ) would be.

Axioms

The Robinson arithmetic formulated in the first order predicate logic with equality, represented by the predicate '='. Their language has the constant 0 " zero ", the successor function S, which adds intuitive to a given number one, and the functions for addition and multiplication for ✕. It has the following axioms, the fundamental properties of natural numbers and the arithmetic operations formalize:

• Zero has no predecessor:
• Different numbers have different successors:
• Each number is zero or has a predecessor:
• Recursive definition of addition and multiplication:

Significance for Mathematical Logic

The Robinson arithmetic plays in particular in the proof of the first Gödel's incompleteness theorem is relevant, as the predicate of provability of a formula can represent within Q (as well as in consistent axiomatic extensions of Q).

This means representability of a predicate P that there is a formula such that for all natural numbers (including zero) applies:

The term is defined as follows:

Since the Beweisbarkeitsprädikat can be represented by a Σ1 - formula, its representability is essential in the Σ1 - completeness of Q, while by Σ1 - completeness to understand here that each Σ1 - statement ( the language of Q), the natural for the numbers applies, even in Q is provable.

Q is interpretable already in relatively weak subtheories of ZFC, such as the so-called Tarski fragment TF, which consists only of the following three axioms: the axiom of extensionality (also axiom of determinacy ), the empty set axiom (also null set axiom: the empty set exists) and the axiom which calls for two sets x, y the existence of the ( adjoint ) x ∪ { y}.