Skip to main content
8 of 8
deleted 31 characters in body
Noah Schweber
  • 21.1k
  • 10
  • 110
  • 331

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

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

Noah Schweber
  • 21.1k
  • 10
  • 110
  • 331