Is there a simple instance of intransitivity for implicit definability?

Question

This question continues the theme of some recent questions on implicit definability.

A relation $R$ is implicitly definable in a first-order structure $M$ if there is a property $\varphi(\dot R)$, expressible in an expansion of the language with a new relation symbol $\dot R$, such that $R$ is the only relation on $M$ for which $\langle M,R\rangle$ satisfies $\varphi(\dot R)$. That is, $R$ is implicitly definable if it has a property with respect to the other structure of $M$ that only it has.

The main original question was whether implicit definability is transitive.

Main Question 1. Is the implicitly-definable-over relation transitive? That is, if $R$ is implicitly definable over $M$ and $S$ is implicitly definable over the expansion $\langle M,R\rangle$, is $S$ implicitly definable over $M$?

I had expected not, and asked Is multiplication implicitly definable from successor? with the idea that addition is easily seen as implicitly definable over successor, and multiplication is easily seen as implicitly definable over addition, but I didn't see initially that multiplication would be implicitly definable over successor. This turned out, however, not to be a counterexample, because multiplication is in fact implicitly definable from successor, as shown in the answers to that question.

The accepted answer to that question shows that we shall not violate transitivity with an example in which $R$ is definable from $S$ over $M$.

With that insight, Geoffrey Irving asked Is the set of primes implicitly definable from successor? which proposes that the set of primes might be a counterexample, since multiplication is implicitly definable over successor, and primality is explicitly definable over multiplication, but it would seem that primality is not implicitly definable from successor.

In my view, that example is probably correct but also I expect extremely difficult to prove, since we have so few tools for proving instances where a relation is not implicitly definable.

In the interest of finding elementary examples of intransitivity, therefore, let me ask explicitly here.

Main Question 2. What are some elementary examples of intransitivity in the implicitly-definable-over relation?

We want an elementary instance of a structure $M$ with an implicitly definable relation $R$, such that another relation $S$ is implicitly definable over $\langle M,R\rangle$, but $S$ is not implicitly definable over $M$.

Noah Schweber proposed an example in the comments of my previous question, namely, that the standard truth predicate is implicitly definable over the standard model of arithmetic and from that truth predicate we can define a definably-generic Cohen real, but the generic real cannot be implicitly definable on the grounds of homogeneity of the forcing. I am hoping that he will post an answer here providing fuller details.

Currently that is our only example of intransitivity, and I am hoping we can find a truly elementary instance. Please post with any instance of intransivity.

Answer 1

Here is an example with a relatively simple and elementary proof.

Lets say that a set $A$ of natural numbers is universal if for any natural $n$ and a set $a\subseteq n$ there exists $m$ such that $\forall x<n (x\in a\mathrel{\leftrightarrow} x+m\in A)$.

Our goal will be to show that no universal set of naturals is implicitly definable in $(\mathbb{N},S)$.

Let $P$ be the predecessor function.

Theorem. The theory of the class $\{(\mathbb{N},0,S,P,A)\mid A\text{ is a universal unary predicate}\}$ enjoys quantifier elimination.

Proof. In the language of this theory we think of the atomic formulas as having one of the following two forms $x+\underline{n}=y+\underline{m}$ and $\dot A(x+\underline{n})$, where $x,y$ are either variables or the constant $0$ and $n,m$ are integer constants. Here $x+\underline{n}$ is $x$ if $n=0$, is $S^n(x)$, if $n>0$, and is $P^{-n}(x)$, if $n<0$.

It is enough to show that for any quantifier-free formula $\varphi(x_0,\ldots,x_{n-1},y)$ there is a quantifier-free formula $\psi(x_0,\ldots,x_{n-1})$ that is equivalent to $\exists y \;\varphi(x_0,\ldots,x_{n-1},y)$. Indeed, it is easy to see that for sufficiently large $k$ (we could choose $k$ to be the maximum $|m|$ among the terms $z+\underline{m}$ occurring in $\varphi$), the formula $\exists y \;\varphi(x_0,\ldots,x_{n-1},y)$ is equivalent to $$\bigvee\limits_{i<n}\bigvee\limits_{-2k\le j\le 2k}\varphi(x_0,\ldots,x_{n-1},x_i+\underline{j})\lor \bigvee\limits_{a\subseteq [-k,k]} \varphi_a(x_0,\ldots,x_{n-1}),$$ where for $a\subseteq [-k,k]$ the formula $\varphi_a(x_0,\ldots,x_{n-1})$ is the result of the following replacements

1. for $s\in a$ all subformulas of the form $\dot A(y+\underline{s})$ are replaced with truth;
2. for $s\not\in a$ all subformulas of the form $\dot A(y+\underline{s})$ are replaced with falsity;
3. all subformulas $x_i+\underline{s_1}=y+\underline{s_2}$ are replaced with falsity.

QED

Now suppose for a contradiction that some universal $A\subseteq \mathbb{N}$ has an implicit definition $\varphi(\dot A)$ in $(\mathbb{N},S)$. Then we find a quantifier-free $\varphi'(\dot A)$ in the signature with $0$ and predecessor that is equivalent to $\varphi(\dot A)$ over the elementary theory of the class of all models with a universal predicate. Observe that any universal set $A'$ coinciding with $A$ on a long enough initial fragments of naturals would also satisfy $\varphi'(\dot A)$ and hence $\varphi(\dot A)$. So since we could choose $A'$ like this that is not equal to $A$ we observe that $\varphi(\dot A)$ is not a definition of a unique predicate, contradiction.

Answer 2

Indeed, the set of primes is not implicitly definable over $(\mathbb{N},S)$. I gave a proof of this in an answer to the question of Geoffrey Irving. See https://mathoverflow.net/a/426382/36385 .

Answer 3

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