Sharp Craig interpolation theorem for $L_{\omega_1 \omega}$

Question

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.

Answer 1

It actually isn't true that the complexity of $\theta$ could be meaningfully bounded in the term of complexities of $\varphi$ and $\psi$.

Let us fix an arbitrary recursive ordinal $\alpha$. Below I sketch a construction of infinitary $\Pi_n$ formulas $\varphi,\psi$, for some finite $n$ such that there are no $\Pi_\alpha$ interpolant for them.

Consider the standard model $\mathbb{N}$ of $\mathsf{PA}$. We fix some $\Delta^1_1$-property $F(X)$ of sets $X\subseteq \mathbb{N}$ that it is not $\boldsymbol\Pi_\alpha$. For example, $F(X)$ could be the property of $X$ to encode an isomorphic copy of $\omega^{\alpha+1}$. Next we fix first-order arithmetical formulas $\varphi'(X,Y)$ and $\psi'(X,Y)$ depending on free unary predicates such that $$F(X)\iff \mathbb{N}\models_2 \exists Y\; \varphi'(X,Y)\iff \mathbb{N}\models_2 \forall Z\; \psi'(X,Z).$$

We put $$\varphi(X,Y) \mathrel{:{=}} \bigwedge \mathsf{Q} \land \forall x \bigvee\limits_{n<\omega} x=S^n(0)\to \varphi'(X,Y)\text{ and}$$ $$\psi(X,Z) \mathrel{:{=}} \bigwedge \mathsf{Q} \land \forall x \bigvee\limits_{n<\omega} x=S^n(0)\to \psi'(X,Z),$$ where $\bigwedge \mathbf{Q}$ is the conjuction of the axioms of Robinson's arithmetic $\mathsf{Q}$. Observe that any interpolant $\theta(X)$ for this pair of $\varphi(X,Y)$ and $\psi(X,Z)$ should express the property $F(X)$ in $\mathbb{N}$. Thus $\theta(X)$ couldn't be a $\Pi_\alpha$ infinitary formula.