Skip to main content
1 of 8
Noah Schweber
  • 21.1k
  • 10
  • 110
  • 331

Here is the example mentioned in the OP:

Take as our "base structure" $\mathcal{N}=(\mathbb{N};+,\times)$, and let $A$ be the truth predicate for $\mathcal{N}$ (relative to some appropriate Godel numbering). The Tarskian definition of truth shows that $A$ is implicitly definable over $\mathcal{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.)

Noah Schweber
  • 21.1k
  • 10
  • 110
  • 331