Eine untere Schranke

Fischer und Rabin 1974: http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps

Für jedes Entscheidungsverfahren E
für Presburger-Arithmetik existiert eine Formel F,

so daß E(F) wenigstens 2^{2| F|} Rechenschritte benötigt.

Beweis-Plan: Diagonalisierung (vgl. Halteproblem):

wende solch ein Entscheidungsverfahren „auf sich selbst`` an.

Dazu ist Kodierung nötig (Turing-Programm ↔ Zahl)