The trick used in the proof of the doubly exponential complexity of Presburger arithmetics

I posted this on MathUnderflow but got no answers, so thought I'd try it here,

I am reading Rabin and Fischer's old paper [will post a link when possible] where among other things, the doubly exponential complexity of Presburger arithmetics is proven.

The proof relies on the existence of a formula $I_{n}(x)$ informally asserting "$x < 2^{2^{kx+1}}$" with $|I_{n}| \in O(n)$. Though the construction of this formula is not given in the paper, which was a surprise to me considering that it is presumably highly nontrivial, given that bound and the fact that we only have addition at our disposal!¹

I later learned that the construction of this formula relies on a "trick", previously discovered by Fischer, and independently by Volker Strassen, but I have not managed to track down a paper describing this trick in detail!

So if anyone knows about the paper I am talking about and can either point me in its direction or even describe the trick to me...

This post from Lipton's blog contains a link to the paper as well as mentions [and provides a rough, unfortunately insufficient for me, sketch of] said trick, BTW.

¹ I know that this is a vague description. Though, a sufficiently detailed description would be way too long for a SX post, so I just hope that someone that already knows about the paper in question - and thus can make do with that brief sketch - bumps into this and is able to help me.

Martin's comment (and Yuval's follow up) gives the reference which explains the construction in some detail.

I'll elaborate a bit because I think it's a gorgeous proof: basically it's performing the "usual" proof of undecidability of PA (arithmetic with addition and multiplication), but relativized to $2^{2^{c\cdot n}}$! That is, there is a (short) formula which expresses multiplication up to that number, i.e. a formula $M_n(x,y,z)$ such that
$$M_n(x,y,z) \Leftrightarrow x\times y=z\ \wedge x< 2^{2^n} $$

Now you build $M_n$ by induction on $n$, with a crucial trick that is reminiscent of the Karatsuba algorithm for multiplying binary numbers or certain tricks for matrix multiplication:

In the definition for $M_{n+1}(x,y,z)$ you end up with a conjunction of the form
$$M_{n}(x_1,y_1,z_1)\wedge M_{n}(x_2,y_2,z_2)\wedge M_{n}(x_3,y_3,z_3)$$

But you can replace this with
$$ \forall u v w,(u=x_1\wedge v=y_1\wedge w=z_1)\vee(u=x_2\wedge v=y_2\wedge w=z_2)\vee(u=x_3\wedge v=y_3\wedge w=z_3)\Rightarrow M_n(u,v,w)$$

This trick allows a linear increase in size instead of an exponential one (as a function of $n$).

There's a couple of other tricks involved, but this is the main one. The internals of the recursion are important, of course, but the similarity to the Karatsuba trick is really quite striking.

StackExchange Computer Science Q#65094, answer score: 7