Presburger-Arithmetik und große Zahlen

(folgende Konstruktion ist ähnlich zu der, die im tatsächlichen Beweis verwendet wird)

es gibt eine Folge von P-Formeln F₀, F₁,… mit

• | F_n|∈O(n)
• F_n(x)$\iff$x = 2²ⁿ

Realisierung

• verwende G_n(x, y, z) mit Spezifikation x = 2²ⁿ∧xy = z

  (die naive Implementierung ist aber zu groß)

• und Trick (``the device preceding Theorem 8''):

  H(x₁)∧H(x₂) ist äquivalent zu

  ∀x∀y : (x = x₁∨...)→...