Gödel zeigte, dass die Ausgangsformel genau dann in der klassischen Peano-Arithmetik (beschränkt auf eine Variablensorte) herleitbar ist, wenn ihre Übersetzung in der Heyting-Arithmetik herleitbar ist.