Skip to main content
4 of 8
added 224 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 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}$.)

We also get from the above example that the implicit definability hierarchy over $(\mathbb{N};\mathsf{succ})$ for $\mathsf{FOL}$ doesn't collapse at any finite level (although we have to pay a bit more attention to how we implement a truth predicate); and again, this observation generalizes to appropriate logics and "logic-capturing structures."

Noah Schweber
  • 21.1k
  • 10
  • 110
  • 331