VR. A Formal System: An Axiom-Free Reconstruction of Arithmetic from Operations Alone

A formal system VR generated by two primitive operations — the nullary base ∅ and the unary succession t. VR posits no axioms of its own: membership ∈ is defined by recursion on t, the succession principle A3 is a theorem, and induction A4 is the recursor of the inductive term-algebra. The von Neumann natural numbers are the unfolding of t from ∅; equality is Leibnizian and coincides with structural term-identity by a theorem. VR is arithmetically equivalent to first-order Peano arithmetic (under the schematic reading of the Leibnizian quantifier), whence consistency relative to ZF follows as a metatheoretic corollary. "Axiom-free" is exact in the Lean 4 companion: #print axioms reports the empty profile [ ] (no propext, Classical.choice, or Quot.sound) for every object of Part I. Version 1.1.1 removes the former third "primitive" — a propositional implication → on a two-valued type. It was load-bearing for no VR theorem (the Lean companion confirms the entire arithmetic — membership, the von Neumann numbers, +, ×, ^, and the PA-equivalence — references it nowhere), and it was not logic in any inferential sense: a truth-function on a two-element type is the semantic Boolean algebra of propositional logic, not the logic itself (no consequence relation, no derivability, no completeness). VR therefore neither needs nor generates a logic of its own; the logic it reasons with is metatheoretic, borrowed from the ambient framework. At this layer VR is pure arithmetic on {∅, t}, equivalent to first-order PA. The arithmetic content is unchanged from v1.1.0; this version removes a non-load-bearing appendage and the over-claim that VR founds its own propositional logic. First/foundational work of the VR Cycle; Lean 4 companion module VRCycle.VR (Zenodo DOI 10.5281/zenodo.20324240). Prepared with the assistance of Claude (Anthropic, Opus 4.8) in the cycle's Variant A architecture; all mathematical content, definitions, theorems and positions are due to the author, Vitaly Reznik.