Let $Q(\vec x, \vec y) \subseteq \mathbb Z^n \times \mathbb Z^n$ be a relation which can be represented in presburger arithmetic.
Let $R(\vec x, \vec y) \equiv Q \cup (Q \circ Q) \cup (Q \circ Q \circ Q) \dots\subseteq \mathbb Z^n \times \mathbb Z^n$ be the transitive closure of the relation $Q$.
We now ask for an oracle \begin{align*} &O: \texttt{PresFormula} \to \texttt{PresFormula} \cup \{ \texttt{noformula}\}\\ &O(\texttt{presforumla}(Q)) = \begin{cases} \texttt{presforumla}(R) & \text{if $R$ is expressible in presburger arithmetic} \\ \texttt{noformula} & \text{otherwise} \end{cases} \end{align*}
That is, the oracle $O$ on input the presburger forumla for $Q$, halts and returns the presburger formula for $R$ if such a formula exists. $O$ halts and returns a unique token $\texttt{noformula}$ if a presburger formula for $R$ does not exist.
What properties does $O$ have? is it computable? what is the complexity of this $O$ if it is computable? If it is uncomputable, are there weaker variants of this which is computable? I want something that's equal to $O$, and if this is not possible, the strongest possible oracle available.
I know that not all presburger arithmetic formulas have transitive closure that is not in presburger arithmetic: Kelly and Pugh, 1996.