I’d like to know if a sharp version of Craig’s interpolation theorem for $L_{\omega_1 \omega}$ is already known or exists in the literature. By a ``sharp” version of this theorem, I mean one in which if $\phi$ implies $\psi$ then the interpolant $\theta$ is of the same syntactic complexity as $\phi$. For example, if $\phi$ is $\Pi_\alpha$ then $\theta$ is also $\Pi_{\alpha}$.

I am aware of similar “sharp” versions of the Craig interpolation theorem, such as that appearing in this paper, but it is not exactly the kind I need. I am pretty certain the “sharp” version above is true, and would be tedius (but not difficult) to prove using a similar proof to the original interpolation theorem. But it also feels to me like something that is known and likely to have been proven before, and that is what I’m curious about.

I’d like to know if a sharp version of Craig’s interpolation theorem for $L_{\omega_1 \omega}$ is already known or exists in the literature. By a “sharp” version of this theorem, I mean something like the following statement: if $\phi$ implies $\psi$ then the interpolant $\theta$ is of the same syntactic complexity as $\phi$. For example, if $\phi$ is $\Pi_\alpha$ then $\theta$ is also $\Pi_{\alpha}$.

I am aware of similar “sharp” versions of the Craig interpolation theorem, such as that appearing in this paper, but it is not exactly the kind I need. I am pretty certain the “sharp” version above is true, and would be tedius (but not difficult) to prove using a similar proof to the original interpolation theorem. But it also feels to me like something that is known and likely to have been proven before, and that is what I’m curious about.