Twierdzenia Gödla o niezupełności
Dowód z 1931 roku, że każdy dostatecznie silny system formalny zawiera prawdy, których nie potrafi udowodnić — i nie może nawet zaświadczyć o własnej niesprzeczności.
Kurt Gödel miał 25 lat i pracował w Wiedniu, gdy opublikował artykuł o niezbyt gościnnym tytule Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. Pierwsze twierdzenie: każdy niesprzeczny, efektywnie wyliczalny system aksjomatów dość silny na arytmetykę zawiera zdania, których nie da się w nim ani udowodnić, ani obalić. Drugie twierdzenie: żaden taki system nie udowodni własnej niesprzeczności. Program Hilberta, który miał dać matematyce ostateczny fundament, okazał się nie tyle trudny, ile niewykonalny.
Spuścizną jest technika. Gödel ponumerował formuły: każde zdanie dostało liczbę, każdy krok dowodu stał się arytmetyczną relacją między liczbami, a system mógł więc mówić o sobie, nie opuszczając arytmetyki. Następnie zbudował zdanie, które w tym kodowaniu głosi „nie jestem dowodliwe". Jeśli da się je udowodnić, jest fałszywe, a system dowodzi fałszów. Jeśli się nie da — jest prawdziwe, a zarazem niedowodliwe.
Ten sam argument przekątniowy wraca pięć lat później w problemie stopu, w twierdzeniu Rice'a, w quine'ach i w każdym wyniku o tym, czego analiza statyczna nigdy nie rozstrzygnie. Gödel kodował formuły jako liczby; maszyna von Neumanna przechowuje programy jako dane w tej samej pamięci. To jedna sztuczka, użyta raz jako dowód, a raz jako sposób budowania maszyn.