VR. A Formal System: A Minimalist Axiomatization of Arithmetic Grounded in Leibnizian Void

We present a formal axiomatic system VR with three primitives {∅, →, t} and four axioms. The von Neumann natural numbers are constructed as the unfolding of the succession operator t from the initial void ∅. Equality and distinctness are defined via Leibniz's principle and are not among the primitives. We show that VR is arithmetically equivalent to Peano arithmetic (PA), from which the consistency of VR relative to ZF set theory follows. The main content of VR is not the novelty of arithmetical results (it is equivalent to PA), but the compactness and minimalism of its axiomatization with a transparent motivation for its primitives: ∅ as Leibnizian initial givenness, → as the minimal logical operator, and t as the generative operator of counting. All standard properties of the natural numbers are obtained from these three primitives and four axioms.Version 1.0.1 (2026) adds three editorial notes reflecting the Lean 4 formalisation of Part I (companion publication, Zenodo DOI 10.5281/zenodo.20324240) without altering any axiom, definition, or theorem.