Building on VR (Reznik, 2026, DOI: 10. 5281/zenodo. 20212092) and VR-Numbers (Reznik, 2026, DOI: 10. 5281/zenodo. 20272743), we develop VR-Sets — an operational theory of sets that unifies ZFC and ZFA through reference semantics. A set is not a container with contents, but an operational functionality: a procedure that, upon a query, either reveals a specific element or reveals nothing. The membership relation x ∈ y is read as reference (the functionality y uses x in its description), not as physical containment. ∅ is not an ontological primitive but the empty functionality — a nullary operation carrying no ontological content, characterised solely by ∀x ¬ (x ∈ ∅) ; everything else arises as operational action upon it. There are only operations. The closure principle — every operationally describable functionality is a set — replaces the existence axioms of classical ZF and dissolves Russell's paradox operationally: paradoxical descriptions simply do not specify functionalities. All eight ZF axioms together with AC are derived as closure theorems of the operational universe (or follow from the definitions). The theory distinguishes two structural modes: the ZFC-mode (well-founded functionalities) and the ZFA-mode (admitting self-reference and cycles) ; both are legitimate, and the choice between them is an explicit foundational decision. The Quine atom A = A and other non-well-founded sets are first-class objects of the ZFA-mode. Three principal divergences from classical ZF emerge: ℘ (ω) is countable; the replacement schema collapses to a single theorem; foundation is mode-dependent. The VR numbers (von Neumann ordinals) of VR fall automatically into the ZFC-mode, and the entire arithmetic of VR and VR-Numbers is inherited without re-proof via the operational isomorphism. The whole operational universe is countable, which dissolves Cantor's diagonal argument operationally (the diagonal procedure does not specify a describable functionality), makes AC a theorem rather than an axiom, and excludes the Banach–Tarski paradox by construction. Tarski's theorem on the undefinability of truth is reformulated through the hierarchy of applications of the successor operator t. Part X (added in version 1. 0. 1) documents the Lean 4 formalisation of Parts II–V (Reznik 2026, Lean VR-Sets, DOI: 10. 5281/zenodo. 20354340), reporting ten methodological observations from the formalisation, centring on five structural boundaries between the operational universe and mathlib's type-theoretic infrastructure — the deepest of which is the constructive (axiom-free) absence of the ZFA-mode in mathlib's `PSet`. Version 1. 0. 2 (2026) reframes the philosophical presentation to a no-ontology position: ∅ is taken as a nullary operation carrying no ontological content, objects are operations (the cycle's slogan becomes "nothing is — all is doing"), and the ZFC/ZFA choice is recast as a foundational rather than ontological decision; no axiom, definition, or theorem is altered. (Version 1. 0. 1 added Part X — methodological observations from the Lean 4 formalisation of Parts II–V. )
Vitaly Reznik (Sat,) studied this question.