Here is the example mentioned in the OP: Take as our "base structure" $\mathfrak{N}=(\mathbb{N};+,\times)$, and let $A$ be the truth predicate for $\mathfrak{N}$ (relative to some appropriate Godel numbering). The Tarskian definition of truth shows that $A$ is implicitly definable over $\mathfrak{N}$, explicit-indefinability notwithstanding. Now we construct a set $B$ which is computable (so a fortiori extrinsically definable, so a f. intrinsically definable) relative to $A$ but not implicitly definable. Specifically, $A$ computes an $f\in 2^\omega$ which meets every dense arithmetically definable subset of $2^{<\omega}$. Such an $f$ cannot be an arithmetical singleton, since by "forcing=truth" every arithmetical property holding of $f$ also holds of all arithmetically generic reals extending $f\upharpoonright n$ for some finite $n$. (Note that a bit of care is needed here: we need to pay attention to the amount of genericity required for "forcing=truth," e.g. it would be a problem if we needed to meet *hyperarithmetic* dense sets to force arithmetical properties. But in fact everything balances out here.) **** Admittedly, this example isn't very elementary or natural. This is especially true in light of [the non-implicit definability of the set of primes over $(\mathbb{N};\mathsf{succ})$ (observed by Pakhomov)](https://mathoverflow.net/a/426382/8133). However, the example above does have a rather nice feature in my opinion: it gives a general result about "nice" logics. Specifically, we can ask an analogue of this question for any abstract logic in place of $\mathsf{FOL}$. Now broadly speaking, the above only used two properties of $\mathsf{FOL}$: - That there is a structure (here, $\mathfrak{N}$) which "appropriately captures" the syntax and semantics of the logic in question. - That "forcing=truth" holds in an appropriately local way. Provocatively, but not (in my opinion) inaccurately, we can take away from this that **any logic for which implicit definability *is* transitive must have some fairly nasty properties**. I think that's neat - at first glance I would have assumed that transitivity of definability variants is a good thing to have, but this shows that that's dubious at best. (Or, perhaps more positively as far as the logic is concerned, if $\mathcal{L}$ *is* a "nice" logic and implicit definability is transitive "over the base structure $\mathfrak{A}$," then that structure $\mathfrak{A}$ must be very bad at talking about $\mathcal{L}$.) **** On the other hand, the implicit definability hierarchy over $(\mathbb{N};\mathsf{succ})$ *does* collapse! After a couple levels we get all the sets of the form $0^\alpha$ for a computable ordinal (notation) $\alpha$ (in [Sacks' book](https://projecteuclid.org/ebooks/perspectives-in-logic/Higher-Recursion-Theory/toc/pl/1235422631) these are called "$H$-sets" if memory serves). Now since "hyperarithmetic over hyperarithmetic = hyperarithmetic," every set in the implicit definability hierarchy over $(\mathbb{N};\mathsf{succ})$ is hyperarithmetic and so Turing-reducible to some $0^\alpha$. But Turing reducibility (once we have $+$ and $\times$, anyways) gives us explicit definability. We do have a "local non-collapsing" result, namely that for every relation $A$ on $\mathbb{N}$ there is a properly-i.d.-over-$(\mathbb{N};+,\times,A)$ relation (the argument above via truth + forcing works for this), but - while nontrivial as far as I can tell - that doesn't contradict the previous paragraph.