VR-Sets: An Operational Set Theory Unifying ZFC and ZFA through Reference Semantics

VR-Sets is the third work in the VR cycle, an operational theory of setsbuilt on the single ontological primitive ∅. A set is not a containerwith contents but an operational functionality — a procedure that, upona query, either reveals a specific element or reveals nothing. Themembership relation x ∈ y is read as reference (the functionality y usesx in its description), not as physical containment, which dissolves theintuitive paradoxes of self-reference at the ontological level. The closure principle — every operationally describable functionality isa set — replaces the existence axioms of classical ZF and dissolvesRussell's paradox: paradoxical descriptions simply do not specifyfunctionalities. All eight ZF axioms together with AC are derived asclosure theorems of the operational universe (or follow directly fromthe definitions). The theory distinguishes two structural modes: theZFC-mode (well-founded functionalities) and the ZFA-mode (admittingself-reference and cycles); both are legitimate, and the choice betweenthem is an explicit ontological decision rather than a mathematicalnecessity. The Quine atom A = {A} and other non-well-founded sets arefirst-class objects of the ZFA-mode. Three principal divergences from classical ZF emerge: ℘(ω) is countable;the replacement schema collapses to a single theorem; foundation ismode-dependent. The VR numbers (von Neumann ordinals) of the VR systemfall automatically into the ZFC-mode, and the entire arithmetic of VRand VR-Numbers is inherited without re-proof via the operationalisomorphism. The whole operational universe is countable, whichdissolves Cantor's diagonal argument operationally (the diagonalprocedure does not specify a describable functionality), makes AC atheorem rather than an axiom, and excludes the Banach–Tarski paradox byconstruction. Tarski's theorem on the undefinability of truth isreformulated through the hierarchy of applications of the successoroperator t. The philosophical position is operationalism: a coherentalternative to Platonism, formalism, constructivism, and structuralism,with its own ontological commitments and area of applicability. Changes in version 1.0.1. A new Part X has been added: "Lean 4 Formalisation of VR-Sets:Methodological Observations." This part documents the Lean 4formalisation of Parts II–V (Reznik 2026, Lean VR-Sets, Software DOI10.5281/zenodo.20354340; Git tag v1.2-vr-sets), reporting tenmethodological observations from the formalisation in four thematicgroups: quotient-base structure (Group A, two observations);five structural boundaries between the operational universe andmathlib's type-theoretic infrastructure (Group B, five observations,centring on the deepest finding — the constructive axiom-free absenceof the ZFA-mode in mathlib's PSet); axiom-minimal patterns (Group C,two observations on the four distinct sources of Classical.choiceand the axiom profiles of the two conjectures); methodologicalconvergences (Group D, two observations on schema-to-theorem unificationand the three-tier formalisation result). Part X resolves §IX.1 Question 3 of the preprint (machine formalisation)for Parts II–V. The Lean formalisation contains 22 public theoremsacross six files, with no sorry, no admit, all axiom-dependencies sittingat the standard ceiling [propext, Classical.choice, Quot.sound]; fourobjects achieve the empty axiom profile (no axioms at all), a tighterresult than VR-Numbers, where no object was axiom-free. The methodologicalobservations are also accessible through the source comments of theformalisation itself. Other changes: §I.7 (Structure of the preprint) updated to list tenparts instead of nine, with the description of Part X added.References updated with the new Lean VR-Sets entry. Acknowledgement ofAI assistance expanded to describe the parent-child review architecture(Opus 4.7 reviewer, Sonnet 4.6 in Claude Code writing Lean code) usedfor the formalisation. No mathematical content of Parts I–IX has been revised; the changes areadditive (Part X is new) and editorial. Companion preprint: VR-Numbers v1.0.2 (DOI 10.5281/zenodo.20352239),which similarly documents the Lean 4 formalisation of itsmathematical core in §VIII.