Closure principle

First I'll speak about the general idea, which bears some remote resemblance to the idea of dropping of type indices in some type related theories, like when stratification drops the type indices, actually even the traditional set theories of Z and ZF can be interpreted in extensions of type related theories with a drop of indices. The idea here is generally similar but on another technical aspect.

The idea here is that if a property is closed over every HℵαHℵα set, then this property is closed over the whole set realm! Closure over a HℵαHℵα set here means that if the formula ϕϕ defining that property has all of its quantifiers bounded in HℵαHℵα then every subset yy of HℵαHℵα for which ϕϕ holds would be an element of HℵαHℵα if all parameters in ϕϕ are elements of HℵαHℵα. So this mean that closure of predication over the set world can be envisioned as paralleling closure over all infinite hereditary size sub-worlds. I'm not sure if this is provable in MK, or even if a version of it suitable for ZFC is provable in ZFC. But this, if consistent, does supply some envisioning on predication within these standard set theories. For example one can have an equivalent formulation of MK by the following axioms that extends mono-sorted first order logic with identity and membership.

• 1. Extensionality: ∀x,y(∀z(z∈x↔z∈y)→x=y)∀x,y(∀z(z∈x↔z∈y)→x=y)

  2. Class comprehension schema: if ϕϕ is a formula in which x doesn't occur free, then (∃x∀y(y∈x↔∃z(y∈z)∧ϕ))(∃x∀y(y∈x↔∃z(y∈z)∧ϕ)) is an axiom.

Define (VV): x=V⟺∀y(∃z(y∈z)→y∈x)x=V⟺∀y(∃z(y∈z)→y∈x)

• 1. Pairing: ∀a,b∈V∃x∈V ∀y(y∈x↔y=a∨y=b)∀a,b∈V∃x∈V ∀y(y∈x↔y=a∨y=b)

  2. Infinity: ∀x∈V[∀y∈x(y<<x)→x∈V]∀x∈V[∀y∈x(y<<x)→x∈V]

Where "<<" signifies "hereditarily strictly subnumerous to", defined as:

y<<x⟺∃z[y∈z∧∀a,b(a∈z∧b∈a→b∈z∧a<x)]y<<x⟺∃z[y∈z∧∀a,b(a∈z∧b∈a→b∈z∧a<x)]

Where "<" is "strictly subnumerous to" defined in the usual manner.

• 1. Closure schema: If ϕ(x,y)ϕ(x,y) is a formula in which only symbols ‘‘x,y"‘‘x,y" appear free, and only appear free, then:

∀α(ordinal(α)∧α∈V→∀x∈Hℵα[∀y⊆Hℵα(ϕHℵα(x,y)→y∈Hℵα)])→∀x∈V ∀y[ϕV(x,y)→y∈V]

Where HℵαHℵαis the set of all sets hereditarily strictly subnumerous to ℵαℵα; and ϕbϕb means the formula ϕϕwith all of its quantifiers bounded by bb, i.e., all of its quantifiers are of the form ∀x∈b;∃x∈b∀x∈b;∃x∈b.

/ theory definition finished.

I think a parallel approach to derive ZFC would be to have Z with infinity axiom written as ∀x∃Hx∀x∃Hx, and add to it the following schema:

∀α(ordinal(α)→∀x∈Hℵα∃y∈Hℵα(ϕHℵα(x,y)))→∀x∃y(ϕ(x,y))

The question is: had that approach been investigated before? Or at least part of it or a similar parallel idea had been investigated before?