Is it possible to formalize iterative reflection in FOL, and what is its strength?

61 Views Asked by At

I'll largely present this posting informally, because I'm not certain if it can be done formally in the language first order logic with identity and membership.

What I want to do is to iterate reflection, the form I'm concerned with is that following:

$$\forall \vec{w} \ \exists \alpha: \varphi(\alpha) \land [\psi \to \psi^{V_\alpha}]$$

Now the idea is change $\varphi$, so we are to have for example formulas $\varphi_0,\varphi_1, \varphi_2,...$, now each formula $\varphi_{i+1}$ is to be defined in terms of $\varphi_i$, more specifically I want $\varphi_{i+1}$ to say that $\alpha$ is a rank of a universe of a theory having axioms: Extensionality, Separation, and reflection...up to $\varphi_i$, the latter is all instances of the following up to $n=i$: $$\forall \vec{w} \ \exists \alpha: \varphi_n(\alpha) \land [\psi \to \psi^{V_\alpha}]$$ for example we begin with $\varphi_0$ to be "is ordinal", now I expect $\varphi_1$ to be "is inaccessible", while $\varphi_2$ to be "is hyper-inaccessible", etc...

Can this be formalized in first order logic?

If this can be done, can we extend the indexing of the $\varphi$'s [through using ordinal notations] as to include all recursive ordinals (i.e. ordinals below $\omega_1^ {CK})$? And in this case how can one define the $\varphi_i$'s when $i$ is a limit?

If the above can be done, what would be the strength of this iterative reflection?