Is separation + subset.reflection on transitive sets strong enough to go beyond ZF?

Question

This question is related to this comment, and to this follow up posting.

Working in mono-sorted first order logic with equality and membership:

• Define: $set(x) \equiv_{df} \exists y \, (x \in y)$

• Axiomatize:

1. Extensionality: $(\forall x \, (x \in a \leftrightarrow x \in b) \to a=b)$

2. Separation: $(set(a) \to \exists \ set \ x \, \forall y (y \in x \leftrightarrow y \in a \land \phi))$

3. Reflection: $\forall \ sets \ \vec{p} \ (\phi \to \exists \text { trs } x : set(x) \land \phi^x)$

Where $``\text { trs }"$ stands for transitive, to mean closure under membership $\in$ relation; and where formula $\phi$, only has $\vec{p}$ as its free variables, that doesn't use $``x"$ in both schemata; $\phi^x$ is the formula obtained from $\phi$ by merely bounding all of its quantifiers by $``\subseteq x"$.

Now clearly this would prove all axioms of $\sf ZF-Reg$! I'm not sure if it is stronger than $\sf ZF$ and of the strength described in Page 6 of this article, hence this question is about if that is the case?

Answer 1

Call this new axiom system $K$.

First, note we can augment the reflection scheme to

$$ \exists x (trans(x) \land set(x) \land (\phi \iff \phi^x))$$

By simply doing case analysis on whether $\phi$ or $\neg \phi$ is true and applying the reflection principle in either case.

Now recall the class comprehension scheme of MK, which consists of all the axioms $A_\phi$ of the form

$$\forall \vec{P}\exists M (\forall x (set(x) \land \phi(\vec{P}, x) \iff x \in M))$$

For any formula $\phi(\vec{P}, x)$ (where $M$ does not appear). I claim each $A_\phi$ is provable from $K$.

For consider some transitive set $t$ such that $A_\phi$ is absolute for $t$. We wish to prove $A_\phi^t$. This formula becomes

$$\forall \vec{P} \subseteq t \exists M \subseteq t (\forall x \in t (\phi^t(\vec{P}, x) \iff x \in M))$$

Take some $\vec{P} \subseteq t$. Then such an $M$ exists by the separation axiom scheme. So we have proved the class comprehension scheme.

With the class comprehension scheme in hand, we can prove the consistency of ZF - Reg in a straightforward way. This is because we can develop the model theory of class-sized models and prove $V \models ZF - Reg$. We can then prove the soundness theorem for class-sized models to conclude that $ZF - Reg$ is consistent.

Answer 2

Let A0 be the set of axioms consisting of 1 and those in 2. Let A1 be the set of axioms in 1, those in 2, and those in the original 3(quantifiers not restricted to "sets"). Let A2 be the set of axioms consisting those in 1, 2 and 3. We will show that A1 is inconsistent and Con(A2) is provable in ZF.

(a)(A0)Suppose ∀(∈-->∈) and set(b).

Then set(a).

Proof: From 2, there is a set c with x∈c<-->(x∈b∧x∈a).

(b) A1 is inconsistent.

Proof:Suppose that there is a b and ¬set(b).

Then ∃d(d=b).

By original 3, there is a transitve x such that ∃d(d⊆x∧d=b).

By (a), set(b). Therefore ∀b∃c(b∈c). By 3, there is a transitive x such that ∀b(b⊆x-->∃c(c⊆x∧b∈c). Therefore x∈x. By 2, there is a d such that ∀y(y∈d↔y∈x∧y∉y). Since d⊆x, there is a c⊆x, such that d∈c.

Consequently d∈x andthus d∈d<-->d∉d.

(c) Con(A2) is provable in ZF.

Proof:Let F(f,n,x1,x2,...,xn) be a formula which says "f is a formula with n free variables holds" and there is an ordinal α such that "f(x1,x2,...,xn) holds in V(α+1)".

Let r be a limit ordinal which reflects F. That is for ∀f,n,x1,x2,...,xn∈Vr("F(f,n,x1,x2,...,xn) holds in Vr"<-->F(f,n,x1,x2,...,xn)).

1 holds in V(r+1). If " is a formula" holds and a,x1,x2,...xm∈V(r+1), then there is a x such that ∀(∈↔∈∧"(y,x1,x2,...,xm) holds in V(r+1)").

Such an x must be in V(r+1). Therefore "2 holds in V(r+1)" holds.

To verify "3 holds in V(r+1)" holds, suppose x1,x2,...,xn∈Vr, "f is a formula with n free variables holds" and "f(x1,x2,...,xn) holds in V(r+1)".

Then F(f,n,x1,x2,...xn) holds. By reflection

"F(f,n,x1,x2,...,xn) holds in Vr".

That is there is a t∈r such that "f(x1,x2,...,xn) holds in V(t+1)".

Thus "3 holds in V(r+1)" holds. Since the statement "A2 holds in V(r+1)" holds, we have Con(A2).