A characterization of permutation models in terms of forcing (Q1430902)

ZFA denotes ZF set theory altered to allow a set of atoms. A known phenomenon is the existence of statements that are independent of ZFA but yet hold in every permutation model. The author produces a sentence of set theory \(\psi\) that is true in all permutation models and has the property that if \(\phi\) is any sentence that is true in every permutation model, then ZFA\( + \psi \vdash \phi\). The existence of \(\psi\) follows from the author's main theorem, which in non-technical terms asserts that a transitive model of ZFA is a permutation model if and only if some generic extension of the transitive model with the same kernel satisfies AC. The sentence \(\psi\) is obtained from this characterization because forcing is definable in set theory.