14 Operational set universe (Brouwer path)
14.1 Position
This chapter is the Brouwer rebuild of VR-Sets (preprint v1.0.3): the operational universe of sets, built from scratch below the Classical.choice floor, and the correction of the earlier §VI. Versions through 1.0.2 realised the ZFC axioms over mathlib’s classical ZFSet (Chapter 4) and argued that the operational universe is countable, whence the Axiom of Choice is free and Banach–Tarski cannot arise. That reading is Bishop’s, and it contradicts the operational continuum (Chapter 13), which took the Brouwer path. Here the universe of sets is rebuilt on that same path and the cardinality core is corrected: the universe as becoming is non-enumerable (choice-free), while only the describable register is countable.
The carrier deliberately avoids mathlib’s coinductive machinery (PFunctor.M of Chapter 5), which is irreducibly Tier-3 even at its destructor. The Lean 4 formalisation lives self-contained under VR/SetsOp/ (Pointed, Builder, Closure, Omega, Extensionality, Congruence, Becoming, Describable, Schemas, Grounded, Power). After the 2026-07-12 tier pass (Iff-rw replaced by combinators) every object is Axiom profile: [] — the empty axiom list — except the describable-register encoding flagged in §14.5.
14.2 The carrier: sets as revealing functionalities
An operational set is a pointed graph \((V, E, \mathit{pt})\): \(E\, a\, b\) reads “querying the functionality at \(b\) reveals \(a\) as a member”; \(\mathit{pt}\) is the set itself; \(x.\mathrm{child}\, a := (V,E,a)\) is the member sitting at \(a\). Identity is supplied operationally and no quotient is taken.
OpSet is the pointed graph; \(x \approx y\) (OpSet.Equiv) holds when a bisimulation relates their points; \(z \in x\) (OpSet.Mem) when some member-vertex of \(x\) is \(\approx \) to \(z\).
Equiv.refl/symm/trans — each Axiom profile: [] (axiom-free).
Turning “bisimilar” into a type-level equality (forming the quotient) requires Skolemising the existential matches of the bisimulation into functions; that is exactly VR’s \(T\! \to \! O\) asymmetry (Chapter 6), and it is where mathlib’s coinductive layer invokes Classical.choice. We therefore keep identity as a relation carried with its witness — a performed bisimulation, “doing not being” made into the construction — which is why the development stays below the floor.
Membership respects identity (mem_congr, Axiom profile: []), and \(x \approx y \iff \forall z,\ (z\in x \leftrightarrow z\in y)\) (equiv_iff_same_mem; backward direction ext). Both Axiom profile: []. The backward direction is the coinductive content (a bisimulation is built from the member-matching); it is AFA-style strong extensionality, kept choice-free precisely because identity was never quotiented. This licenses \(\approx \) as a faithful equality of sets.
14.3 Operations
All operations instantiate one constructor: \(\mathrm{sup}\, c\), the set whose members are exactly the family \(c\).
\(z \in \mathrm{sup}\, c \iff \exists i,\ z \approx c\, i\) (mem_sup, Axiom profile: []).
From mem_sup: \(\varnothing \) (emptySup, \(z\notin \varnothing \)), singleton (\(z\in \{ a\} \iff z\approx a\)), pair (\(z\in \{ a,b\} \iff z\approx a\vee z\approx b\)), union (\(z\in \bigcup x\iff \exists y,\ y\in x\wedge z\in y\)), and successor \(\mathrm{succ}\, a := a\cup \{ a\} \) (\(z\in \mathrm{succ}\, a\iff z\in a\vee z\approx a\)). Each Axiom profile: []. The operations respect \(\approx \) (*_congr, via Theorem 344).
The von Neumann naturals \(\mathrm{vn}\) and \(\omega := \mathrm{sup}\, \mathrm{vn}\): the members of \(\omega \) are exactly the \(\mathrm{vn}\, n\) up to \(\approx \); \(\varnothing \in \omega \); and \(\omega \) is closed under successor for any member (omega_succ_closed). All Axiom profile: [].
For a species \(p\) respecting \(\approx \), \(z\in \{ z\in x\mid p\, z\} \iff z\in x\wedge p\, z\) (mem_sep). For a rule \(F\) respecting \(\approx \), \(w\in \{ F\, z\mid z\in x\} \iff \exists z,\ z\in x\wedge w\approx F\, z\) (mem_repl). No decidability is needed; both Axiom profile: [].
\(\wp \, x := \mathrm{sup}\) over the vertex-predicates \(s : x.V \to \mathrm{Prop}\) (subsetOf \(x\, s\) keeps the member-vertices in \(s\)), with \(z \in \wp \, x \iff z \subseteq x\) (mem_powerset); the backward direction selects \(s\, a :=\) “\(a\) is a member-vertex whose member lies in \(z\)” and closes by strong extensionality (Theorem 344). Axiom profile: [] — axiom-free. But see Finding 350: the construction is below the choice floor yet impredicative. With it, OpSet verifies every ZF\(^-\) axiom (Extensionality, \(\varnothing \), Pairing, Union, Power, Separation, Replacement, Infinity) choice-free; Foundation is the predicate IsGrounded (§14.4).
A completed power set \(\wp \, x\) is constructible choice-free (Theorem 349); in particular \(\wp \, \omega \) exists as a set with \(z\in \wp \, \omega \iff z\subseteq \omega \). What this costs is not Classical.choice — the axiom audit reports the empty list — but impredicativity: the index \(x.V\to \mathrm{Prop}\) is the full power of the representative’s vertex type, a move legitimate in Lean’s impredicative Prop but outside a predicative (Brouwer / Martin-Löf) discipline, and one that #print axioms cannot detect. The operational register’s relation to power set is therefore sharper than “absent”: the predicative content of \(\wp \, \omega \) is the becoming (Theorem 354, the diagonal), while the impredicative completed \(\wp \, \omega \) also exists, choice-free, at the cost named here — isolating the obstruction as impredicativity, not choice.
14.4 Foundation is a predicate, not a choice
Classical set theory must decide, at the axiom level, whether \(\in \)-descent always terminates (Foundation) or may cycle (Aczel’s AFA, Chapter 5). VR is not forced to: well-foundedness is a property of a set’s graph, observed not postulated.
IsGrounded \(x := \mathrm{Acc}\, (E)\, x.\mathit{pt}\). Accessibility transports along a bisimulation (acc_bisim), so \(x\approx y\Rightarrow (\, x\) grounded \(\iff y\) grounded\()\) (isGrounded_iff); and a member of a grounded set is grounded (mem_grounded). All Axiom profile: []. Hence “well-founded / ZFC-mode” is a well-defined hereditary property of sets, not of graphs.
The ZFC fragment is the grounded sets (\(\varnothing \) grounded; the von Neumann naturals are \(\in \)-acyclic, vn_not_self_mem, by strong induction). The Quine atom \(A=\{ A\} \) (quine) is a genuine operational set with \(A\in A\) (quine_self_mem) and is not grounded (quine_not_grounded) — no anti-foundation axiom invoked, the graph simply has a cycle. VR thus holds ZFC and ZFA natively, as fragments of one universe under a uniform (bisimulation) identity, and faces neither Foundation nor AFA as a postulate. All Axiom profile: [].
Because membership is the edge relation and a member is the same graph re-pointed (child), nesting — including self-membership — is native, and Aczel’s decoration is almost definitional. Every graph \((V,E)\) has a decoration \(\texttt{decorate}\, E\, v:=(V,E,v)\) (decorate_isDecoration, by rfl — membership is the decoration condition), unique up to \(\approx \) (decoration_unique; for each \(v\) the choice-free exhibited bisimulation \(R_v\, a\, w := (d\, v).\texttt{child}\, a \approx d\, w\)). Axiom profile: [] — fully axiom-free.
Cost of the quotient (bridge to Chapter 5). VR-Sets-ZFA obtains the same content on mathlib’s M-types by quotienting; there AFA is Axiom profile: [propext, Classical.choice, Quot.sound] — forming the quotient Skolemises the bisimulation’s witnesses (transit asymmetry, Theorem 344 ff.) and uniqueness selects representatives by Classical.choice through the choice-pulling PFunctor.M.dest. The relational identity is axiom-free precisely where its quotient sits at the full ceiling. We read the two works together as \(\mathrm{OSetZFA}\simeq \texttt{OpSet}/\! \approx \) (this version the choice-free floor of which VR-Sets-ZFA is the quotient) — a prose-level reading, not yet machine-checked (in the modality of Conjecture IV.2); its formalisation (a Bridge file: M.corec unfolding, descent through the quotient, bijectivity on \(\approx \)-classes) is a candidate for VR-Sets-ZFA v1.1.
14.5 Cardinality, the diagonal, and choice — the corrected core
No \(\mathbb {N}\)-indexed enumeration is surjective up to \(\approx \): \(\lnot \, \exists e:\mathbb {N}\to \texttt{OpSet},\ \forall x,\ \exists n,\ e\, n\approx x\) (universe_not_enumerable, Axiom profile: [] — axiom-free). The proof is a self-contained Cantor diagonal inside the universe: the diagonal set \(D := \{ \mathrm{vn}\, n \mid \mathrm{vn}\, n\notin e\, n\} \) (a sup over a subtype, no decidability) satisfies, by the distinctness of the naturals (vn_inj, Axiom profile: []), \(\mathrm{vn}\, k\in D\iff \mathrm{vn}\, k\notin e\, k\); were \(e\) surjective, some \(e\, m\approx D\) forces \(\mathrm{vn}\, m\in e\, m\iff \mathrm{vn}\, m\notin e\, m\). This is the Brouwerian content: the diagonal works, cutting done from becoming; the universe is genuinely uncountable, choice-free.
A finite description syntax Desc (\(\varnothing \), pair, union, \(\omega \)) with interpretation eval gives “describable” sets; an exhibited \(\mathbb {N}\)-enumeration (descEnum) reaches every describable set up to \(\approx \) (describable_countable).
Theorem 355 is the only Tier-3 object, depending on Classical.choice, and the dependence is borrowed: it enters solely through mathlib’s pairing inversion (Nat.unpair_pair / Nat.pair_eq_pair are both Axiom profile: [propext, Classical.choice, Quot.sound]; Nat.pair itself is Axiom profile: []). The fact is constructively true; mathlib proves it with incidental choice. The countability of a register of descriptions is in any case formal-register meta-accounting, where classical reasoning is admitted with its cost made visible. Kept and documented (decision A).
Theorems 354 and 355 together are the corrected §VI: the describable (done) register is countable, the universe (becoming) is not. Consequently the Axiom of Choice is not an operational theorem. Dependent choice is operational (Theorem 341); full AC is a formal-register label with no operational correlate. Banach–Tarski is a \(T\! \to \! T\) phenomenon of the full-AC context — a completed uncountable totality plus selection by full AC, neither with an operational correlate — which by conservativity (Chapter 6) never transits to the operational register: its absence operationally is a conservativity phenomenon, not a cardinality accident.
14.6 Honest scope
Below the floor by construction. “Choice-free” is a statement about audited axiom dependencies, exhibited build-time; Lean’s ambient logic remains classical. Two reals. The operational reals (becoming, Chapter 13) and \(\mathbb {R}_{\mathrm{VR}}\cong \mathbb {R}\) (uncountable, Chapter 3) are distinct objects; this chapter commits the set universe to the Brouwer reading. Power set is impredicative, not choice-laden. A completed power set \(\wp \, x\) is constructible choice-free (Theorem 349), but only impredicatively (Finding 350); the predicative content of \(\wp (\omega )\) is the becoming, Theorem 354. The earlier version stands as the classical-surrogate presentation (Chapter 4); only its §VI cardinality reading is superseded here.