TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Fraenkel–Mostowski permutation-model theorem

Statement

For a transitive ZFA model $M$ and an $M$ -internal normal permutation system $(A, G, F)$ , ${H S}_{F}^{M}$ is a transitive ZFA model with the same atoms and pure kernel. Here $A, G, F \in M$ , the action and filter satisfy the defining clauses in $M$ , and hereditary symmetry is evaluated in $M$ . Even if $M$ satisfies AC, ${H S}_{F}^{M}$ need not.

Facts & Assumptions

Given: The stated transitive ZFA model and $M$ -internal normal permutation system. AC is not assumed for the model construction.

[F1]

Symmetric and hereditarily symmetric sets gives transitivity and hereditary closure.

[F2]

The Axiom of Choice names the property addressed only in the final noninheritance clause.

Proof

1.1

Every atom is symmetric because ${fix}_{G} ({a})$ fixes $a$ , and every pure set is fixed by every permutation; both are hereditarily symmetric, so $A \cup K \subseteq H S$ , while conversely the pure kernel is unchanged because no atom lies in a pure set. Transitivity is F1. Empty Set, Infinity, Extensionality and Foundation restrict from $M$ . If $x, y \in H S$ , the stabilizer intersection fixes ${x, y}$ , $x \cup y$ , and the usual finite set operations; their members are hereditary, giving Pairing and Union.

1.2

Because $G, F$ and their action are internal to $M$ , the predicate “ $u \in {H S}_{F}^{M}$ ” is definable over $M$ from those parameters by rank recursion. Hence $M$ -Separation forms

$z = {u \in P^{M} (x) : M ⊨ u \in {H S}_{F}} .$

Every permutation fixing $x$ maps $z$ to itself because hereditary symmetry is invariant; all members are HS, so $z \in H S$ and it is exactly the internal power set. For Separation with supported parameters, formula invariance shows the defining subset of $x$ has the intersection of their stabilizers as support. [F1]

1.3

For Replacement, suppose the internal formula assigns a unique $y$ to every $x \in a$ . Ambient Replacement forms the image $b$ . Any permutation fixing $a$ and all parameters maps a witnessed pair $(x, y)$ to $(g x, g y)$ ; uniqueness therefore maps $b$ to itself. Each value $y$ is in HS by the internal quantifier domain, so $b$ is hereditarily symmetric. This proves every ZFA axiom without Choice.

2.1

Noninheritance is witnessed by the finite-support full-permutation system on a countably infinite atom set: its atom set is HS, but a supported well-order would be moved by a transposition outside its finite support. Thus the ambient $M$ may satisfy F2 while its HS submodel does not.

F2∎

Depends on

Used by

Jech–Sochor first embedding theorem Theorem
The basic Fraenkel model Theorem
The ordered Mostowski model Theorem
The second Fraenkel model has countable pairs without a choice function Theorem

Dependency tree · two levels

5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jech, The Axiom of Choice, Theorem 4.1, pp. 46–47 (standard reference, not scraped)