Two forms of Beth's theorem?

Question

The version of Beth's theorem I'm familiar with is that if $\phi$ is a sentence in the language $\Sigma\sqcup \lbrace R\rbrace$ depends only on $\Sigma$ (i.e., $\mathcal{M}\upharpoonright\Sigma\cong\mathcal{N}\upharpoonright\Sigma\implies[\mathcal{M}\models\phi\iff\mathcal{N}\models\phi]$ for $\mathcal{M},\mathcal{N}$ ($\Sigma\sqcup\lbrace R\rbrace$)-structures), then there is a $\Sigma$-sentence $\psi$ equivalent to $\phi$ (i.e., $\mathcal{M}\models\phi\iff\psi$ for all $(\Sigma\sqcup\lbrace R\rbrace)$-structures $\mathcal{M}$). This is the version currently described in detail on the wikipedia page.

On the other hand, there is the implicit definability theorem (also called Beth's theorem?) which states that if $\phi$ is a sentence in $\Sigma\sqcup\lbrace R\rbrace$ such that for every $\Sigma$-structure $\mathcal{M}$ there is exactly one expansion $\mathcal{M}^\phi$ to $\Sigma\sqcup R$ such that $\mathcal{M}^\phi\models\phi$, then "$R$ is already definable:" there is some $\Sigma$-formula $\psi$ such that $R^{\mathcal{M}^\phi}=\psi^\mathcal{M}$. (And a stronger version where "exactly one" is replaced by "at most one.")

My question is, what is the relation between these two theorems? I vaguely recall that they can be deduced from each other, but I can't seem to work it out right now (maybe I'm being thick); also, what are their correct names?

Answer 1

What you call Beth’s theorem in the first paragraph is in fact trivial: just take for $\psi$ the sentence $\phi$ where all instances of $R$ are replaced by $\bot$ (or any fixed $\Sigma$-formula, for that matter).

The proper way to formulate Beth’s theorem along these lines is as follows:

(B1) Let $\Sigma\subseteq\Sigma^*$ be two languages, $T$ a theory in $\Sigma^*$, and $\phi$ a $\Sigma^*$-sentence. Assume that for every pair of models $M,N\models T$ such that $M\let\res\restriction\res\Sigma\simeq N\res\Sigma$, $M\models\phi$ iff $N\models\phi$. Then there exists a $\Sigma$-sentence $\psi$ such that $M\models\phi\let\eq\leftrightarrow\eq\psi$ for every model $M\models T$.

This is also more or less the version given on Wikipedia, except they use $=$ instead of $\simeq$, and allow formulas with free variables (both of which are immaterial differences). The presence of $T$ (and specifically the fact that it may not be a $\Sigma$-theory) is essential, otherwise the result is trivial, as mentioned above.

The second form of Beth’s theorem, in the “at most one” version, can be stated as follows:

(B2) Let $\Sigma\subseteq\Sigma^*$ be two languages, $T$ a theory in $\Sigma^*$, and $R\in\Sigma^*$. Assume that $R^M=R^N$ for every pair of models $M,N\models T$ such that $M\res\Sigma=N\res\Sigma$. Then there exists a $\Sigma$-formula $\psi$ such that $R^M=\psi^M$ for every model $M\models T$.

Note that in both (B1) and (B2), a simple application of compacteness shows that we could assume without loss of generality that $T$ is finite, hence in (B2), $T$ plays the role of your $\phi$. The only remaining difference is that I allow $\Sigma^*$ to be larger than $\Sigma\cup\{R\}$.

Now it is easy to see that (B1) and (B2) are equivalent.

(B1)${}\Rightarrow{}$(B2): If $\Sigma,\Sigma^*,T,R$ satisfy the assumptions of (B2), choose new constants $\vec c$ corresponding to the variables of $R$, and put $\Sigma'=\Sigma\cup\{\vec c\}$, $\Sigma'^*=\Sigma^*\cup\{\vec c\}$, $\phi=R(\vec c)$. Then the assumptions of (R1) are satisfied for $\Sigma',\Sigma'^*,T,\phi$, hence there exists a $\Sigma'$-sentence $\psi(\vec c)$ equivalent to $\phi$ in models of $T$ (expanded to $\Sigma'$), which means $R(\vec x)$ is equivalent to $\psi(\vec x)$ in models of $T$ in the original language.

(B2)${}\Rightarrow{}$(B1): Given $\Sigma,\Sigma^*,T,\phi$ satisfying the assumptions of (B1), let $\Sigma'=\Sigma^*\cup\{R\}$, where $R$ is a new nullary predicate, and $T'=T\cup\{\phi\eq R\}$. Then (B2) implies that there is a $\Sigma$-formula $\psi$ (which may be assumed to have the same free variables as $R$, i.e., none) equivalent to $R$ in models of $T'$. Since every model of $T$ can be expanded to a model of $T'$, this implies that $\psi$ is equivalent to $\phi$ in models of $T$. (If you do not like nullary predicates, you can make do with unary just the same.)

The two versions of Beth’s theorem can also be restated syntactically. Let $\Sigma^*\smallsetminus\Sigma=\{R_i:i\in I\}$, and let $R'_i$ be new predicates with matching arity. In order not to burden the notation too much, I will write formulas or theories in $\Sigma^*$ or $\Sigma\cup\{R'_i:i\in I\}$ in the form $\phi(\vec R)$, as if these predicates were second-order free variables. Then (B1) is equivalent to:

(B1’) If $T(\vec R),T(\vec R')\vdash\phi(\vec R)\eq\phi(\vec R')$, there is a $\Sigma$-sentence $\psi$ such that $T(\vec R)\vdash\phi(\vec R)\eq\psi$,

and (B2) is equivalent to

(B2’) If $T(\vec R),T(\vec R')\vdash R_i(\vec x)\eq R'_i(\vec x)$, there is a $\Sigma$-formula $\psi$ such that $T(\vec R)\vdash R_i(\vec x)\eq\psi(\vec x)$.