Return to Answer

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). 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}$:

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 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.

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). However, the example above is fairly flexible, and yields a couple nice generalizations with no additional work.

Most easily, we can show a weak "non-collapsing" result. Suppose $(\mathfrak{A}_i)_{i\le n}$ is a sequence of structures such that $\mathfrak{A}_0=\mathfrak{N}$ and $\mathfrak{A}_{i+1}$ is an expansion of $\mathfrak{A}_i$ by finitely many relations implicitly definable (in the sense of the OP) over $\mathfrak{A}_i$. Then we can nontrivially keep going: there is a relation $R$ on the top structure $\mathfrak{A}_n$ which is implicitly definable but not explicitly definable over $\mathfrak{A}_n$. I would be interested in a proof of this result which did not go through forcing. At the same time (and contra an earlier foolish claim of mine), it's worth noting that we also have a "collapsing" result: everything i.d. over an expansion of $\mathbb{N}$ by hyperarithmetic predicates is again hyperarithmetic, and every hyperarithmetic relation is already i.d. over $\mathfrak{N}$.

But in my opinion the neatest thing about this approach is its generalization to arbitrary "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}$:

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}$.

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). 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 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 that doesn't contradict the previous paragraph.

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). 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 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.

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). 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 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.

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). 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 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 that doesn't contradict the previous paragraph.