I encountered the following problem in Ash&Knight's Computable Structures and the Hyperarithmetical Hierarchy, Theorem 10.9 (slightly rephrased):
TFAE for a computable structure $A$ with a further relation $R$:
- In all copies $B$ of $A$, if $R$ is $\Sigma^0_\alpha(B)$, then so is $\neg R$.
- $\neg R$ is definable in $A$ by a computable formula of the form $$\varphi(\bar c,\bar x):=\bigvee_i \exists\bar u_i(\psi_i(\bar c,\bar x,\bar u_i)\wedge\rho_i(\bar c,\bar x,\bar u_i))$$ where each $\psi_i$ is computable $\Pi_\beta$ for some $\beta<\alpha$ and does not involve $R$; and $\rho_i$ is a finite conjunction of positive atomic formulas involving $R$.
It's clear that 2 implies 1. For the nontrivial direction, I have trouble proving it even for $\alpha=1$. I am unable to define a notion of forcing that produces a copy in which $R$ is $\Sigma^0_\alpha$, without disturbing the formula complexity of the forcing relation (which will presumably correspond to the complexity for $\psi_i$), by trying to modify the forcing poset.
Is there a way to define the forcing poset properly (say for $\alpha=1$ for a start)? Or is there a way to define some clever structure $A'$ containing information on $R$, and somehow applying Theorem 10.1 ($\Sigma_\alpha^0$-definability of $R$ in all copies of $A$ is equivalent to image of $R$ always being $\Sigma_\alpha^0$ in the copy) to $A'$ gives exactly this theorem?