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) \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?

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?

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) \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. 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?

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) \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?