Can we always "sharpen" interpretations? For the purposes of this question, a $T$-interpretation with arity $n$ will be a tuple $\Phi=(\delta,\eta,F)$ where

*

*$\delta$ and $\eta$ are individual formulas of arity $n$ and $2n$ respectively,


*$T$ proves that $\eta$ defines an equivalence relation on the set picked out by $\delta$, and


*$F$ is a (possibly infinite) set of formulas each of which has arity a multiple of $n$ such that for each $\varphi(x_1,...,x_{kn})\in F$ we have that $T$ proves that $\varphi$ is $\eta$-invariant on $\delta$.
Say that $\Phi=(\delta,\eta, F)$ is sharp in $T$ iff - letting $\Sigma$ be a language with a $k$-ary relation symbol corresponding to each $kn$-ary formula in $F$ - the following "substitution" principle holds:

If $\mathcal{A}$ is a $\Sigma$-structure satisfying (the translation to $\Sigma$ of) every sentence $T$ proves about $\Phi$, then there is some $\mathcal{B}\models T$ with $\Phi^\mathcal{B}\cong\mathcal{A}$.

It's easy to show that not all interpretations are sharp. However, I don't have a good sense of how rare sharpness is, especially in "rich" theories like $T=\mathsf{ZFC}$ or $T=\mathsf{PA}$. The following seems like a natural question to get a better understanding of this:

Suppose $\Phi=(\delta,\eta,F)$ is a $\mathsf{ZFC}$-interpretation. Must there be a set of sentences $G\supseteq F$ and a consistent extension $T\supseteq\mathsf{ZFC}$ such that $(\delta,\eta,G)$ is sharp in $T$?

I suspect the answer is negative, even if we restrict attention throughout to countable models, but I don't see how to prove this. (I also vaguely recall a paper on this topic from the 80s, maybe by Friedman or Mostowski, but I can't track it down.)
 A: If you allow to add to an interpretation infinitely many predicate symbols (infinite $G\setminus F$) then any interpretation in $\mathsf{ZFC}$ could be extended to a sharp interpretation in $\mathsf{ZFC}+L=V$. So you original question has a positive answer.
However, if you restrict your attention to extensions by finitely many predicate symbols then it wouldn't be possible to extend some interpetations in $\mathsf{ZFC}$ to sharp interpretations. But actually all interpretations in $\mathsf{PA}$ admit finite extension to a sharp interpretation in some extension of $\mathsf{PA}$.
Now let me sketch the proofs of the claims that I mentioned.
Since in $\mathsf{ZFC}+V=L$ any interpretation is definably isomorphic to a one-dimensional interpretation with absolute equality, without loss of generality I'll assume that I am given a one-dimensional iterpretation $\Phi$ with absolute equality in $\mathsf{ZFC}+V=L$. Let the interpretation $\Phi'$ extend $\Phi$ by all possible relations on the domain of interpretation that are definable in set-theoretic language. Any model $\mathcal{M}$ satisfying all sentences whose $\Phi'$-translations are $\mathsf{ZFC}+V=L$-provable, contains a complete first-order theory in the language with parameters from $\mathcal{M}$ of a set-theoretic universe that should lead to $\mathcal{M}$ as the result of application of $\Phi'$. Since $\mathsf{ZFC}+V=L$ admits definable Skolem functions, we could recover from $\mathcal{M}$ a model $\mathcal{A}$ of $\mathsf{ZFC}+L=V$ that leads to $\Phi'^\mathcal{A}$ being an isomorphic copy of $\mathcal{M}$, by constructing it as a model consisting exactly of the definable sets with parameters from $\mathcal{M}$.
If we look just on the extensions of interpretations by finitely many relations, then the point is that set-size interpretations in non-$\omega$ models of $\mathsf{ZFC}$ always lead to recursively-saturated models. And for example, it is easy to see that for any finite extension $\Phi'$ of the standard interpretation of arithmetic in $\mathsf{ZFC}$ and any consistent $T\supseteq \mathsf{ZFC}$, we always will have non-recursively saturated, non-$\omega$ model of all sentences whose $\Phi'$-translations are $T$-provable.
For interpretations in $\mathsf{PA}$ we could exploit the dichotomy that in the standard model the domain of the interpretation is either finite or definably isomorphic to the set of naturals. And hence for a given interpretation $\Phi$ in $\mathsf{PA}$ provably in an appropriate extension $T$ of $\mathsf{PA}$, we have a parameter-free definable bijection between the domain of $\Phi$ and either a standard natural $n$ or the class of all elements. In the case of the finite domain there is nothing to prove. In the case of the domain isomorphic to all naturals, we simply expand the interpretation by the addition and multiplication.
