5 VR-Sets-ZFA
5.1 Position
VR-Sets-ZFA extends VR-Sets with a coinductive universe that admits non-well-founded sets and proves Aczel’s Anti-Foundation Axiom (AFA) as a theorem. The chapter constructively resolves Conjecture IV.2 from Chapter 4: the required type \(U\) satisfying AFA with extensional membership exists and is machine-verified.
Architectural fact. The construction is built on mathlib’s PFunctor.M (Avigad–Carneiro–Hudon 2019), the greatest fixpoint of the pre-set functor. CoPSet is the coinductive counterpart of mathlib’s inductive PSet: both use branching type \((\alpha : \mathrm{Type}\, u,\, A : \alpha \to \cdot )\); the difference is the generation principle (greatest vs. least fixpoint). OSetZFA is the quotient of CoPSet by extensional cobisimulation, the coinductive analogue of OSet = ZFSet = Quotient PSet.setoid.
AFA follows from the universal property of the final coalgebra: every directed graph has a unique decoration, proved by CoPSet.corec (existence) and CoPSet.bisim_imp_Equiv (uniqueness). No coinductive axiom is added; the result lies entirely within [propext, Classical.choice, Quot.sound].
5.2 Architecture (Part II)
\(\texttt{CoPSetFunctor} : \texttt{PFunctor}\) with shape type \(\texttt{A} := \mathrm{Type}\, u\) and branching \(\texttt{B} := \mathrm{id}\). \(\texttt{CoPSet}.{u} := \texttt{PFunctor.M CoPSetFunctor}.{u}\) (greatest fixpoint of CoPSetFunctor). Elements of CoPSet are potentially infinite or cyclic trees; in contrast, elements of PSet (inductive, mathlib) are always well-founded. Universe: CoPSet.u : Type (u+1).
\(\texttt{CoPSet.dest}(x) := \texttt{PFunctor.M.dest}(x) : \Sigma \, \alpha : \mathrm{Type}\, u,\; \alpha \to \texttt{CoPSet}\). Shape \(:= (-).\texttt{dest}.1\); children \(:= (-).\texttt{dest}.2\). Constructor: \(\texttt{CoPSet.mk}(\alpha , A) := \texttt{PFunctor.M.mk}\, \langle \alpha , A\rangle \). Roundtrip: dest_mk and mk_dest hold by rfl.
For any type \(X\) and coalgebra \(f : X \to \texttt{CoPSetFunctor}\, X\), \(\texttt{CoPSet.corec}(f) : X \to \texttt{CoPSet}\) is the unique coalgebra morphism into the final coalgebra. Computation rule: \(\texttt{dest}(\texttt{corec}(f)(x)) = f(x)[\texttt{corec}(f)]\) — proved by rfl (definitional, not axiomatic). This is the existence half of AFA.
\(\texttt{CoPSet.isBisim}(R)\): a relation \(R\) is a bisimulation when for every \((c, d) \in R\), the shapes of \(c\) and \(d\) are in bijection carrying \(R\)-related children to \(R\)-related children. \(\texttt{CoPSet.Equiv}(x, y) := \exists R,\; \texttt{isBisim}(R) \land R\, x\, y\) (greatest bisimulation; reflexive, symmetric, transitive). Key: \(\texttt{bisim\_ imp\_ Equiv}\) — if \(R\) is a bisimulation and \(R\, x\, y\), then \(\texttt{Equiv}\, x\, y\). This is the uniqueness half of AFA. CoPSet.instSetoid packages Equiv as a Lean setoid.
\(\texttt{OSetZFA} := \texttt{Quotient CoPSet.instSetoid}\) (cobisimulation quotient of CoPSet). \(\texttt{OSetZFA.mk}(x) := \llbracket x \rrbracket \) (quotient constructor). \(\texttt{sound}\): \(x \approx y \Rightarrow \texttt{mk}(x) = \texttt{mk}(y)\). \(\texttt{exact}\): \(\texttt{mk}(x) = \texttt{mk}(y) \Rightarrow x \approx y\). \(\texttt{mk\_ surjective}\): every element of OSetZFA has a CoPSet representative.
\(\texttt{CoPSet.mem}(x, y) := \exists \, i : y.\texttt{shape},\; x \approx y.\texttt{children}(i)\). Lifted to \(\texttt{OSetZFA.Mem}\) via OSetZFA.lift; well-definedness by CoPSet.mem_congr. mem_mk: \(a \in \llbracket b \rrbracket \leftrightarrow \exists \, i : b.\texttt{shape},\; a = \llbracket b.\texttt{children}(i) \rrbracket \). Extensionality: \(\llbracket x \rrbracket = \llbracket y \rrbracket \leftrightarrow \forall z,\; z \in \llbracket x \rrbracket \leftrightarrow z \in \llbracket y \rrbracket \).
5.3 AFA as theorem (Part III)
\(\texttt{isDecoration}(E, f) := \forall v : V,\; \forall x : \mathrm{OSetZFA},\; x \in f(v) \leftrightarrow \exists \, w : V,\; E\, v\, w \land x = f(w)\). \(\texttt{graphCoalg}(E)(v) := \langle \{ w \mid E\, v\, w\} , \texttt{Subtype.val}\rangle \in \texttt{CoPSetFunctor}\, V\) (the out-neighbourhood coalgebra for vertex \(v\)).
\(\texttt{graphCoPSet}(E) := \texttt{CoPSet.corec}(\texttt{graphCoalg}(E)) : V \to \texttt{CoPSet}\) (the unique coalgebra morphism from \((V, \texttt{graphCoalg}(E))\) to \((\texttt{CoPSet}, \texttt{CoPSet.dest})\)). Computation: \(\texttt{dest}(\texttt{graphCoPSet}(E)(v)) = \langle \{ w \mid E\, v\, w\} ,\; w \mapsto \texttt{graphCoPSet}(E)(w)\rangle \) (graphCoPSet_dest by rfl). \(\texttt{graphDecoration}(E)(v) := \llbracket \texttt{graphCoPSet}(E)(v)\rrbracket : \mathrm{OSetZFA}\).
graphDecoration_isDecoration: \(\texttt{graphDecoration}(E)\) is a decoration of \((V, E)\). Proof: unfold via mem_mk and graphCoPSet_dest; the shape is definitionally \(\{ w \mid E\, v\, w\} \); OSetZFA.sound and OSetZFA.exact close the iff.
graphDecoration_unique: if \(f\) is any decoration of \((V, E)\), then \(f = \texttt{graphDecoration}(E)\). Proof by coinductive bisimulation at CoPSet-level: choose Classical.choice representatives \(\texttt{fRep}(v)\) for each \(f(v)\); define \(R(c, d) := \exists \, v,\; c \approx \texttt{fRep}(v) \land d \approx \texttt{graphCoPSet}(E)(v)\); show \(R\) is a bisimulation by tracing decoration conditions; apply CoPSet.bisim_imp_Equiv to get \(\texttt{fRep}(v) \approx \texttt{graphCoPSet}(E)(v)\); conclude \(f(v) = \texttt{graphDecoration}(E)(v)\).
Direct induction is impossible (graphs may be non-well-founded); PFunctor.M.corec_unique is not applicable (it requires exact coalgebra equality, not cobisimulation).
\(\forall (V : \mathrm{Type})\; (E : V \to V \to \mathrm{Prop}),\; \exists !\, f : V \to \mathrm{OSetZFA},\; \texttt{isDecoration}(E, f)\).
AFA is a theorem in OSetZFA, not an axiom. It follows from: existence \(=\) graphDecoration_isDecoration; uniqueness \(=\) graphDecoration_unique; assembled as ExistsUnique.intro.
Axiom profile: [propext, Classical.choice, Quot.sound]. No new axioms beyond the standard mathlib ceiling.
5.4 Embedding \(\mathrm{OSet} \hookrightarrow \mathrm{OSetZFA}\) (Part IV)
\(\texttt{embedPSet} : \texttt{PSet} \to \texttt{CoPSet}\) by structural recursion: \(\texttt{embedPSet}(\texttt{mk}(\alpha , A)) := \texttt{CoPSet.mk}(\alpha ,\; i \mapsto \texttt{embedPSet}(A(i)))\). Computation: embedPSet_dest by rfl.
Forward: \(\texttt{embedPSet\_ congr}\): \(\texttt{PSet.Equiv}\, x\, y \Rightarrow \texttt{CoPSet.Equiv}(\texttt{embedPSet}(x), \texttt{embedPSet}(y))\). Proved by coinductive bisimulation (no induction on PSet needed).
Backward: \(\texttt{embedPSet\_ faithful}\): \(\texttt{CoPSet.Equiv}(\texttt{embedPSet}(x), \texttt{embedPSet}(y)) \Rightarrow \texttt{PSet.Equiv}\, x\, y\). Proved by structural induction on PSet (uses well-foundedness).
\(\texttt{embedOSet} := \texttt{Quotient.lift}(\texttt{OSetZFA.mk} \circ \texttt{embedPSet}) : \mathrm{OSet} \to \mathrm{OSetZFA}\) (noncomputable). \(\texttt{embedOSet\_ mk}(p) : \texttt{embedOSet}(\llbracket p \rrbracket ) = \llbracket \texttt{embedPSet}(p)\rrbracket \) by rfl.
\(\texttt{embedOSet\_ injective}\): \(\texttt{Function.Injective}(\texttt{embedOSet})\). Proof: \(\texttt{embedOSet}(x) = \texttt{embedOSet}(y) \Rightarrow \texttt{embedPSet}(x') \approx \texttt{embedPSet}(y')\) (by OSetZFA.exact) \(\Rightarrow \texttt{PSet.Equiv}\, x'\, y'\) (by embedPSet_faithful) \(\Rightarrow x = y\) (by quotient injectivity).
\(\texttt{embedOSet\_ mem}\): \(\texttt{embedOSet}(x) \in \texttt{embedOSet}(a) \leftrightarrow x \in a\) (membership preserved in both directions).
5.5 Demonstrations (Part V)
\(\texttt{quineAtom} := \texttt{graphDecoration}(\lambda \, \_ \, \_ ,\; \top )(()) : \mathrm{OSetZFA}.{0}\) — decoration of the one-vertex self-loop \((V = \texttt{Unit},\; E\, \_ \, \_ = \top )\).
\(\texttt{omegaChain} := \texttt{graphDecoration}((n, m) \mapsto m = n+1) : \mathbb {N} \to \mathrm{OSetZFA}.{0}\) — decoration of the forward-chain graph.
\(\texttt{quineAtom\_ mem\_ iff}(z)\): \(z \in \texttt{quineAtom} \leftrightarrow z = \texttt{quineAtom}\) (the atom contains exactly itself). Proof via graphDecoration_isDecoration at \(() : \texttt{Unit}\): existential over Unit forces \(w = ()\).
\(\texttt{quineAtom\_ self\_ mem} : \texttt{quineAtom} \in \texttt{quineAtom}\). Proof: quineAtom_mem_iff quineAtom and rfl.
\(\texttt{cycleDecoration} := \texttt{graphDecoration}(x, y \mapsto x \ne y) : \texttt{Bool} \to \mathrm{OSetZFA}.{0}\) — decoration of the two-vertex mutual-edge graph.
\(\texttt{cycleDecoration\_ eq\_ quineAtom}(b)\): both nodes of the two-cycle equal the Quine atom. Proof by bisimulation: \(R := \{ (\texttt{cycleA}, \texttt{quineA}), (\texttt{cycleB}, \texttt{quineA})\} \) where \(\texttt{cycleA/B}\) are the two CoPSet nodes and \(\texttt{quineA}\) is the Quine atom’s CoPSet representative. \(R\) is a bisimulation because each cycle-node has exactly one child (the other node) and the Quine-node has exactly one child (itself); CoPSet.bisim_imp_Equiv closes.
This is the bisimulation collapse theorem: different-looking APGs produce the same OSetZFA element when cobisimilar.
\(\lnot \, \texttt{WellFounded}({\cdot } \in {\cdot } : \mathrm{OSetZFA} \to \mathrm{OSetZFA} \to \mathrm{Prop})\). Proof: accessibility implies irreflexivity (acc_irrefl); if membership were well-founded, \(\texttt{quineAtom}\) would be accessible, hence \(\texttt{quineAtom} \notin \texttt{quineAtom}\); contradicts quineAtom_self_mem.
\(\texttt{quineAtom} \notin \texttt{Set.range}(\texttt{embedOSet})\). Proof: suppose \(\texttt{embedOSet}(x) = \texttt{quineAtom}\); then \(x \in x\) (from \(\texttt{quineAtom\_ self\_ mem}\) and embedOSet_mem); but \(\texttt{ZFSet.mem\_ wf}\) gives \(x\) is accessible, hence \(x \notin x\) by acc_irrefl. Contradiction. This witnesses that \((\mathrm{OSet}, \in ) \subsetneq (\mathrm{OSetZFA}, \in )\).
\(\texttt{omegaChain\_ mem\_ iff}(n, z)\): \(z \in \texttt{omegaChain}(n) \leftrightarrow z = \texttt{omegaChain}(n+1)\) (each element contains exactly the next). \(\texttt{omegaChain\_ descent}(n)\): \(\texttt{omegaChain}(n+1) \in \texttt{omegaChain}(n)\).
The omega chain is an infinite \(\in \)-descending sequence without cycles: no element contains itself. This is a second, distinct mode of non-well-foundedness from quineAtom (self-membership vs. infinite descent without cycles).
\(\texttt{OSetZFA.empty}\): the empty element with no members. \(\texttt{OSetZFA.singleton}(x)\): the element containing exactly \(x\). \(\texttt{quineAtom\_ eq\_ singleton\_ self}\): \(\texttt{quineAtom} = \texttt{OSetZFA.singleton}(\texttt{quineAtom})\) — the Quine atom is its own singleton.
5.6 ZF\(^-\) axioms on \(\mathrm{OSetZFA}\) (Part VI)
The previous parts prove AFA and a strict \(\in \)-preserving embedding of the well-founded universe, but do not by themselves verify the ZF axioms on \(\mathrm{OSetZFA}\). This part does: Pairing, Union, Power, Separation, Replacement and Infinity hold on \(\mathrm{OSetZFA}\) as machine-checked theorems, so that — with Extensionality (Definition 133), the empty set (Definition 146), and Foundation supplied by AFA (Theorem 137) — \(\mathrm{OSetZFA}\) is a model of ZF\(^-\).
\(z \in \{ a,b\} \leftrightarrow z = a \vee z = b\) (mem_pair); \(z \in \bigcup x \leftrightarrow \exists y,\ y \in x \wedge z \in y\) (mem_sUnion); \(z \in \wp \, x \leftrightarrow z \subseteq x\) (mem_powerset). Each is built at the CoPSet level as a single \(\texttt{mk}\, \alpha \, A\) touching only the top branching levels (the coinductive structure affects only equality, supplied by isBisim_Equiv / bisim_imp_Equiv); the workhorse CoPSet.mk_equiv_of_coverage reduces each well-definedness obligation to a child-coverage check. In particular Power set is a verbatim PSet.powerset calque — no special difficulty from the coinductive quotient.
For a predicate \(p : \mathrm{OSetZFA} \to \mathrm{Prop}\), \(z \in \{ w \in x \mid p\, w\} \leftrightarrow z \in x \wedge p\, z\) (mem_sep). For a function \(F : \mathrm{OSetZFA} \to \mathrm{OSetZFA}\), \(z \in \{ F\, y \mid y \in x\} \leftrightarrow \exists y,\ y \in x \wedge F\, y = z\) (mem_image). Because \(p\) and \(F\) are first-class objects over the quotient, they are automatically \(\approx \)-invariant: the collapse of the first-order Separation / Replacement schemas into single quantified-over-an-object statements is here the operational reification of describability, not a generic type-theoretic accident.
With the von Neumann successor \(\mathrm{succ}\, x := \texttt{insert}\, x\, x = x\cup \{ x\} \) and \(\omega \) the set of von Neumann naturals: \(\varnothing \in \omega \) and \(\forall x,\ x \in \omega \to \mathrm{succ}\, x \in \omega \) (infinity); \(z \in \omega \leftrightarrow \exists n,\ z = \llbracket \texttt{ofNat}\, n\rrbracket \) (mem_omega). The naturals match VR’s \(O_n\) (Chapter 2) and mathlib’s ZFSet.omega.
With Extensionality, \(\varnothing \), Pairing, Union, Power, Separation, Replacement and Infinity verified, and Foundation supplied as AFA, every member of \(\mathrm{OSetZFA}\) obeys the ZF\(^-\) axioms as machine-checked theorems. This earns the reading of \(\mathrm{OSetZFA}\) as a ZFA universe: the strict embedding \((\mathrm{OSet},\in )\subsetneq (\mathrm{OSetZFA},\in )\) (Remark 157) is the inclusion of the grounded fragment. All witnesses sit at Axiom profile: [propext, Classical.choice, Quot.sound] — the M-type ceiling, inherited from PFunctor.M.dest (the destructor pulls Classical.choice), not from the set theory; the choice-free counterparts live on the pointed-graph carrier (Chapter 14, Theorem 349). Honest boundary: each axiom holds in \(\mathrm{OSetZFA}\) as a theorem; \(\mathrm{OSetZFA}\) is not itself given a first-order satisfaction relation — that “\(\models \) ZF\(^-\)” reading stays metatheory, as elsewhere in the cycle.
5.7 Conjecture IV.2 closed
Conjecture IV.2 from Chapter 4 (VR.Sets.Conjecture_IV_2_Statement) is resolved by this chapter: the type \(U := \mathrm{OSetZFA}\) with membership \(\mathrm{mem} := ({\cdot } \in {\cdot })\) witnesses the conjecture.
The three conjuncts of Conjecture_IV_2_Statement: (i) self-membered element: \(\texttt{quineAtom} \in \texttt{quineAtom}\) (quineAtom_self_mem); (ii) extensionality: OSetZFA.ext; (iii) classical AFA: AFA_in_OSetZFA.
The construction is constructive (no new axioms beyond the standard ceiling) and machine-verified. This is the completion of the three-chapter arc: Chapter 4 refutes AFA in PSet; this chapter proves AFA as a theorem in OSetZFA.
5.8 Methodological observations
PSet (inductive, mathlib) and CoPSet (greatest fixpoint of the same functor) are structurally dual: both have shape \((\alpha : \mathrm{Type}\, u,\; A : \alpha \to \cdot )\). The difference is generation principle: least fixpoint (PSet, well-founded by construction) vs. greatest fixpoint (CoPSet, admits cycles and infinite depth). The two-chapter arc (Ch. 4 refutes AFA in PSet; Ch. 5 proves AFA in OSetZFA) is the formal expression of this duality.
CoPSet.corec (existence) and CoPSet.bisim_imp_Equiv (uniqueness) together give AFA without any additional axiom. The key insight: a directed graph \((V, E)\) determines a coalgebra \(\texttt{graphCoalg}(E) : V \to \texttt{CoPSetFunctor}\, V\); the final coalgebra morphism is the decoration. This is Aczel’s AFA theorem reformulated as a property of the M-type, not postulated.
\(\texttt{OSetZFA} = \texttt{Quotient CoPSet.instSetoid}\) genuinely collapses non-equal CoPSets. Example: the self-loop CoPSet and one component of the two-cycle CoPSet are distinct as M-type elements but become the same element in OSetZFA (Theorem 142). The quotient is not a formality: different-shaped CoPSets can represent the same ZFA set. This parallels OSet = ZFSet = Quotient PSet.setoid where different PSet shapes collapse under bisimulation.
The self-loop APG (one vertex, self-edge) and the two-cycle APG (two vertices, mutual edges) are cobisimilar; their decorations in OSetZFA are equal. This is the correct behaviour of the extensional membership quotient: a ZFA set is determined by its membership graph up to bisimulation, not by syntactic representation.
Forward (embedPSet_congr: PSet.Equiv \(\Rightarrow \) CoPSet.Equiv): proved by coinductive bisimulation, no induction. Providing one bisimulation suffices. Backward (embedPSet_faithful: CoPSet.Equiv \(\Rightarrow \) PSet.Equiv): requires structural induction on PSet. PSet’s well-foundedness is used as a proof resource to descend through the coinductive equivalence. The asymmetry is structural: the forward direction is a coinductive free lunch; the backward direction pays the cost of well-foundedness.
\(\texttt{embedOSet}\) is injective (embedOSet_injective) but not surjective (quineAtom_not_in_range_embedOSet). The strict inclusion \((\mathrm{OSet}, \in ) \subsetneq (\mathrm{OSetZFA}, \in )\) is not merely asserted but machine-verified: the Quine atom is the explicit witness of surjectivity failure.
VR-Sets-ZFA provides two distinct witnesses of non-well-foundedness: (1) quineAtom: a cyclic set (\(q \in q\), self-membership); (2) omegaChain: an acyclic infinite descent (\(\texttt{omegaChain}(n+1) \in \texttt{omegaChain}(n)\) for all \(n\), no element is self-membered). Both are machine-verified.
5.9 Position relative to existing work (Part VII)
Aczel’s AFA (1988) is a classical axiom added to ZF. VR-Sets-ZFA proves AFA as a theorem of type theory via the M-type final coalgebra. The axiom content is absorbed into the inductive/coinductive infrastructure of Lean 4.
Paulson’s Isabelle/ZF formalises classical ZF via first-order axioms. AFA is not part of the standard Isabelle/ZF library. VR-Sets-ZFA provides AFA as a theorem in a type-theoretic framework without axiom extension.
Gylterud (2018) constructs sets in Homotopy Type Theory using HITs. VR-Sets-ZFA uses an M-type (greatest fixpoint) in plain dependent type theory (no univalence, no HITs). Both obtain AFA as a theorem; the route and the ambient type theory differ.
5.10 Axiom profile
Axiom profile: [] for 8 objects: pure structural definitions (CoPSetFunctor, projections, isDecoration, graphCoalg, CoPSet.isBisim, and analogues) that do not invoke quotients, ordinals, or classical selection.
Axiom profile: [propext, Classical.choice, Quot.sound] for the remaining objects, including all principal theorems: AFA_in_OSetZFA, quineAtom_self_mem, OSetZFA_mem_not_wf, quineAtom_not_in_range_embedOSet, embedOSet_injective, the ZF\(^-\) axiom-witnesses of §5.6 (mem_pair, mem_sUnion, mem_powerset, mem_sep, mem_image, infinity), and all construction theorems. The ceiling is the M-type substrate’s, not the set theory’s: every observation routes through PFunctor.M.dest, which is itself Tier-3 (the choice-free register is Chapter 14).
Zero sorry, zero admit, zero axioms beyond the standard mathlib ceiling. VR-Sets-ZFA is the largest module in the VR Cycle by line count (2109 lines) and the first to prove AFA as a theorem in the Lean 4 type-theoretic framework.
5.11 References
The preprint for this chapter is VR-Sets-ZFA, v1.0.0 (24 May 2026).
The Lean 4 formalisation is archived at VR-Sets-ZFA Lean, v1.0.0 (24 May 2026), git tag v1.5-vr-sets-zfa.