тавтологичных формул — иными словами,
всех логически истинных высказываний, выразимых на языке исчисления высказываний. Системы аксиом, обладающие таким свойством, принято называть «полными».
Вопрос о полноте той или иной системы аксиом представляет, как правило, большой интерес. В самом деле, основным стимулом для аксиоматизации различных разделов математики бывает стремление найти подходящий перечень исходных допущений, из которых затем можно было бы вывести все истинные предложения данной области. Скажем, когда Евклид формулировал некоторую аксиоматизацию элементарной геометрии, он старался отобрать аксиомы таким образом, чтобы из них можно было вывести все истинные геометрические утверждения, не только уже известные в то время, но в принципе и любые другие, которые можно было бы научиться доказывать когда-либо в будущем.
Помимо прочего, Евклид обнаружил поразительную проницательность своей трактовкой знаменитой аксиомы параллельности как допущения, логически не зависящего от остальных аксиом предложенной им системы. Лишь спустя много времени удалось доказать, что эта аксиома действительно не может быть выведена из остальных аксиом Евклида, т. е. что без аксиомы параллельности эта система аксиом неполна.
До недавнего времени считалось более или менее само собой разумеющимся, что для каждой конкретной области математики можно подобрать полную систему аксиом. В частности, математики были убеждены, что система аксиом, предложенная для аксиоматизации арифметики натуральных чисел, полна или во всяком случае может быть пополнена (сделана полной) добавлением к исходному перечню еще конечного списка аксиом. Одним из величайших открытий Гёделя и было как раз обнаружение невозможности такой полной аксиоматизации арифметики.
6
Идея кодирования и ее использование в математике
Исчисление высказываний представляет собой пример математической системы, по отношению к которой задачи, выдвигаемые гильбертовской теорией доказательства, оказались, как мы видели, полностью реализованными. Конечно, это исчисление формализует лишь некоторый фрагмент формальной логики, язык и дедуктивный аппарат которого недостаточны даже для формального построения элементарной арифметики. Но возможности гильбертовской программы отнюдь не ограничиваются доказательством непротиворечивости исчисления высказываний. Можно привести примеры гораздо более богатых теорий, для которых оказалось возможным дать строго метаматематические доказательства непротиворечивости и полноты. Примером может служить арифметическая система с операцией
