It is well known that the 'set-hood' predicate in Ackermann's set theory essentially needs to be undefinable in the language of set theory. This theory present what can be generally thought of as being Akermannian like theory, but here the pivotal predicate is that of well-foundedness, it does everything in the language of set theory.
Language: First order logic with equality and membership, with the extra-logical axioms of:
Extensionlity: $\forall z (z \in x \leftrightarrow z \in y) \to x=y$
Classes: if $\phi$ is a formula in which $x$ doesn't occur free, then $(\exists x \forall y (y \in x \leftrightarrow set(y) \land \phi))$
Where: $set(y) \iff \exists z (y \in z)$
Define: $V=\{x| set(x)\}$
Well founded Reflection: if $\phi$ is a formula in which every quantifier is bounded $\in V$, and having all its free variables among symbols $y,x_1,..,x_n$, then: $$\forall x_1,..,x_n \in V \\ [\forall y (\phi \to wf(y)) \to \exists x \in V \forall y (y \in x \leftrightarrow \phi)]$$
Where $``wf"$ stands for "is a well founded class", defined as:
$wf (y) \iff \not \exists d (y \cap d \neq \emptyset \land \forall m \in d \exists n \in d (n \in m))$
Infinity: $\omega \in V$
Where $\omega$ is the set of all finite Von-Neumann ordinals.
I personally think that this must be inconsistent. I think that there must be a bounded in $V$ formula that is equivalent to well-foundedness, which would prove this theory inconsistent. However this is somehow eluding me.
Question 1: is the above theory obviously inconsistent?
Question 2: if consistent? What would be its consistency strength?