Załóżmy, że znamy algorytmiczną procedurę, która rozstrzyga (choćby tylko w niektórych przypadkach) czy dowód p, że maszyna Turinga q dla danych wejściowych n nie ma własności stopu, jest poprawny (algorytm walidacji dowodów braku własności stopu maszyny Turinga).

Oznaczmy:

int PROCEDURA(int q, int n, int p)

możliwe wartości zwracane:

0 - dowód p że q(n) nie kończy pracy jest poprawny
1 - dowód p że q(n) nie kończy pracy jest błędny
2 - rozstrzygnięcie niemożliwe

oznaczenia:

q - numer maszyny Turinga lub liczba naturalna za pomocą której zakodowana jest treść funkcji napisanej w dowolnym języku programowania, który jest kompletny w sensie Turinga
n - liczba naturalna będąca daną wejściową
p - liczba naturalna za pomocą której zakodowana jest treść dowodu

Załóżmy, że znamy algorytm PROCEDURA i wiemy, że działa poprawnie (jeśli zwraca 0 to p faktycznie jest poprawnym dowodem, że q(n) nie kończy pracy).

Istnieje również pewna funkcja SERIALIZE, która każdej procedurze przypisuje pewną liczbę naturalną. Taką funkcję łatwo podać, można na przykład przyjąć, że tekst, którym zapisana jest procedura (string) to po prostu liczba naturalna zapisana w systemie pozycyjnym z bazą obejmującą cały zbiór znaków wykorzystywanych w języku programowania, w którym zapisana jest ta funkcja. W analogiczny sposób można kodować treść dowodów.

Teraz zdefiniujmy:

def ALGORYTM(q, n, p):
⠀⠀if PROCEDURA(q, n, p) == 0:
⠀⠀⠀⠀return 0
⠀⠀while True:
⠀⠀⠀⠀pass

Teraz wyobraźmy sobie taką funkcję (dla zachowania zwięzłości nie napiszę jej explicite, ale przedstawię dokładny schemat, jak można to zrobić):

def KONTRPRZYKŁAD(n):
⠀⠀1. wykonaj pierwszą setkę kroków procedury ALGORYTM(N, N, 1)
⠀⠀2. wykonaj drugą setkę kroków procedury ALGORYTM(N, N, 1), wykonaj pierwszą setkę kroków procedury ALGORYTM(N, N, 2)
⠀⠀3. wykonaj trzecią setkę kroków procedury ALGORYTM(N, N, 1), wykonaj drugą setkę kroków procedury ALGORYTM(N, N, 2), wykonaj pierwszą setkę kroków procedury ALGORYTM(N, N, 3)

⠀⠀...

⠀⠀dalej postępujemy analogicznie, zawsze dodając na koniec listy kolejny ALGORYTM(N, N, p) gdzie p jest kolejną liczbą naturalną (w tym wypadku byłoby cztery) i wykonując kolejne setki z algorytmów na aktualnej liście

⠀⠀jeśli gdziekolwiek dochodzimy do tej części funkcji ALGORYTM(N, N, x), że następuje zakończenie pracy i zwrócenie zera to cała procedura KONTRPRZYKŁAD kończy pracę

Zauważmy, że procedura KONTRPRZYKŁAD działa w taki sposób, że kończy pracę wtedy i tylko wtedy gdy któraś procedura ALGORYTM(N, N, x) kończy pracę i zwraca zero.

Po powyższych definicjach możemy wyprowadzić dwa wnioski:

a) Jeśli znamy procedurę PROCEDURA i wiemy że jest poprawna to możemy dowieść twierdzenia że "KONTRPRZYKŁAD(SERIALIZE(KONTRPRZYKŁAD)) nie kończy pracy". Jest to oczywiste, bo gdyby KONTRPRZYKŁAD(SERIALIZE(KONTRPRZYKŁAD)) kończył pracę (tzn. któraś z procedur ALGORYTM(N, N, x) kończyłaby prace i zwracała zero) to musiałby istnieć taki dowód p że ALGORYTM(SERIALIZE(KONTRPRZYKŁAD),SERIALIZE(KONTRPRZYKŁAD), p) zwracałby zero, czyli również PROCEDURA(SERIALIZE(KONTRPRZYKŁAD),SERIALIZE(KONTRPRZYKŁAD), p) zwracałaby zero, czyli PROCEDURA byłaby błędna gdyż uznałaby za poprawny dowód nieprawdziwego twierdzenia. A więc nasza wiedza że metody ujęte w zdefiniowanej na początku procedurze PROCEDURA prowadzą do poprawnych wyników, pociąga wiedzę o tym że KONTRPRZYKŁAD(SERIALIZE(KONTRPRZYKŁAD)) rzeczywiście nie kończy pracy.

b) Wiemy więc że algorytm KONTRPRZYKŁAD(SERIALIZE(KONTRPRZYKŁAD)) rzeczywiście nie kończy pracy ale to oznacza, że nie istnieje żaden dowód p dowodzący tego faktu, który jednocześnie mieści się w zbiorze dowodów rozpoznawanych jako poprawne zdefiniowanej początkowo procedury PROCEDURA, bowiem gdyby taki dowód istniał to KONTRPRZYKŁAD(SERIALIZE(KONTRPRZYKŁAD)) kończyłby pracę po prostu dochodząc w końcu do tego dowodu (postępując zgodnie z tym schematem opisanym wyżej, dla pewnego x ALGORYTM(N, N, x) zakończy pracę co oznacza że dla tego x PROCEDURA(N, N, x) zwraca 0). Jednak, skoro wiemy, że KONTRPRZYKŁAD(SERIALIZE(KONTRPRZYKŁAD)) nie kończy pracy to wiemy także, że taki dowód p nie istnieje.

Udowodniliśmy jednocześnie dwa twierdzenia:

a) KONTRPRZYKŁAD(SERIALIZE(KONTRPRZYKŁAD)) nie kończy pracy

b) Nie istnieje taki dowód p, że PROCEDURA(SERIALIZE(KONTRPRZYKŁAD), SERIALIZE(KONTRPRZYKŁAD), p) zwróci zero czyli rozpozna że jest poprawny

Jeśli przyjmiemy, że moglibyśmy dokładnie zbadać ludzki mózg i wyizolować algorytm PROCEDURA, który leży u podstaw logicznego rozumowania to a) jest w sprzeczności z b).

Powyższy dowód jest konstruktywny tzn. dokładnie pokazuje jak skonstruować obiekt, którego istenienia dowodzi. Jeśli ktoś poda procedurę PROCEDURA wraz z dowodem, że ta procedura działa poprawnie, natychmiast staje się możliwe podanie twierdzenia, którego dowód prawdziwości można zrozumieć, ale PROCEDURA nie jest w stanie go zaakceptować tzn. zwraca 2, "rozstrzygnięcie niemożliwe".

Ponadto funkcję PROCEDURA możemy tak zdefiniować aby zwracała 0 tylko dla bardzo dokładnie sprawdzonych dowodów p wykorzystujących jedynie najbardziej pewne, elementarne techniki dowodowe. Dowód zachodzi praktycznie niezależnie od tego gdzie ustalimy granice "pewności". Nawet jeśli PROCEDURA nigdy nie zwraca zera, powyższe rozumowanie pozostaje w mocy, chyba że poddalibyśmy w wątpliwość którąś z podstawowych metod logicznego dowodzenia wykorzystanych w punkcie a).

.