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

1 Answer

This theory is consistent since NBG proves this form of reflection and the rest of axioms are either axioms or theorems of MK, so this theory is a subtheory of MK. Now to establish the other direction of equivalence with MK, we note that Extensionality, Pairing, Boolean union, Set Union, Power, Infinity and Separation all are easily provable using reflection, subsetting, and comprehension, what needs to be proved is Kelley's axiom of Substitution.

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.