Мне было интересно прочитать у Вавилова, что и в математике-то место теоремы Гёделя - очень скромное.
Вавилов. Не совсем наивная теория множеств. (web draft)
Там сказано во введении:
[...]
Довольно странное высказывание. Теорема Геделя же применима не только к арифметике, но и, например, к аксиоматическим теориям множеств. Это, конечно, правда, что она говорит о генерации текстов в специальном типе систем, но этот специальный тип не такой узкий, как его хочет выставить Вавилов. То же доказательство Генцена проводится во вполне себе теории первого порядка.
Более того, если мы говорим о логике второго порядка и так далее, то все равно неполнота вылезает, она просто сдвигается - теперь у нас семантическое понятие истинности не покрывается никаким (рекурсивно перечислимым) синтаксическим понятием выводимости. А выводимость это именно то, что моделирует реальную математику - возможность доказательства чего-то из некоторого числа строго очерченных правил.