**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?
> 
> 
> 



Can we have a hybrid comprehension between Z and NF?
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.


