Return to Answer

For the other direction it won't hold unless $x$ has a transitive closure, and every element in its transitive closure has a transitive closure, that is every Sheridan well-founded set that hereditarily has a transitive closure, is a traditional well-founded set.

Proof: suppose $x$ is Sheridan well founded, hereditarily has a transitive closure, but not traditional well founded, then there is a set $c \subseteq \operatorname {trcl}(x)$ such that $c$ is a descending membership set, now take any $b \in c$, then define the set $B$ of all elements of $\operatorname {trcl}(x)$ that has $b$ in their transitive closure, take $B \cup c $, this would be a descending membership set because all elements of $c $ are already fulfilling the descending membership property, now every set $y \in B$ must have an element $z \in y$ such that either $z=b \lor b \in \operatorname {trcl}(z)$ and thus $z \in (B \cup c )$, because the transitive closure of $y$ is the set union of the transitive closures of its elements, so if $b$ is not in any of those nor is an element of $y$, then $b$ won't be in the transitive closure of $y$, a contradiction! Thus $B \cup c \cup \{x\}$ must be a descending membership set of which $x$ is an element, negating Sheridan's definition of non-well foundedness.

  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, and so would prove the equivalence with the traditional definition. However, if the theory in the head post was formalized in terms of the traditional definition, then it won't grant that equivalence.

$\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.

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.

For the other direction it won't hold unless $x$ has a transitive closure, that is every Sheridan well-founded set that has a transitive closure is a traditional well-founded set.

Proof: suppose $x$ is Sheridan well founded, has a transitive closure, but not traditional well founded, then there is a set $c \subseteq \operatorname {trcl}(x)$ such that $c$ is a descending membership set, now take any $b \in c$, then define the set $B$ of all elements of $\operatorname {trcl}(x)$ that has $b$ in their transitive closure, take $B \cup c $, this would be a descending membership set because all elements of $c $ are already fulfilling the descending membership property, now every set $y \in B$ must have an element $z \in y$ such that either $z=b \lor b \in \operatorname {trcl}(z)$ and thus $z \in (B \cup c )$, because the transitive closure of $y$ is the set union of the transitive closures of its elements, so if $b$ is not in any of those nor is an element of $y$, then $b$ won't be in the transitive closure of $y$, a contradiction! Thus $B \cup c \cup \{x\}$ must be a descending membership set of which $x$ is an element, negating Sheridan's definition of non-well foundedness.

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 so would prove the equivalence with the traditional definition. However, if the theory in the head post was formalized in terms of the traditional definition, then it won't grant that equivalence.

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.

For the other direction it won't hold unless $x$ has a transitive closure, and every element in its transitive closure has a transitive closure, that is every Sheridan well-founded set that hereditarily has a transitive closure, is a traditional well-founded set.

Proof: suppose $x$ is Sheridan well founded, hereditarily has a transitive closure, but not traditional well founded, then there is a set $c \subseteq \operatorname {trcl}(x)$ such that $c$ is a descending membership set, now take any $b \in c$, then define the set $B$ of all elements of $\operatorname {trcl}(x)$ that has $b$ in their transitive closure, take $B \cup c $, this would be a descending membership set because all elements of $c $ are already fulfilling the descending membership property, now every set $y \in B$ must have an element $z \in y$ such that either $z=b \lor b \in \operatorname {trcl}(z)$ and thus $z \in (B \cup c )$, because the transitive closure of $y$ is the set union of the transitive closures of its elements, so if $b$ is not in any of those nor is an element of $y$, then $b$ won't be in the transitive closure of $y$, a contradiction! Thus $B \cup c \cup \{x\}$ must be a descending membership set of which $x$ is an element, negating Sheridan's definition of non-well foundedness.

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, and so would prove the equivalence with the traditional definition. However, if the theory in the head post was formalized in terms of the traditional definition, then it won't grant that equivalence.

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.

For the other direction it won't hold unless $x$ has a transitive closure, that is if every Sheridan well-founded set that has a transitive closure is a traditional well-founded set.

Proof: suppose x is Sheridan well founded, has a transitive closure, but not traditional well founded, then there is a set $c \subseteq \operatorname {trcl}(x)$ such that $c$ is a descending membership set, now take any $b \in c$, then define the set $B$ of all elements of $\operatorname {trcl}(x)$ that has $b$ in their transitive closure, take $B \cup c $, this would be a descending membership set because all elements of $c $ are already fulfilling the descending membership property, now every set $y \in B$ must have an element $z \in y$ such that either $z=b \lor b \in \operatorname {trcl}(z)$ and thus $z \in (B \cup c )$, because the transitive closure of $y$ is the set union of the transitive closures of its elements, so if $b$ is not in any of those nor is an element of $y$, then $b$ won't be in the transitive closure of $y$, a contradiction! Thus $B \cup c \cup \{x\}$ must be a descending membership set of which $x$ is an element, negating Sheridan's definition of non-well foundedness.

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 so would prove the equivalence with the traditional definition. However, if the theory in the head post was formalized in terms of the traditional definition, then it won't grant that equivalence.

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.

For the other direction it won't hold unless $x$ has a transitive closure, that is every Sheridan well-founded set that has a transitive closure is a traditional well-founded set.

Proof: suppose $x$ is Sheridan well founded, has a transitive closure, but not traditional well founded, then there is a set $c \subseteq \operatorname {trcl}(x)$ such that $c$ is a descending membership set, now take any $b \in c$, then define the set $B$ of all elements of $\operatorname {trcl}(x)$ that has $b$ in their transitive closure, take $B \cup c $, this would be a descending membership set because all elements of $c $ are already fulfilling the descending membership property, now every set $y \in B$ must have an element $z \in y$ such that either $z=b \lor b \in \operatorname {trcl}(z)$ and thus $z \in (B \cup c )$, because the transitive closure of $y$ is the set union of the transitive closures of its elements, so if $b$ is not in any of those nor is an element of $y$, then $b$ won't be in the transitive closure of $y$, a contradiction! Thus $B \cup c \cup \{x\}$ must be a descending membership set of which $x$ is an element, negating Sheridan's definition of non-well foundedness.

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 so would prove the equivalence with the traditional definition. However, if the theory in the head post was formalized in terms of the traditional definition, then it won't grant that equivalence.