Теорема Гёделя о неполноте утверждает, что в любом достаточно богатом языке найдутся истинные, но не доказуемые утверждения. Теорема имеет алгоритмические истоки, и существуют четыре принципиально различные пути, ведущие к ней. Лекции летней школы «Современная математика», г. Дубна, 21-22 июля 2007 г., Владимир Успенский.