формальная). При этом предполагается, что А корректно описывает арифметику, т. е., что все ф-лы, выводимые в А, являются истинными утверждениями о натуральных числах. Для любой такой системы А первая теорема Гёделя утверждает, что не все истинные ф-лы арифметики доказуемы в А. Другими словами, понятие истинности ф-л арифм. языка шире, чем понятие доказуемости в любой формальной системе (если последняя корректна). Ниже приводится интуитивная идея доказательства этой теоремы, которая существенна для понимания содержания обеих теорем о неполноте.
Предположим обратное, т. е., что арифм. истинность совпадает с доказуемостью в А. Поскольку доказательства в системе А суть конечные последовательности ф-л, связанных между собой правилами вывода, то проверка того, является ли данная последовательность ф-л доказательством, выполняется с помощью довольно простого алгоритма. При подходящем кодировании этот алгоритм может быть описан в арифм. языке (см. Арифметизация метаматематики). Поэтому можно построить арифм. ф-лу 
, означающую, что х есть код ф-лы, доказуемой в А. Теперь нетрудно написать ф-лу - назовем ее v, которая выражает свою собственную недоказуемость. Точнее, для этой ф-лы в системе А доказуема эквивалентность:
где 
есть код ф-лы 
. В силу предположения о том, что доказуемость совпадает с истинностью, получаем, что выражает также свою собственную ложность. Но тогда эта ф-ла не может быть ни истинной, ни ложной, так что мы приходим к известному «парадоксу лжеца». Следовательно, истинность и доказуемость не совпадают. Примером истинной, но недоказуемой в А ф-лы как раз и является ф-ла 
она истинна, так как утверждает свою недоказуемость и в самом деле недоказуема.
Приведенные выше эвристические соображения существенно используют предположение о том, что в А доказуемы только истинные формулы. Более строгое исследование показывает, однако, что недоказуемость может быть выведена из более слабого предположения о непротиворечивости системы А. Это уточнение имеет принципиальный характер. Дело в том, что понятие арифм. истинности невыразимо в языке арифметики, в то время как утверждение о непротиворечивости А можно записать й виде довольно простой арифм. ф-лы 
. Благодаря этому первую теорему о неполноте можно высказать на языке арифметики посредством ф-лы:
Можно показать, что эта ф-ла сама выводима из аксиом Пеано. Отсюда легко получается вторан теорема Гёделя о неполноте, которая (нестрого) утверждает, что непротиворечивость формальной системы А нельзя доказать средствами этой системы. Более строго, если формальная система А непротиворечива и содержит аксиомы Пеано, то ф-ла 
недоказуема в 
. В самом деле, из доказуемости ф-л (1) и (2) вытекает, что формулы и 
эквивалентны в системе А. Но 
недоказуема в Л, согласно первой теореме Гёделя; значит, 
тоже недоказуема.
До сих пор речь шла только об арифметике. Но все предыдущие рассуждения применимы также к достаточно произвольным формальным системам. В частности, совсем не обязательно, чтобы языком системы А был язык элементарной арифметики. Единственное, что здесь требуется, — это чтобы осн. понятия арифметики были выразимы в языке рассматриваемой формальной системы, а аксиомы Пеано — доказуемы в этой системе. Поэтому теоремы Гёделя применимы к любым разумным аксиоматизациям арифметики, анализа или множеств теории.
Теоремы о неполноте выявляют одну специфическую трудность, связанную с доказательствами непротиворечивости. Сущность ее удобнее всего проиллюстрировать на примере теории мн-в. Пусть ZF есть формальная система теории мн-в, основанная на аксиомах Цер-мело — Френкеля. До сих пор не существует доказательства непротиворечивости для ZF. Однако можно заранее сказать, что такое доказательство должно удовлетворять следующим двум требованиям (из которых первое обусловлено самой постановкой вопроса, а второе следует из теоремы Гёделя): а) это доказательство должно опираться лишь на концепции, интуитивно более простые, чем те, которые используются в самой теории мн-в; б) его нельзя провести в рамках системы ZF. Но система ZF отличается чрезвычайной широтой: в ней формализуется практически вся современная математика. Поэтому трудно представить себе, как выглядело бы матем. доказательство, удовлетворяющее указанным требованиям. Т. о., здесь затрагиваются сложные проблемы оснований математики, в силу чего теоремы Гёделя имеют определенный философский интерес.
Существует мнение, что теоремы о неполноте показывают невозможность маш. моделирования каких-либо нетривиальных форм мыслительной деятельности. Такое мнение, по-видимому, лишено достаточных оснований; Г. т. о н. имеют к вопросу о машинном творчестве такое же отношение, как, напр., логические парадоксы к творческим способностям человеческого разума. Вопрос о возможностях «машинного разума» является дискуссионным (см. Искусственный разум).
Лит.: Клини С. К. Математическая логика. Пер. с англ. М., 1973 [библиогр. с. 451-465); FefermanS. Arithmetization of metamathematics in a general setting. «Pundamenta mathematicae», 1960, v. 49; Линдон P. Заметки по логике. Пер. с англ. М., 1968 [библиогр. с. 123]; Арбиб М. Мозг, машина и математика. Пер. с англ. М., 1968 [библиогр. с. 217— 224]; Нагель Э., Ньюмен Д. Р. Теорема Гёделя. Пер. с англ. М., 1970.
Я. В. Белякин.
