# Is this theory equivalent to MK?

[EDIT] The older exposition of this theory was proved inconsistent by EmilJeřábek (see comments). Here, this is a possible salvage. (the new information over the older post shall be put in square brackets)

Working in mono-sorted FOL with equality and membership, add the following axioms:

Define: $$set(y) \iff \exists z: y \in z$$

If formula $$\phi$$ does not use $$x"$$, then:

1. Comprehension: $$(\exists! x \ \forall y \ (y \in x \leftrightarrow set(y) \land \phi))$$

Define: $$x=V \iff \forall y: set(y) \to y \in x$$

1. Reflection: $$(\phi \to \exists \text { transitive } x \in V: \phi^x)$$;

Where $$\phi$$ is a formula that does not use $$x"$$ [having all of its quantifiers bounded by $$V$$], $$\phi^x$$ is the formula obtained by merely replacing all bounding occurrences of $$V$$ in $$\phi$$ by $$x$$; "transitive" is defined as a class whose elements are subsets of it.

1. Subsetting: $$x \in V \land \forall y \in A (y \subseteq x) \to A \in V$$
2. Global Choice: For every nonempty class $$X$$ of pairwise disjoint sets, there is a class having singleton intersection with each nonempty element of $$X$$.
3. Foundation: $$\exists y \,(y \in X) \to \exists y \in X \, (y \cap X = \emptyset)$$

So the question is:

Is the above theory consistent? Is it equivalent to $$\small \sf MK$$?

• The first question that we will have to answer is whether this theory proves the axiom of extensionality. Nov 7, 2021 at 11:04
• I think extensionality follows from the uniqueness in the Comprehension axiom: If $\forall x(x\in a \leftrightarrow x\in b)$, both $a$ and $b$ satisfy $\forall y(y\in c\leftrightarrow set(y)\wedge y\in x)$ (because all members of $a$ or $b$ are sets by definition) (replacing $x$ with $a$ or $b$). Because such an $x$ is unique, $a=b$. Nov 7, 2021 at 11:50
• @ArvidSamuelsson, yes, repeating what Hannes Jakob commented, it does prove Extensionality over all classes. Take any class $A$, let $\phi$ be $y \in A$, then by Comprhension, there exists a unique class $x$ that have the same elements of $A$, thereby proving Extensionality. Nov 7, 2021 at 13:18
• If it’s really any formula, then the schema is obviously inconsistent: e.g., let $\phi$ be $\forall y\,\forall z\,(y\in z\to\exists v\in V\,v=y)$, in which case reflection gives $\exists x\in V\,\forall y\,\forall z\,(y\in z\to\exists v\in x\,v=y)$, i.e., "there is a universal set”. Nov 8, 2021 at 19:21
• Possibly. I didn’t check the other axioms in either way, but if all quantifiers of $\phi$ are bounded by $V$, then this form of reflection is provable in NBG. Nov 9, 2021 at 14:14

Now let $$F$$ be a class function, whose domain is the set $$d$$, then reflect on the formula $$\exists k \in V: k=d \land \forall m \in V (m \in k \to \exists y \in V: y=F(m))$$, obviousely from parameters $$F,d$$; and we get the range of $$F$$ being a subclass of some transitive set, and by separation it would be a set, thus proving Substitution.