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 mathend000#
für Presburger-Arithmetik existiert eine Formel F mathend000#,

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

Beweis-Plan: Diagonalisierung (vgl. Halteproblem):

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

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