Corson's ordered-rational permutation model

Work internally in a model $M$ of $\mathrm{Z}\mathrm{F}\mathrm{A}+\mathrm{A}\mathrm{C}$ with an internally countably infinite set $A$ of all its atoms (ZFA universes, atoms, pure sets, and the kernel, The Axiom of Choice); no external well-foundedness or transitivity of $M$ is assumed. Every structure, group, support and hereditarily symmetric set below is computed in $M$. Equip $A$, using an internal enumeration, with a copy of the rational ordered Urysohn metric space $U_{\mathbb{Q}}^{<}$: the countable metric space with rational distances which is universal and homogeneous for finite ordered rational metric spaces, and let $G:=\mathrm{Aut}(U_{\mathbb{Q}}^{<})$ be the group of its order-and-metric automorphisms. The finite-support filter is generated by the pointwise stabilisers $\mathrm{fix}(e)$ of finite $e\subseteq A$ (Permutation groups, stabilizers, supports, and normal filters), and Corson's permutation model is the hereditarily symmetric interpretation of Symmetric and hereditarily symmetric sets for that filter; it is a ZFA model with the same atoms and kernel by the internal argument below. The transitive-ground special case is Fraenkel–Mostowski permutation-model theorem. Ambient AC licenses the usual countable construction of the universal homogeneous structure; AC is not asserted in the symmetric interpretation.

The atom space itself, with its metric, belongs to the model: the whole structure has empty support, each coded metric or order tuple is supported by its finitely many atom coordinates, and pure rational values and their membership descendants are fixed. Thus the structure is hereditarily symmetric, not merely symmetric. Its metric satisfies the metric axioms in the model (Metric space: $d(x,y)=0$ iff $x=y$, symmetry, and the triangle inequality; pseudometric and ultrametric, The Axiom of Choice). The ordering is a distinguished dense rational order used to rigidify the finite metric structures; no equality or compatibility between its order topology and the metric topology is part of the construction.

For completeness, the model assertion is an internal axiom verification, as in Kleppmann §2.1, rather than an appeal to external well-foundedness. Finite supports form a normal system: intersections are handled by unions of supports, and $g\mathrm{fix}(e)g^{-1}=\mathrm{fix}(g[e])$. Rank recursion inside $M$ defines the action and the HS predicate; internal induction proves that HS is closed under membership and invariant under $G$. Every atom has singleton support, $A$ has empty support, and all pure sets are HS. Empty Set, Infinity, Extensionality and Foundation therefore restrict to HS. Pairing and Union preserve HS, using finite unions of supports. For $x\in \mathrm{H}\mathrm{S}$, Separation in $M$ forms $\{y\in {\mathcal{P}}^M(x):y\in \mathrm{H}\mathrm{S}\}$; invariance gives it any support of $x$, and its members are HS. This is the power set in the interpretation. For each fixed formula with HS parameters, relativize its quantifiers to HS. The action preserves the relativized formula. Consequently Separation on an HS set produces an HS subset, supported by the union of the supports of the set and parameters. If the formula defines a unique HS value for each member of an HS set, Replacement in $M$ produces its range; uniqueness and formula invariance give that range the same finite support, and all its members are HS. This verifies every instance of Separation and Replacement. The atom predicate and set of all atoms are inherited, completing ZFA. Purity is unchanged: internal membership closure places every descendant of an HS object in HS, so the pure kernel is exactly that of $M$. All recursions and inductions here are in $M$; no external induction on its possibly ill-founded membership relation is used.

• Why this group and not $\mathrm{Aut}(\mathbb{Q},<)$. The atoms carry both a rational metric and a distinguished order, and the automorphisms preserve both structures without any claim that their induced topologies coincide. The ordered-metric analogue of the finite-stabiliser extreme-amenability criterion is supplied separately in the next items, through Nešetřil's Ramsey theorem for finite ordered rational metric spaces and the KPT correspondence.