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₁,… mathend000# mit

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

Realisierung

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

  (die naive Implementierung ist aber zu groß)

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

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

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