Can we have a hybrid comprehension between Z and NF?

Question

Hybrid Comprehension: if $\phi,\varphi$ are formulas in which $x$ doesn't occur, and $\varphi$ is stratified; then: $$ \forall A \exists x \forall y \, (y \in x \leftrightarrow \varphi \land [wf(A) \land A \neq \emptyset \to y \in A \land\phi] )$$

Where $wf$ stands for being well founded, defined as:

$wf(A) \iff \not \exists S: \operatorname {\downarrow}(S) \land A \in S$

Where: $\operatorname {\downarrow}(S) \iff \forall x \in S \exists y \in x \, (y \in S)$

The above is a hybrid between $\sf Z$ and $\sf NF$ set theories. Assuming Extensionality, if we add the existence of $\omega$, then we get to interpret $\sf Z$ over the well founded set realm of this theory, while $\sf NF$ would hold over all sets.

Can this be extended further as to have more non-stratified comprehension beyond the well founded world?

I have the following line of thought:

Let $x$ be termed as "superficially well founded" if and only if every subset $y$ of $x$ has an element that is disjoint of it, formally:

$swf(x) \iff \forall y \subseteq x \exists z \in y: z \cap y = \emptyset$

Let $\phi^{swf}$ be the formula resulting from merely bounding all quantifiers in $\phi$ by the predicate $swf$, that is $\forall x .. , \exists y..$ in $\phi$ becomes $\forall x \, (swf(x) \to ..); \exists y (swf(y) \land ..)$ in $\phi^{swf}$.

Contemplate adding the following axiom:

swf-Separation: if $\phi$ is a formula in which $x$ doesn't occur; then: $$ \forall A \, [swf(A) \to \exists x \forall y \, (y \in x \leftrightarrow y \in A \land\phi^{swf} )]$$

Is there an obvious inconsistency with that?

Answer 1

NF+swf-Separation is inconsistent.

Let P1(X) be the set of one element subsets of X. Let z={Ø,{Ø},{{Ø}}} Let S={{P1(A),z}| A is infinite}.

Let T be the set of subsets of S.

(1) Suppose A is infinite. Then {P1(A),z}∩P1(A)=Ø and therefore swf({P1(A),z}).

(2) Suppose A is infinite. Then {P1(A),z}∩S=Ø. and therefore swf(S).

Proof: P1(A) is not in S because every element of S is a set with 2 elements. 
       
       z is not in S because every element of S is a set with 2 elements.

(3) S∩T=Ø.

Proof: Suppose A is infinite. Then {P1(A),z} is not  a subset of S.

Let P={{a,b}| a∈T and b∈S}.

(4) Suppose a∈T, b∈S, and b∉a. Then a∩{a,b}=Ø and b∩{a,b}=Ø, and thus swf({a,b}).

Proof: If a∈a, then a∈S, and consequently there is an infinite set A with 

       P1(A)∈a. But every element of a is a 2 element set. Therefore a∩{a,b}=Ø.

       a∉b because neither element of b is a set of 2 element sets. b∉b because

       b is a 2 element set with no element which is a 2 element set. 

       Therefore b∩{a,b}=Ø.

(5) Suppose a∈T and b∈S. Then {a,b}∩P=Ø and therefore swf(P).

Proof: By (3), a∩T=Ø and so a∉P. P1(A)∈b for some infinite set A. By (2), P1(A)∉S.   
       
       P1(A)∉T because T is a set of 2 element sets. Therefore b∉P.

(6) There is a 1-1 function from T to S.

Proof: Let N be the set of natural numbers and let O be the set of odd numbers.

       Let d be the 1-1 function from sets to infinite sets defined by 

         da={2n|n∈N∩a}U{x|x∈(a-N)}UO.

       Now define f:T-->S by ft={P1(d{A|{P1(A),z}∈t}),z}. Then f is 1-1.

Let f be a 1-1 function from T to S. Let F={{a,b}|a∈T and b∈S and fa=b}. By (5), swf(F).

Let φ(x) be the formula ∃t(t∈T∧∃p(p∈F∧t∈p∧x∈p∧x∉t)). Then for x∈S, φ(x) is equivalent to its

relativization to swf. By swf-Separation, there is a C such that x∈C<-->x∈S∧φ(x).

Suppose fC=c. Then c∈C<-->c∉C.