About the definitions of well-foundedness in this extension of NFU that interprets ZFC?

Question

Lets see how the world of sets could look like from the perspective of $\sf NFU$. So, here we work within the first order language of set theory, with the following extra-logical axioms:

1. Quine atom: There exists a unique Quine atom, i.e. a singleton that is an element of itself.

An "urelement" is defined as a singleton of the Quine atom. That is, it has one element and that element is the Quine atom.

2. Extensionality: if $x$ is not an urelement, then every set co-extensional with $x$ is equal to $x$.

3. Stratified Comprehension: as stated in $\sf NFU$.

4. Urelements: The set of all urelements is bijective with the set of all objects, i.e. the set of all urelements is as big as the universe.

5. Choice: as stated in $\sf NFU$.

Define: a set is said to be well founded if it is an element of every set that is a superset of its own powerset. Formally:

$$\operatorname {well-founded}(s) \iff \forall X: \mathcal P(X) \subseteq X \to s \in X$$

6. Replacement: if $A$ is a well founded set, and $\phi(x,y)$ is a formula standing for a many-to-one relation from well founded sets to well founded sets, then there is a set $\{y \mid \exists x \in A : \phi(x,y)\}$.

7. Infinity: There is a well-founded set having the empty set among its elements, that is closed under singletons.

So, this theory has a universe obeying the rules of $\sf NFU$ (but with urelements being the singletons of the Quine atom, instead of the usual formulation as element-less objects), and that has its well founded realm obeying the rules of $\sf ZFC$.

The definition of well-foundedness is due to Thomas Forster, while the theory is speaking about Holmes's $\sf BEST$ model of $\sf NFU$ with little modification.

This theory is way stronger than $\sf ZFC$ and of course $\sf NFU$, it goes high up to measurable cardinals.

Now, my question is about that definition of well foundedness which is just a recapture of stratified $\in$-induction in $\sf NFU$ terms. How this compares to the traditional definition of well foudedness:

\begin{align} \operatorname {well-founded}(s) \iff \exists t : \ & \operatorname {trs}(t) \land s \subseteq t \ \land \\&\forall v: \operatorname {trs}(v) \land s \subseteq v \to t \subseteq v \ \land \\ & \forall c \subseteq t \exists b \in c: b \cap c = \varnothing \end{align}

This definition also obeys stratified $\in$-induction.

Actually even the following simpler definition obeys stratified $\in$-induction:

$ \operatorname {well-founded}(s) \iff \\ \forall x \, (s \in x \to \exists y \in x: y \cap x =\varnothing)$

Answer 1

The Forster definition of well foundedness, which is essentially nothing but stratified $\in$-induction, i.e. a set $x$ is Forster well-founded if for any stratified property $P$ such that for any set $s$ if all elements of $s$ meet $P$ then $s$ must meet $P$ also, then $x$ must meet $P$. Now, the Sheridan definition of well foundedness (the last definition in the head post) is the dual of Forster's.

First direction: if $x$ is Forster well-founded, then $x$ must be Sheridan well-founded

Proof: let $x$ be Forster well-founded and Sheridan non-well-founded, then there is a descending membership set $d$ where $x \in d$, now take the complementary set $d'$ of $d$, so $d'$ would be a superset of its own powerset, but $x$ is not in $d'$, contradicting it being Forster well-founded.

Second direction: if $x$ is Sheridan well-Founded, then $x$ is Forster well-founded

Proof: let $x$ be Sheridan well-founded but not Forster well-founded, so there must be a set $K$ such that $\mathcal P(K) \subseteq K$ and $x \notin K$. Now take the complementary set $K'$ of $K$, and $K'$ would be a descending membership set where $x \in K'$, contradicting $x$ being Sheridan well-founded.

Regarding the stance from the traditional definition (the second one in the head post), we have each traditional well-founded set being Sheridan well-founded, but not necessarily the converse.

Proof: if $x$ is traditional well founded and not Sheridan well-founded, then there is a descending membership set $d$ with $x \in d$. Now, $d \cap \operatorname {trcl}(x)$ would be a subset of the transitive closure of $x$ that is a descending membership set, violating the definition of traditional well-foundedness.

$\sf NFU$ cannot prove the other direction, since it doesn't prove existence of transitive closures for all sets. The problem with $\sf NFU$ is that possessing a transitive closure is not stratified. So, unlike in extensions of $\sf Zermelo$, it won't be guaranteed by $\in$-induction over all Forster (Sheridan) sets. So, $\sf NFU$ by itself won't grant the second direction, and so equivalence of the traditional definition with Forster (Sheridan) definition won't be proved.

However, in the system presented in the head posting which uses Forster's definition, this would prove the existence of a transitive closure for every Forster well-founded set and hereditarily so, as well as $\in$-induction over Forster's well-founded sets for all formulas, and so would prove the equivalence with the traditional definition. But, if the theory in the head post was formalized in terms of the traditional definition, then it won't grant that equivalence.