For a logic $\mathcal{L}$, say that a cardinal $\kappa$ is $\mathcal{L}$-correct iff every satisfiable $\mathcal{L}$-theory of size $<\kappa$ has a model of size $<\kappa$. First-order correctness is of course boring, but quite quickly we enter the realm of strong large cardinal properties (see e.g. here).

I'm interested in a kind of "iterated correctness:" repeatedly add to a given logic the ability to quantify over cardinals which are correct for it (or rather, for the previous iteration of this process). This doesn't make obvious sense in general, but for logics with reasonably nice syntax things are better. In particular, I'm interested in what happens when we iteratively "add correctness quantifiers" to second-order logic, as follows:

Let $\mathcal{L}^2_0$ be usual second-order logic, and let $\mathcal{L}^2_{n+1}$ be $\mathcal{L}_n^2$ augmented with a quantifier $$\mathsf{C}_nx\varphi(x)\equiv\mbox{the set of $x$ satisfying $\varphi$ is $\mathcal{L}^2_n$-correct.}$$ So $\mathcal{L}^2_k$, in addition to the usual logical symbols, has $k+2$ different types of quantifier: the first-order quantifiers, the second-order quantifiers, and $k$-many correctness quantifiers. These quantifiers can alternate however is desired.

My question is:

Do any of the "usual" large cardinal properties imply $\mathcal{L}^2_n$-correctness for every $n$?

This is not at all obvious to me. On the other hand, I can't pin down a concrete obstacle to e.g. supercompactness having the above property.

For a logic $\mathcal{L}$, say that a cardinal $\kappa$ is $\mathcal{L}$-correct iff every satisfiable $\mathcal{L}$-theory of size $<\kappa$ has a model of size $<\kappa$. First-order correctness is of course boring, but quite quickly we enter the realm of strong large cardinal properties (see e.g. here).

I'm interested in a kind of "iterated correctness:" repeatedly add to a given logic the ability to quantify over cardinals which are correct for it (or rather, for the previous iteration of this process). This doesn't make obvious sense in general, but for logics with reasonably nice syntax things are better. In particular, I'm interested in what happens when we iteratively "add correctness quantifiers" to second-order logic, as follows:

Let $\mathcal{L}^2_0$ be usual second-order logic, and let $\mathcal{L}^2_{n+1}$ be $\mathcal{L}_n^2$ augmented with a quantifier $$\mathsf{C}_nx\varphi(x)\equiv\mbox{$\vert\{x: \varphi(x)\}\vert$ is $\mathcal{L}^2_n$-correct.}$$ So $\mathcal{L}^2_k$, in addition to the usual logical symbols, has $k+2$ different types of quantifier: the first-order quantifiers, the second-order quantifiers, and $k$-many correctness quantifiers. These quantifiers can alternate however is desired.

My question is:

Do any of the "usual" large cardinal properties imply $\mathcal{L}^2_n$-correctness for every $n$?

This is not at all obvious to me. On the other hand, I can't pin down a concrete obstacle to e.g. supercompactness having the above property.