Applications of Robinson's consistency theorem in algebra? This is crossposted from MSE. It's also my first time asking on MO, so please let me know if there's anything you need from me!

There are a family of results which, in many model theory books, are proven around the same time, often as corollaries of each other. These are

*

*The Craig interpolation theorem

*The Robinson consistency theorem

*The Beth definability theorem
For many "early" topics in model theory, there are some obvious results in algebra which admit easy proofs using this machinery. Compactness, completeness, and Lowenheim-Skolem all come to mind. Marker even finds low-hanging applications of o-minimality! However, I can't seem to find any algebraic applications of these theorems, even though they seem just as applicable as the other concepts I've mentioned.
I'm sure there are special cases where one might like to know that a relation (say, the ordering of a group, etc.?) is not definable from the rest of the structure (here Beth's Theorem and Padoa's Method might be useful). Similarly, knowing that we can find a model of $T_1 \cup T_2$ provided there's no obvious obstruction seems eminently useful (here I have in mind the version of Robinson's theorem that doesn't rely on completeness of $T_1 \cap T_2$). I'm not so surprised that I can't come up with any applications myself (sometimes being creative is hard), but I am surprised that searching my usual references, as well as spending some time on google, hasn't turned up any results.
Does anyone have any fun applications of these theorems in algebra?
Thanks in advance ^_^
 A: I don't know of a nice purely algebraic application off the top of my head, I don't even know of many applications to model theory. I was actually pretty happy with I found some application of Craig interpolation to model theory a few years back with Minh Chieu Tran and Alex Kruckman.
I can mention an application to model-theoretic algebra. Koeniggsmann and Jahnke show that if K is a field which admits a non-trivial Henselian valuation and is neither separably nor real closed then K defines a valuation which induces the Henselian topology. (Any two non-trivial Henselian valuations on a field induce the same topology, and they do not show that the definable valuation is Henselian.) Their proof makes crucial use of Beth definibility.
This is in the paper "Uniformly defining p-Henselian valuations", which you can find here: https://arxiv.org/pdf/1407.8156.pdf. It may also be worth mentioning that if K is either separably closed or real closed then K does not admit a non-trivial definable valuation (in either case this follows from the relevant quantifier elimination.)
It is my understanding that Craig interpolation has applications to computer science, but I'm not very familiar with this.
