Questions on Fraenkel models Halbeisen on page 172 contains a section entitled "The Second Fraenkel Model". The original paper by Fraenkel containing this model can be found here. I have several questions regarding this model and $\mathsf{FM}$-models in general. 


*

*If this 1922 paper by Fraenkel is not the first describing $\mathsf{FM}$-models, can someone please point me to his very fist paper in which he invents the technique? (given that Halbeisen calls it the second model I suppose there must be an earlier paper containing his first model although looking at this list of publications it appears to be his first.)

*In this 1922 paper he writes that for this model construction we can keep the axioms of Zermelo I,II,IV-VII as they are but in Halbeisen on page 168 it is stated that we need to use modified versions of Empty Set and Extensionality. Hence my question 2.a) is: Is this a mistake in Fraenkel's paper? (Unlikely, I would think) and my question 2.b) is: Empty Set is a consequence of all the other axioms hence wouldn't it be enough to just use a modified version of Extensionality?

*Last but not least the question that is most important to me: What exactly did Fraenkel's 1922 paper prove? The aim of course was to show that $\mathsf{AC}$ is independent of $\mathsf{ZF}$ by constructing a model of $\mathsf{ZF}$ in which $\mathsf{AC}$ fails. But the model he constructed is a model of $\mathsf{ZFA}$ and not of $\mathsf{ZF}$ and it seems to be the case that those transfer methods used to embed these Fraenkel models into symmetric models weren't known for another 30 years or so. Hence: what is the relation of $\mathsf{ZFA}$ and $\mathsf{ZF}$? (without using transfer methods)
 A: Historically the list of axioms known as $\sf ZF$ wasn't written until mid-1920's when von Neumann wrote his Ph.D. dissertation, where he proved the relative consistency of regularity, and defined the ordinals as we know them today, and so on.
Fraenkel's original proofs contained mistakes. I don't know the exact mistake, but I do know that Mostowski found a mistake; Fraenkel rewrote his arguments; Mostowski found further mistakes, and ended up writing the arguments using supports which is very similar to what we know today, Specker was the one putting the finishing touch on the technique. Do note that not once the constructions were done in $\sf ZFC-Reg$, where sets of the form $x=\{x\}$ were used for atoms. (This is why in quite a few places this method is called Fraenkel-Mostowski or even Fraenkel-Mostowski-Specker.)
Lastly, $\sf ZFA$ contains atoms. That's huge. Even more so when we only "disorder" the impure sets. Note that no matter how hard you'll try, you can never form a permutation model in which the real numbers cannot be well-ordered. Because the power of the integers can be well-ordered in permutation models of $\sf ZFA$. But Fraenkel did "prove" (or at least lay foundations for the proof) that the axiom of choice is not provable from the other axioms when we allow atoms, and that was a big step. It shows that this axiom is not a consequence of Zermelo's set theory (sans choice itself, of course) if we allow atoms.
The historical overview, including references, by the way, can be found in both Jech's "The Axiom of Choice" and in Halbeisen's book, in the same chapter (the notes section at the end).
A: Since we are dealing with models of $\sf{ZFA}$, we have to keep those atoms in mind.  In particular, atoms have no elements, and so they have the same elements as the empty set.  But they are different from the empty set.  And from each other.  Therefore a modified form of Extensionality is needed.  Usually $\sf{ZFA}$ includes a predicate to the effect of $A(x)$ holds iff $x$ is an atom.  So Extensionality should be rephrased

$( \forall x ) ( \forall y ) ( ( \neg A(x) \wedge \neg A(y) ) \rightarrow ( ( \forall u ) ( u \in x \leftrightarrow u \in y ) \rightarrow x = y ) )$.

To put it into words: any two non-atoms (i.e., sets) which have the same elements are equal.
The Empty Set Axiom is similarly altered to ensure a set without elements:

$( \exists x ) ( \neg A(x) \wedge ( \forall u ) ( u \notin x ) )$.

As to the question of its necessity? This is a bit tricky. 


*

*Note that unchanged, the Axiom Schema of Separation applied to some set $X$ and the formula $\varphi (u) \equiv u \neq u$ will yield some object $Y$ with the property that $u \notin Y$ for all $u$.  However by unchanged this means that there is no specification that the object $Y$ is itself a set. In particular, the object $Y$ could be an atom.  

*Note also the following construction:  Given any atom $a$, consider, by the Axiom of Power Set (unchanged) $$\mathcal{P} ( a ) = \{ X : ( \forall u ) ( u \in X \rightarrow u \in a ) \}.$$ Note that $\mathcal{P} ( a )$ contains all atoms, and no nonempty sets.  Then applying an instance of (a slightly expanded) Axiom Schema of Separation, we get the set $$Y = \{ X \in \mathcal{P} ( a ) : \neg A ( X ) \}.$$ Then either $Y$ is empty, or contains the empty set.  In particular, the empty set must exist.  But this construction only works if you allow the predicate $A$ in instance of the Axiom Schema of Separation, which hasn't been explicitly stated by Halbeisen.
After some extra consideration, it appears to me that the way to get the existence of the empty set in $\sf{ZFA}$ making the least number of changes to $\sf{ZF}$ might be to include the (modified) Axiom of Empty Set.  Of course, one could formulate the axioms of $\sf{ZFA}$ by going through all the axiom of $\sf{ZF}$ and ensure that when objects are constructed they are sets, and then the usual method of showing that the empty set exists would go through.
One should note that in Jech's The Axiom of Choice, $\sf{ZFA}$ is described as the theory obtained by making the following alterations to $\sf{ZF}$:


*

*include a unary predicate symbol $A$, and a constant symbol $0$.

*Axiom of Empty Set. $\neg ( \exists x ) ( x \in 0 )$.

*Axiom of Atoms. $( \forall z ) ( A(z) \leftrightarrow ( z \neq 0 \wedge \neg ( \exists x ) ( x \in z ) ) )$.

*Axiom of Extensionality. $( \forall \text{ set } X ) ( \forall \text{ set } Y ) ( ( \forall u ) ( u \in X \leftrightarrow u \in Y ) \leftrightarrow X = Y )$.

*Axiom of Regularity. $( \forall \text{ nonempty } S ) ( \exists x \in S ) ( x \cap S = 0 )$.


where 


*

*$( \forall \text{ set } X ) \ldots$ abbreviates $( \forall X ) ( \neg A ( X ) \rightarrow \ldots )$; and

*$( \forall \text{ nonempty } X ) \ldots$ abbreviates $( \forall X ) ( ( \exists x ) ( x \in X ) \rightarrow \ldots )$.



What did Fraenkel's paper do?  You're right that it was a weaker result, proving that $\sf{AC}$ is not provable from $\sf{ZFA}$, but it at least hinted at the possibility of Cohen's later result.  And one should see a similarity between the method of permutation models, and symmetric submodels of generic extensions.  Note, also, that any model of $\sf{ZF}$ is a model of $\sf{ZFA}$, with an empty collection of atoms.
A: This is just a footnote to the other responses. But it is interesting that there seems to be a bit of a resurgence of interest in Fraenkel-Mostowski permutation models going on (for a small local example, this year 'Permutation Models for Set Theory' is on the list of essay topics for Part III Maths Tripos).
One source of renewed interest is from computer scientists interested in "capture-avoiding substitution": for some general thoughts, see e.g. this paper.
Another recent source is that Randall Holmes's announced proof of the consistency of NF set theory uses FM techniques. Interesting times!
