Write a relatively simple, recursive claim in arithmetic which is equivalent to defining truth.
For example: Define $f(x):\Bbb{N}\to\Bbb{N}$ such that if we set:
$x_{n+1}=f(x_n)$
Then any proof of the claim:
$\forall x\in\Bbb{N}, \exists m\in\Bbb{N}:x_m=1$
would break Tarski's indefinability of truth.
Okay, in response to Gerry's comment I'm expanding the background behind this question; perhaps against my better judgement; but here it is... The Collatz graph is closely related to iteration of the left and right transforms $T_L(x)=2x-1$ and $T_R(x)=2x+1$ on the odd integers.
Now these transforms on iteration are sufficient to construct every odd integer from the number $1$. Furthermore if we use the very similar transforms $T_{L2}(x)=x-2^{v_2(x)-1}$ and $T_{L2}(x)=x+2^{v_2(x)+1}$ we can construct the dyadic rationals modulo $1$ from the starting integer $0$ - in fact this generates both the positive and negative dyadic rationals modulo $\pm1$, i.e. $\pm1\times\Bbb{Z}(2^{\infty})$. Now it turns out the Collatz conjecture has a natural extension which is situated in the Prufer 2-group $\Bbb{Z}(2^{\infty})$, and this also reflects perfectly into $-\Bbb{Z}(2^{\infty})$
So the question I'm left asking myself, when I wonder what provability theory says about Collatz conjecture, is whether this iterative process of constructing the integers from $1$ "looks like" in a "homotopy type theory" sense, some theorem which states that its own solution is impossible.
My curiosity is further piqued by a) this process is an infinitely recursive process and b) Proof of the Collatz conjecture seems to rely on the the failure of the Prufer 2-group to be Noetherian. This puts the "final set" of odd integers beyond reach in a special way which renders the entire Collatz graph incomplete without the "final set". So there is a sense in which recursion can never get you to a proof - which I'm interpreting as saying; you need to transcend recursion and consider the overall properties of the Prufer 2-group. And again, I see similarities with what little I know of provability theory; namely the fact that a diagonal argument is used which could be analogous to the Prufer 2-group not being noetherian.
Trouble is; while I know the Collatz Conjecture intimately, knowing much about provability and decidability is a million miles away for me right now. But if I can "see" what such a recursive process looks like in an unprovability/undecidability proof I might recognise which, if any, of the objects in it might correspond to the thing I'm studying, and how the "not attainable by recursion" problem (or more precisely; $\Phi(\Bbb{Z}(2^{\infty}))=\Bbb{Z}(2^{\infty})$ where $\Phi$ is the Frattini Subgroup and recursion is the repeated application of some map from the smallest subgroup containing $x$ to an element strictly of some supergroup thereof) may have been overcome elsewhere.
I think you're making a bit of a category error. The undefinability of truth is not about proofs at all, or indeed any axiomatic system in any way: it's about the structure $\mathcal{N}=(\mathbb{N}; +,\times,0,1)$. Specifically, any formula $\varphi(x)$ in one variable in the language of arithmetic defines the set $$\varphi^\mathcal{N}=\{n\in\mathbb{N}: \mathcal{N}\models\varphi(n)\}.$$ Tarski's theorem says that the set $TA$ of Godel numbers of sentences true in $\mathcal{N}$ is not definable; that is, $$TA\not=\varphi^\mathcal{N}$$ for any one-variable formula $\varphi$ in the language of arithmetic.
Note that there is no "background theory" here; Tarski's theorem says something about the complexity of a particular set of natural numbers. In purely computability-theoretic language, Tarski's theorem says $$\mbox{For all $n\in\mathbb{N}$, we have }TA\not\le_T {\bf 0^{(n)}}.$$
Now what you're asking for essentially is a situation where a proof of a sentence $\psi$ would yield a definition of a particular set of natural numbers. But this isn't really a thing that happens. In fact, there's a clear mismatch here: a proof takes place within an axiom system, whereas a definition takes place inside a structure, and our structure isn't changing here (it's just $\mathcal{N}$).
In general, the existence of a proof of a statement from a theory doesn't give you a definition of a set in a structure; they're just different kinds of objects. Of course, a proof of a statement from a theory can tell you that the theory proves some important fact about a definition, but that definition was (if it existed at all) pre-existing. So the point is that there's no real way to leverage Tarski's theorem to do the sort of thing you want it to.
In principle, the following could occur:
You have some sort of object you want to prove doesn't exist.
You show that if such an object does exist, then there is a definable such object.
You show that relative to any such object, you can define truth.
Combining the second and third bulletpoints above and using Tarski's theorem, we've accomplished the goal set out in the first bulletpoint.
I am, however, not aware of a single case where this approach has been used successfully (well, I can cook up a couple artificial ones, but they are better solved with other means anyways).