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 nullary base operation. 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. 3 (2026 — no ontology of the empty set (∅ as a nullary operation; only operations) ; supersedes the brief Spencer-Brown reframing of v1. 0. 2 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 (Reznik, 2026; Zenodo DOI 10. 5281/zenodo. 20324240). The notes do not alter any axiom, definition, or theorem.
Vitaly Reznik (2026) studied this question.