Ideal OCF
\(\kappa\) is hereditarily \(\Pi_n\)-reflecting if and only if it is \(\Pi_n\)-reflecting or \(\Pi_m\)-reflecting on the hereditarily \(\Pi_n\)-reflecting ordinals.
\(C_\kappa(\alpha)\) is the closure of \(\kappa\cup{\text{least }\Pi_n\text{-reflecting}\mid n>1}\) under \(\beta,\gamma\mapsto\beta+\gamma\) and \(\beta,\gamma,\delta\mapsto\chi_\beta(\gamma,\delta)\) provided \(\gamma<\alpha\).
Suppose \(\kappa\) is \(\Pi_{n+1}\)-reflecting (\(n>0\)) but not \(\Pi_{n+2}\)-reflecting. Then set \(\mathcal A_\kappa^\alpha\) to be the set of \(\pi<\kappa\) such that:
- If \(\lambda\) is \(\Pi_{n+2}\)-reflecting, \(\beta,\gamma\in C_\pi(\alpha)\cap\alpha\), and \(\kappa\) is \(\Pi_{n+1}\)-reflecting on \(\mathcal A_\lambda^\beta\), \(\pi\) is \(\Pi_n\)-reflecting on \(\mathcal A_\lambda^\beta\cap A_\kappa^\gamma\).
- If \(\lambda\) is hereditarily \(\Pi_{n+2}\)-reflecting, \(\beta\in C_\pi(\alpha)\cap\alpha\), and \(\kappa\) is \(\Pi_m\)-reflecting on \(\mathcal A_\lambda^\beta\), then \(\pi\) is \(\Pi_m\)-reflecting on \(\mathcal A_\lambda^\beta\).
- \(C_\pi(\alpha)\cap\kappa=\pi\).
Define \(\chi_\kappa(\alpha,\beta)=\operatorname{enum}(\operatorname{cl}(\mathcal A_\kappa^\alpha))(\beta)\). Define \(\psi_\kappa(\kappa^{\alpha_1}_{\beta_1}+\ldots+\kappa^{\alpha_n}_{\beta_n})=\chi_\kappa(\alpha_1,\chi_\kappa(\alpha_2,\chi_\kappa(\ldots)+\beta_2)+\beta_1)\).