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 mark ∅ (the first distinction). 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. Keywords: axiomatic arithmetic, foundations of mathematics, Leibnizian equality, von Neumann ordinals, Peano arithmetic, consistency. Version 1. 0. 2 (2026) reframes the ontology of the empty set — from the Leibnizian void to Spencer-Brown's mark (the first distinction: ∅ = as a boundary drawn around nothing, an operational act). The base constructor is renamed void → mark in the companion Lean 4 formalisation. No axiom, definition, or theorem is altered. Version 1. 0. 1 (2026) adds three editorial notes reflecting the Lean 4 formalisation of Part I, published as a separate companion work (Reznik, 2026; Zenodo DOI 10. 5281/zenodo. 20324240). The notes do not alter any axiom, definition, or theorem; they record points of methodological clarification that became visible only through formalisation. See the closing Part IV.
Vitaly Reznik (2026) studied this question.