Consider Olivier Esser’s alternative axiomatic set theory $\mathit{GPK}^{+}_{\infty}$. Esser defines it as follows (this from his paper "Inconsistency of The Axiom of Choice with The Positive Theory $\mathit{GPK}^{+}_{\infty}$"):

The language is the usual one of set theory: $(\in,=)$. The class of the $\mathit{BPF}$ [the bounded positive formulas--my comment] is the class obtained from atomic formulas ($x=y$, $x\in y$) and the following rules: if $\varphi$ and $\psi$ are $\mathit{BPF}$ formulas, so are:

$\varphi\land\psi$, $\varphi\lor\psi$, $(\forall x\in y)\varphi$, $\exists x\varphi$

The $\mathit{GPK}^{+}$ theory is the following theory:

$\mathit{EXT}$: $\forall x\forall y\,[(\forall z(z\in x\Leftrightarrow z\in y))\Rightarrow x=y]$

$D$ [Empty Set(Class)–my comment]: $\exists x\forall y\,y\notin x$

$\mathit{Comp}(\mathit{BPF})$: the universal closure of the following formulas: $\exists a\forall x(x\in a\Leftrightarrow\varphi)$, where $\varphi$ is $\mathit{BPF}$

$\mathit{CL}$: $\forall y_1,\dots,\forall y_n\exists x[\forall z(\Gamma(z,y_1,\dots,y_n)\Rightarrow z\in x)\land\forall y((\forall z(\Gamma(z,y_1,\dots,y_n)\Rightarrow z\in y))\Rightarrow x\subseteq y)]$.

Note what Esser says about $\mathit{CL}$:

The scheme $\mathit{CL}$ says that for each class $A = \{ z: \Gamma(z, y_1,\dots,y_n) \}$, there is a smallest set for the inclusion which contains it; we denote this set $\bar A$.

(The astute reader may have noticed that '$\Rightarrow$' was not included in the list of primitive connectives by Esser. This is mentioned because in classical logic, $\varphi\Rightarrow\psi .\equiv. \lnot\varphi\lor\psi$, and if $\psi.\equiv.x\in x$, $x\in x\Rightarrow x\in x .\equiv. (x\notin x) \lor(x\in x)$ and $x\notin x$ is the formula which leads to Russell’s paradox. How then does one avoid Russell's paradox in $\mathit{GPK}^+$ (note that the '$\notin$' relation is used in Axiom $D$--hardly an example of a 'positive formula')? First note that Esser deems $\{z: \Gamma(z, y_1,\dots,y_n)\}$ a *class*, so $\mathit{GPK}^{+}$ is ostensibly about classes. In his paper, "On the Consistency of a Positive Theory", he defines the notion of set as follows:

"$\alpha$ is a set" ${}\Leftrightarrow\exists y\,\alpha\in y$

where $y$ is a class. In the same paper, Esser gives a topological definition of classes and sets:

We define classically a class as being a

definablecollection of the universe. We call a classclosediff it is a set (i.e. iff there is a set which same elements as it--in this case we identify the class and the set),openiff it is the complement of a set [that is, if $A$ is a class, the complement of $A$ is the class $\{x: x\notin A\}$–my comment].

Note also that taking the conjunction of the contrapositives of both sides of the implications of the definition of *set*, one has

"$\alpha$ is not a set" ${}\Leftrightarrow\forall y\,\alpha\notin y$ [this immediately shows that $\{\alpha\mid \alpha\notin\alpha\}$ is not a set]

Furthermore, Proposition 1.1(a) of "On the Consistency of a Positive Theory" states

The empty class and the universal class are open and closed.

Since the universal class is closed, it is a set, but the class $\{\alpha|\alpha\notin\alpha\}$ is not closed (otherwise the paradox would reappear–so proper classes are definable in $\mathit{GPK}^{+}$ as well), thus the paradox is avoided.)

To complete the definition of $\mathit{GPK}^{+}_{\infty}$, one adds to $\mathit{GPK}^{+}$ the following axiom of infinity:

"There exists a limit ordinal."

The following facts are known about $\mathit{GPK}^{+}_{\infty}$:

(i) $\mathit{GPK}^{+}_{\infty}$ interprets both $\mathit{ZF}$ and $\mathit{MK}$ set theories (so the Kunen Inconsistency can be properly interpreted in $\mathit{GPK}^{+}_{\infty}$)

(ii) Esser allows for class-functions to be defined in $\mathit{GPK}^{+}_{\infty}$ (so the possibility of 'class-cardinals' distinct from 'set-cardinals' exists--cardinals that may not have "critical points")

