Untere Schranke

Für Maschine M mathend000# und Eingabe x mathend000# sowie Funktion f : $\mathbb {N}$→$\mathbb {N}$ mathend000# (z. B. n $\mapsto$ 2²ⁿ mathend000#) konstruiere Formel D(M, x) mathend000# mit

• D(M, x)$\iff$ mathend000# Maschine M mathend000# hält bei Eingabe x mathend000# in ≤f (| x|) mathend000# Schritten.
• D(M, x) mathend000# ist klein und kann schnell berechnet werden.

Für jedes Entscheidungsverfahren E mathend000# für Presburger-Arithmetik:

• konstruiere Programm E₀(x) mathend000#:
  if E(¬D(x, x)) mathend000# then stop else Endlosschleife.
• Beweise: Rechnung E₀(E₀) mathend000# hält nach > f (| E₀|) mathend000# Schritten.

bleibt zu zeigen, daß man solche D mathend000# konstruieren kann.