The trick used in the proof of the doubly exponential complexity of Presburger arithmetics
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&lt; 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.