W 1931 Kurt Gödel pokazał, że system dowodzenia twierdzeń arytmetycznych sformalizowany w ramach Principia Mathematica nie jest zupełny i niesprzeczny. Dowód Gödla jest czysto logiczny i nie odnosi się do żadnej notacji obliczalności, w związku z tym nie implikuje bezpośrednio nierozstrzygalności w obrębie zdań systemów aksjomatycznych logiki pierwszego rzędu.
Formalnie, negatywna odpowiedź na Entscheidungsproblem pojawiła się wraz z pracą Alonzo Churcha'a w 1936 i niezależną od niej, opublikowaną rok później, wyżej wspomnianą pracą Alana Turinga. Church przedstawił dowód w ramach rozwijanego przez siebie formalizmu rachunku lambda. Turing posłużył się wprowadzoną przez siebie koncepcją maszyny Turinga. Formalizmy te, jak się okazało, są równoważne, jednak wersja dowodu przedstawiona przez Turinga zyskała większą popularność.
W 1970 roku Yuri Matiyasevich udowodnił silniejsze twierdzenie dotyczące równań diofantycznych, które m.in. implikuje wyniki Churcha i Turinga (patrz: dziesiąty problem Hilberta).
Dowód
Dowód, że Entscheidungsproblem nie ma rozwiązania (lemat 3), stanowi wniosek w pracy Turinga wynikający z dwóch wcześniejszych lematów.