(iii) $\mathit{GPK}^{+}_{\infty}\vDash\lnot\mathit{AC}$, where $\mathit{AC}=_{df}$ "there exists a function $f$ such that $(\forall x\ne\emptyset) f(x)\in x$" . (This suggests that one can use $\mathit{GPK}^{+}_{\infty}$ to study whether or not one can reproduce the Kunen Inconsistency without Choice, upon which it seems to depend. Also note that the following forms of $\mathit{AC}$ are also inconsistent with $\mathit{GPK}^{+}_{\infty}$: "For any non-empty set $x$ of disjoint non-empty sets, there exists a set $a$ intersecting each element of $x$ into a singleton"; "Any relation includes a function with the same domain"; "Any set can be well-ordered".)

(iv) $\mathit{GPK}^{+}_{\infty}\vDash\lnot\mathit{Foundation}$. This can be shown by recalling that

the hyperuniverses $\mathrm N_{\kappa}$ ($\kappa$ being a strongly inaccessible, weakly compact cardinal) satisfy the theory $\mathit{GPK}^{+}_{\infty}$ [this from Esser's "On the Consistency of a Positive Theory, pg.110--my comment]

and that

Trivially, $\kappa$-hyperuniverses do not satisfy the Axiom of Foundation. [This from Forti and Honsell's paper, "Choice principles in hyperuniverses", pg. 46. The $\mathrm N_{\kappa}$ are the symbols for the $\kappa$-hyperuniverses--my comment.]

It is interesting to note that, though $\mathit{GPK}^{+}_{\infty} + \mathit{Foundation}$ is inconsistent, Esser, in his paper, "Inconsistency of $\mathit{GPK} + \mathit{AFA}$", proved that at least one of the antifoundation axioms does not hold for $\mathit{GPK}$, where $\mathit{GPK}$ is theory $\mathit{EXT} + \mathit{Comp}(\mathit{GPK})$, and the $\mathit{GPK}$ formulas are just the $\mathit{BPF}$ formulas and the folowing rule:

If $\theta(x)$ is any formula having a unique free variable $x$, and if $\alpha$ is a $GPF$ formula, then the formula $\forall x(\theta(x)\Rightarrow\alpha )$ is a $GPF$ formula.

Esser, in his paper, "An Interpretation of the Zermelo-Fraenkel and the Kelly-Morse Set Theory in a Positive Theory" (from which the rule defining the $GPK$ theory from the $BPF$ formulas was quoted) also proves that the $GPK^{+}$ theory implies the $GPK$ theory (because, according to Esser, "...the passing from the $GPK$ theory to the $GPK^{+}$ theory amounts to allowing parameters in $\theta$ [the rule I quoted above--my comment]). This is because by replacing the closure axiom $CL$ by the axiom $CL'$,

$CL'$: Let $\theta$ be a formula (not necessarily $BPF$ or $GPK$ ) not having $y$ as a free variable and let $\alpha$ be a $BPF$ formula (or more generally any formula defining a set). Then the class $\{y\mid \forall x(\theta\Rightarrow\alpha ) \}$ is closed.,

$GPK^{+}$ looks like $GPK$. Also,because

Proposition 1.3. $\mathit{Comp}(\mathit{BPF}) + D +\mathit{EXT}\vDash \mathit{CL}\Leftrightarrow\mathit{CL}'$

one has that $\mathit{GPK}^{+} + \mathit{AFA}$ is inconsistent and $\mathit{GPK}^{+}_{\infty} + \mathit{AFA}$ is inconsistent as well, so that one can rightly ask the question asked in the title,

"Is $\mathit{GPK}^{+}_{\infty} + \mathit{BAFA}$ inconsistent?", where $\mathit{BAFA}$ is the axiom

For every injective function $f\colon X\rightarrow\mathscr P(x)$, which is the identity on a transitive $T\subseteq X$, there is an injective function $g\colon X\rightarrow V$, which is the identity on $T$ and verifies

$g(x) = \{ g(y)\mid y \in f(x)\}$ $\forall x\in X$ [this from Forti and Honsell's paper, Choice principles in Hyperuniverses--my comment].

(For if it is not inconsistent, then there are nontrivial elementary embeddings of the universe into itself--and I hope that this overly long exposition shows the reader why it does matter.)

allmodels of the theory refute foundation, not thatsomemodel does. Fortunately, the theory indeed disproves foundation for the trivial reason that it proves the existence of a universal set, which is then its own element. (2) BAFA doesnotimply the existence of nontrivial elementary embeddings. At the very least, the usual proof also relies on global choice (enumeration of the universe by ordinals). Since your theory disproves choice, the argument breaks down. $\endgroup$ – Emil Jeřábek Sep 15 '16 at 14:21itsuniverse, this does not imply anything about the existence of automorphisms or el.emb. of the universe of theinterpretingtheory. Also, your question omits AC_{WF}. $\endgroup$ – Emil Jeřábek Sep 21 '16 at 9:23not$\kappa$-topological spaces, so the lemma is irrelevant here. $\endgroup$ – Emil Jeřábek Sep 21 '16 at 16:14