Robinson Arithmetic (Q)

Origin. Raphael Robinson, "An essentially undecidable axiom system" (1950); Tarski, Mostowski, and Robinson, Undecidable Theories (1953), where Q and R are isolated together as base theories and Q became the standard instrument. Built for one purpose: a finitely axiomatized arithmetic still strong enough for Gödel's argument, so that undecidability could be proved for anything interpreting it.

Models. Peano arithmetic minus induction, and almost nothing survives — Q cannot prove that addition is commutative, or that 0 + x = x, or that ≤ is transitive. What it can do is represent every computable function and prove every true Σ₁ sentence, and that is all incompleteness needs. Any theory that interprets Q is essentially undecidable, and most theories do. Q is not the floor: Theory R is essentially undecidable and does not interpret Q, and there is no interpretability-minimal essentially undecidable theory at all (Pakhomov–Murwanashyaka–Visser 2022). Q is a degree, not a bottom.

Formalism.

Language: 0, S, +, × (and ≤ definable)

The seven axioms: Q1. S(x) ≠ 0 Q2. S(x) = S(y) → x = y Q3. x ≠ 0 → ∃y (x = S(y)) Q4. x + 0 = x Q5. x + S(y) = S(x + y) Q6. x × 0 = 0 Q7. x × S(y) = (x × y) + x Finitely axiomatized. No induction, in any form.

What fails: Q ⊬ ∀x (0 + x = x) Q ⊬ ∀x∀y (x + y = y + x) Q ⊬ ∀x (x ≠ S(x)) Non-standard models with visible pathologies: an element z with z + 1 = z is consistent with Q.

What holds — the two properties Q exists for: Σ₁-completeness: every true Σ₁ sentence is provable in Q. Representability: every computable function is representable in Q.

Essential undecidability (Robinson 1950): Q is undecidable, and so is every consistent extension of it — including complete ones. Hence: any theory interpreting Q is undecidable. This is the standard method: to show T undecidable, interpret Q in T.

Consequences by interpretation: Group theory, ring theory, lattice theory, ZF, and the theory of two equivalence relations are undecidable, each by interpreting Q.

Incompleteness: Gödel's first theorem holds for every consistent, effectively axiomatized extension of Q. The theorem needs Σ₁-completeness and representability, and Q has both — so PA's induction is not what makes it incomplete.

Symbols.

Metatheory. Q's importance is entirely instrumental and entirely disproportionate to its strength. What it locates is which properties incompleteness needs — not induction, not infinity, not any of the strength PA adds, but Σ₁-completeness together with representability, and Q has those with seven axioms and no schemas. It does not locate a minimum: R has those properties too and does not interpret Q, and there is no interpretability-minimal essentially undecidable theory (Pakhomov–Murwanashyaka–Visser 2022). What Q marks is a degree, occupied also by the concatenation theory TC and by adjunctive set theory. Essential undecidability makes it the interpretation target of choice, and the Tarski–Mostowski–Robinson method — undecidability by interpreting Q — is how most undecidability results in algebra were proved. Being finitely axiomatized is what makes the interpretations manageable, and it is also what separates Q from R: a finitely axiomatized consistent theory with no finite models cannot be interpreted in a locally finitely satisfiable one.

Applies to. Undecidability proofs by interpretation, across algebra, order theory, and set theory. The precise statement of Gödel's incompleteness hypotheses. Bounded arithmetic and weak fragments, where Q is the base. Any question of the form "how little arithmetic does this argument need".

Limitations. Q is not a theory anyone reasons in — it cannot prove commutativity of addition, and its models include structures with an element equal to its own successor's predecessor's successor in ways no one wants. Its interest is exhausted by the two theorems, and the axioms are chosen to make those theorems go through rather than because seven of anything is natural. Q is not sequential and is not finitely axiomatizable with full induction, so the elegant properties do not survive strengthening.

© 2026 Lingenic LLC