What is the consistency strength of adding this ordinal reflection scheme on top of Ackermann set theory?

Question

Axiom scheme of Ordinal Reflection: if $\phi$ is a formula that doesn't use the symbol $V$, whose parameters are among $x_1,..,x_n$; then: $$\forall x_1 \in V,\dotsc,\forall x_n \in V: \phi(On) \to \\\forall c \subseteq On \\ (c=\{\alpha \in On| \phi(\alpha)\} \lor \bigcup( c) = On \to |c|=On);$$ is an axiom.

Where: $$On=\{\alpha \in V|\operatorname{ordinal}(\alpha)\};$$ and "$|c|$" stands for cardinality of class $c$, defined as the least von Neumann ordinal class bijective to $c$.

Add this axiom on top of Ackermann's set theory.

What would be the consistency strength of the resulting theory?

Answer 1

The schema (if 𝜙 is a formula that doesn't use the symbol 𝑉, whose variables are among 𝑥1,..,𝑥𝑛; then: ∀𝑥1∈𝑉,…,∀𝑥𝑛∈𝑉:𝜙(𝑂𝑛)→|{𝛼∈𝑂𝑛|𝜙(𝛼)}|=On) is provable in Ackermann's set theory plus foundation. To see this suppose
𝜙 is a formula that doesn't use the symbol 𝑉, whose variables are among 𝑥1,..,𝑥𝑛; and ∀𝑥1∈𝑉,…,∀𝑥𝑛∈𝑉:𝜙(𝑂𝑛). Suppose that there was an ordinal d∈On such that 𝛼∈𝑂𝑛 and 𝜙(𝛼) implies 𝛼∈d. Then On would be definable(for suitable definition of ordinal) as the least ordinal x such that 𝜙(x) and d∈x. Since this is impossible, ⋃{𝛼∈𝑂𝑛|𝜙(𝛼)}=On. Let F(x,y) be a formula which "says" x and y are ordinals and 𝜙(y) and the order type of {𝛼∈y|𝜙(𝛼)}=x. Suppose F(b,On) holds for some b∈On. Then On is definable, which is impossible. Therefor the order type of {𝛼∈𝑂𝑛|𝜙(𝛼)} is On.

Ackermann's set theory plus foundation plus ∀𝑐⊆𝑂𝑛(⋃(𝑐)=𝑂𝑛→|𝑐|=𝑂𝑛) proves Con(ZF). To see this note that this theory proves the formula "L(On) satisfies ZF".