# Is this set theory equivalent to ZFC?

Consider a variant of set theory with these axioms:

• Extensionality,
• Regularity (foundation),
• Separation,
• Powerset,
• Axiom of Choice, and
• Transitive closure of a set-like relation is set-like. Update: This did not exactly represent what I had in mind, so the corrected version is given on the next line, and its precise formalization is given below. Sorry for my mistake and ensuing confusion.
• The transitive closure of any set under a set-like relation is a set.

Note that it does not explicitly postulate Pairing, Union, Infinity and Replacement.

Question: Is this set theory equivalent to $$\mathrm{ZFC}$$?

Detailed explanation and formalization:

• We use symbol $$\prec$$ to represent a binary relation. In general, it is a definable class relation, that is a first-order formula with 2 free variables (and, possibly, additional parameters). As usual, we write $$a\prec b$$ to represent $$\prec\!(a,b),$$ and we assume that all bound variables in any formula are automatically renamed before a substitution to avoid variable name conflicts that would change its meaning.
• We use “is a set” and “exists” as synonyms; “sethood” and “existence” are also synonyms.
• We write $$a\prec b\prec c$$ to represent $$a\prec b\land b\prec c$$. This notation can also mix several different relation symbols, e.g. $$a\prec b\in c$$.
• When we say that a relation $$\prec$$ is “set-like”, we mean $$\color{green}{\forall x\,\exists y\,\forall z\left(z\prec x\;\Rightarrow\; z\in y\right)}.$$
• When we say that “$$w$$ is a superset of the transitive closure of $$s$$ under the relation $$\prec$$”, we mean $$\color{maroon}{s\subseteq w\,\land\,\forall u\,\forall v\left(u\prec v\in w\;\Rightarrow\; u\in w\right)}.$$
• We also may rephrase it as “the transitive closure of $$s$$ under $$\prec$$ is a subset of $$w$$” or simply “the transitive closure of $$s$$ under $$\prec$$ is a set”. At this point, we do not need to define what “the transitive closure” exactly is, because we are only interested in asserting its sethood, so existence of any its superset $$w$$ is sufficient for our purposes. I suppose that, when the need arises, “the transitive closure” can be defined as the smallest such set, and can be carved out of its superset using Separation.
• Our last axiom asserts that, provided $$\prec$$ is a set-like relation, the transitive closure of any set $$s$$ under that relation $$\prec$$ is a set. It can be formalized using the following axiom schema where $$\prec$$ ranges over all binary relations: $$\left(\vphantom{\Large|}\color{green}{\forall x\,\exists y\,\forall z\left(z\prec x\,\Rightarrow\,z\in y\right)}\right)\,\Rightarrow\,\forall s\,\exists w\!\left(\vphantom{\Large|}\color{maroon}{s\subseteq w\,\land\,\forall u\,\forall v\left(u\prec v\in w\,\Rightarrow\,u\in w\right)}\right)\!.$$
• The last axiom schema can be thought of as a bolder version of Replacement. Dec 29, 2020 at 23:39
• How are you defining the transitive closure of a relation without the axiom of infinity? Dec 29, 2020 at 23:39
• The class consisting of all finite sets satisfies your axioms but not ZFC. Dec 30, 2020 at 0:34
• @PaceNielsen I updated my question to express my idea more clearly. There is a proposed formalization for the transitive closure not using a notion of an infinite set or a union. I believe, the last axiom is strong enough to imply Axioms of Infinity and Union. Dec 30, 2020 at 2:16
• If you believe that your axioms imply the axiom of infinity, you may want to present a proof here. Your last line of OP is not clear to me. What is $s$? Dec 30, 2020 at 6:06

Accepting the convention that it is a logical axiom that the universe is nonempty, the answer is yes. We will formalize the transitive closure axiom schema (TC) as follows: for any definable (with parameters) binary relation $$R,$$ if for all $$x,$$ $$\{y: y R x\}$$ is a set, then for all $$x,$$ there is a set $$T$$ such that $$x \in T$$ and $$T$$ is closed downwards under $$R.$$ (*) Of course, this can only be weaker than asserting the existence of a minimum such $$T.$$

For efficiency, we will prove Pairing, Union, Infinity, and Replacement from Extensionality, Separation, and TC.

Pairing: We first note that $$\emptyset$$ exists by applying separation to an arbitrary set. Next, for all $$x,$$ $$\{x\}$$ exists by applying TC to $$x$$ and the empty relation. Finally, for all $$x, y,$$ we get $$\{x,y\}$$ by applying TC to $$x$$ and the relation defined by $$a R b$$ iff $$b = x$$ and $$a=y.$$

Union: Fix a set $$S.$$ By Separation and Russell's paradox, there is $$x \not \in S.$$ Define $$R$$ by $$a R b$$ iff $$b = x$$ and $$a \in S$$ or $$b \in S$$ and $$a \in b.$$ Then we get $$\bigcup S$$ by applying TC to $$x$$ and $$R.$$

Infinity: Define a relation $$R$$ by $$a R b$$ iff $$a$$ and $$b$$ are natural numbers and $$a=b+1.$$ Then $$\omega$$ exists by applying TC to $$\emptyset$$ and $$R.$$

Replacement: Fix a set $$S$$ and a definable function $$F.$$ Fix $$x \not \in S.$$ Define $$R$$ by $$a R b$$ iff $$b=x$$ and $$a \in S$$ or $$b \in S$$ and $$a = F(b).$$ Then we get $$F"S$$ by applying TC to $$x$$ and $$R.$$

(*) Note that my formulation of TC only makes sense under the convention that the transitive closure of a relation is reflexive. Without this convention, then it's not clear we can prove the existence of $$\{x\}$$ from the axioms I specified. Of course, we can prove it exists from Separation and Power Set, which is included in the axioms listed in the question, but that feels overpowered for our purposes.

Edit: The question was updated with the intended formalization of the transitive closure schema. My TC here follows from Vladimir's version plus existence of $$\{x\}$$ for all $$x,$$ and the latter follows from Separation and Power Set.

• " Define a relation $R$ by $aRb$ iff $a$ and $b$ are natural numbers and $a=b+1$. Then $\omega$ exists by applying TC to $\emptyset$ and $R$." What are "natural numbers"? Dec 30, 2020 at 6:10
• I'm using the standard definition here. They are finite transitive sets well-ordered by $\in.$ Dec 30, 2020 at 6:58
• Is the definition of the relation for union backwards? It seems you have $x$ as the smallest set in the order, not the largest, so $T$ would just end up being $\{x\}$. (Edit: the same comment applies to the relations for pairing and replacement, so I'm probably missing something.) Dec 30, 2020 at 9:17
• @MarioCarneiro You're right, all three of those were backwards. Dec 30, 2020 at 14:16