Akademik

- свойство формальной системы, состоящее в том, что не каждая формула этой системы доказуема в ней. Формальные системы, обладающие этим свойством, наз. непротиворечивым и, или формально непротиворечивым и. В противном случае формальная система наз. противоречивой, или несовместной. Для широкого класса формальных систем, язык к-рых содержит знак отрицания эквивалентна свойству:

"не существует такой формулы , что и обе доказуемы". Класс формул данной формальной системы наз. непротиворечивым, если не всякая формула этой системы выводима из данного класса. Формальная система наз. содержательно непротиворечивой, если существует модель, в к-рой истинны все теоремы этой системы. Если формальная система содержательно непротиворечива, то она формально непротиворечива. Для формальных систем, основанных на классическом исчислении предикатов, справедливо и обратное утверждение: в силу Гёделя теоремы о полноте классического исчисления предикатов, всякая такая непротиворечивая система имеет модель. Таким образом, один из способов доказательства Н. формальной системы состоит в построении модели. Другой (метаматематический) метод доказательства Н., предложенный в начале 20 в. Д. Гильбертом (D. Hilbeit), состоит в том, что утверждение о Н. нек-рой формальной системы рассматривается как высказывание о доказательствах, возможных в этой системе. Теория, объектами к-рой являются произвольные математич. доказательства, наз. доказательств теорией, или метаматематикой. Примером применения метаматематич. метода может служить предложенное Г. Генценом (G. Gentzen) доказательство Н. формальной системы арифметики (см. Генцена формальная система).

Любое доказательство Н. использует средства той или иной математич. теории, а потому лишь сводит вопрос о Н. одной теории к вопросу о Н. другой теории. При этом говорят также, что первая теория непротиворечива относительно второй теории. Большое значение имеет вторая теорема Гёделя, к-рая утверждает, что Н. формальной теории, содержащей арифметику, невозможно доказать с помощью средств самой рассматриваемой теории (при условии, что эта теория действительно непротиворечива).

Лит.:[1] Гильберт Д., Бернайс П., Основания математики. Логические исчисления и формализация арифметики, пер. с нем., М., 1979; [2] Новиков П. С, Элементы математической логики, 2 изд., М., 1973; [3] Френкель А., Бар-Хиллел И., Основания теории множеств, пер. с англ., М., 1966; [4] Генцен Г., в кн.; Математическая теория логического вывода, М., 1967, с. 77-153; [5] Минц Г. Е., в кн.: Итоги науки и техники. Алгебра. Топология. Геометрия, т. 13, М., 1975, с. 5-49; [6] Godеl К., "Monatsch. Math, und Physik", 1930, Bd 37, S. 349-60.

В. Е. Шиско.