Doubly exponential complexity of Presburger arithmetics

I am trying to understand the proof of the aforementioned fact.
For context, here’s a rough outline of [what I am understanding to be] the idea behind the proof: in the language we construct a formula ϕ(x)\phi(x) asserting “machine xx, when started on input xx, halts in less than f(|x|)f(|x|) steps”, where f:x↦22kxf:x\mapsto 2^{2^{kx}} for some kk.
Next, given any machine MM intending to decide PrAPrA, we construct a machine M′M’ as follows: when started on input ww, M′M’ overwrites it with ¬ϕ(w)\neg\phi(w), then runs MM to decide it. If MM decides ¬ϕ(w)∈PrA\neg\phi(w) \in PrA, M′M’ halts, otherwise it loops forever. The conclusion is that any machine that decides PrAPrA must take ≥f(|♯M′|)\geq f(|\sharp M’|) steps to decide ¬ϕ(♯M′)\neg\phi(\sharp M’) – otherwise we get a contradiction when we run M′M’ on ♯M′\sharp M’. So far so good, I guess.

I get lost when it is time to construct ϕ\phi, though. For example, one of the building blocks [used in the construction] of ϕ\phi is a formula In(x)I_{n}(x), |In(x)|=O(n)|I_{n}(x)| = O(n), asserting “xx is less than f(n)2f(n)^{2}”. Now, the paper doesn’t show how to construct this formula, and I have no idea how to, too, given that we can only use addition and we have that bound there.

What am I missing?

EDIT, as suggested: the proof I am talking about is in Rabin and Fischer’s paper – .pdf available here. And one further thing: I found one post from Lipton’s blog where he talks about the “trick” used to construct InI_{n} succinctly. It is a sketch only and unfortunately not enough for me. It is mentioned however that the trick was previously discovered by Fischer and Meyer, and Volker Strassen, independently, but I couldn’t track down these papers describing it in detail – if anyone knows about them, please tell me!




It would probably help to reference the exact source you’re reading the proof in, such that answerers have the opportunity to try to align the structure and notation of their answers to it.
– Henning Makholm
Oct 20 at 21:34