Relativity Theories (SpecRel, AccRel, GenRel)

Origin. The idea is old — Hilbert's sixth problem asked for the axiomatization of physics, and Reichenbach, Carnap, Gödel, Robb, and Suppes each attempted parts of it. The programme this entry describes is Hajnal Andréka, Judit Madarász, and István Németi's at the Rényi Institute from the late 1990s (On the Logical Structure of Relativity Theories, 2002, 1312 pp.), with Gergely Székely's thesis (2009) supplying the accelerated-observer analysis. Its ancestry runs through Tarski's elementary geometry, and directly: Tarski's 1959 paper appeared in a volume titled The Axiomatic Method, with Special Reference to Geometry and Physics.

Models. Special relativity as a first-order theory, with the same status as Peano arithmetic — a signature, a handful of axioms, classical consequence, and metatheory. Not a formalization exercise. The programme's claim is that the axioms can be made few enough and simple enough that a layperson checks them, and that every characteristic prediction then follows, so one can ask which axiom is responsible for which effect and delete axioms to find out. That question — why is there no faster-than-light travel, and from what — has an answer here and nowhere else.

Formalism.

Language: three sorts, four predicates. Sorts: B (bodies), Q (quantities). Unary on B: IOb (inertial observers), Ph (photons). Field operations on Q: +, ·, ≤. The worldview relation: W(m, b, x₁, x₂, x₃, x₄) — "observer m coordinatizes body b at spacetime point x̄". Everything else is defined. An event seen by m at x̄ is {b : W(m, b, x̄)}; the worldline of b according to m is {x̄ : W(m, b, x̄)}; the worldview transformation w_mk relates the coordinates m and k assign to the same event.

SpecRel := {AxField, AxSelf, AxPh, AxEv, AxSymDist}

AxField ⟨Q; +, ·, ≤⟩ is an ordered field. (Bookkeeping — the mathematical frame.) AxSelf Every inertial observer coordinatizes itself on the time axis: it is at x̄ iff its space component is ⟨0,0,0⟩. AxPh The speed of light is 1 for every inertial observer, and a photon can be sent in any direction. AxEv All inertial observers coordinatize the same set of events. AxSymDist Inertial observers agree on the spatial distance between two events if the events are simultaneous for both.

Four axioms with content, one auxiliary. AxSelf, AxPh, AxEv alone already prove the paradigmatic effects — moving clocks slow, moving rods contract, moving clock-pairs desynchronize.

The representation theorem: Let d ≥ 3. Assuming SpecRel, every worldview transformation w_mk is a Poincaré transformation. The proof: AxPh and AxEv make w_mk a bijection of Q^d preserving lines of slope 1; the Alexandrov–Zeeman theorem generalized to arbitrary fields makes any such bijection a Poincaré transformation composed with a dilation and a field-automorphism-induced map; AxSymDist forces both of those to be the identity. So the Lorentz group is not assumed. It is derived, from four sentences, and this is the theorem the axiomatization exists for — the same move as Tarski's geometry deriving its coordinate field.

What each axiom buys: AxSymDist ⟺ AxSymTime ⟺ "w_mk is a Poincaré transformation", over SpecRel₀ = {AxSelf₀, AxPh, AxEv}. NoFTL — no inertial observer moves faster than light — follows from SpecRel₀, so it does not need the symmetry axiom. The independence of each axiom is proved by exhibiting models, which is the reason for having several competing axiom systems rather than one.

AccRel := SpecRel + AxCmv + IND AxCmv Every accelerated observer has, at every moment, a co-moving inertial observer. IND Induction for FOL-definable subsets of Q — a schema, imported from real analysis.

The twin paradox needs IND (Madarász–Németi–Székely). SpecRel is complete with respect to questions about inertial motion, and cannot settle accelerated clocks. Adding IND settles them. That is a reverse-mathematics result about a physical theorem: the twin paradox is equivalent, over the base, to an induction principle — and identifying which mathematical principle a physical prediction consumes is what a first-order axiomatization is for.

GenRel: obtained from SpecRel in two steps by relativizing the axioms so they no longer mention inertial observers, replacing AxCmv with differentiability: GenRel^n := {AxSelf⁻, AxPh⁻, AxEv⁻, AxSymDist⁻, AxDiff_n} ∪ CONT finitely axiomatized for each n, with a smooth version and a continuity schema CONT.

Metatheoretic results (Andréka–Madarász–Németi): SpecRel is undecidable. It has natural extensions, some decidable, others to which the full strength of both incompleteness theorems applies. SpecRel⁺ is hereditarily undecidable, formalizes its own consistency, and that sentence is neither provable nor refutable in it. SpecRel is consistent over ℚ (Székely): the theory holds with the rationals as the quantity field, so no completeness or Archimedean property is needed — relativity does not require the reals.

Symbols.

Metatheory. Two results carry the entry. First, SpecRel derives the Poincaré transformations from four axioms via Alexandrov–Zeeman — the axioms determine the transformation group exactly as Tarski's geometric axioms determine the coordinate field, and it is the same theorem shape in a different subject. Second, the twin paradox is unprovable in SpecRel and provable in SpecRel + IND, which converts "what does relativity assume" from a philosophical question into a conservativity question with an answer. The incompleteness results are the third thing worth having: SpecRel is undecidable, some extensions are decidable and others are hereditarily undecidable with Gödel's theorems applying in full, so a physical theory sits in the same landscape as an arithmetical one and can be located in it. Placement follows the division's boundary clause — the bare axiomatization belongs here; Applications, which holds theories used to model a domain, has no physics subdivision to cross-list to, so nothing is cross-listed.

Applies to. The logical foundations of spacetime theories — the question of which axiom yields which prediction, answered by deleting axioms and checking models. Comparison of theories: Lefever and Székely's first-order comparison of classical and relativistic kinematics, and definitional-equivalence questions between formulations of the same physics. Reverse mathematics outside mathematics, via IND and the twin paradox. Philosophy of physics, where theoretical equivalence is the live question and this is the only apparatus that states it precisely. Hilbert's sixth problem, as the one serious extant attempt on relativity's part of it.

Limitations. The theory is undecidable, so the axiomatization buys explanation rather than computation. It is relativity's kinematics: dynamics requires further axioms (mass, four-momentum conservation), and the extensions proposed for them — SpecRel⁺ and its relatives — are not standardized, so results must be checked against which system is meant. Several competing axiom systems exist by design, which is a methodological virtue for the independence analysis and a hazard for citation. The quantum theories have no comparable programme, and GenRel's axiomatizations are much less settled than SpecRel's. Whether an FOL axiomatization of a physical theory captures the physics or only a model class of it is exactly the theoretical-equivalence question the programme is used to study, so it cannot be answered from inside.

© 2026 Lingenic LLC