Гёделя Теорема О Полноте

утверждение о полноте классического исчисления предикатов. Всякая предикатная формула, истинная на всех моделях, выводима (по формальным правилам классич. Исчисления предикатов). Г. Т. О п. Показывает, что множество выводимых формул этого исчисления в определенном смысле максимально. Оно содержит все чисто логические законы теоретико-множественной математики. Доказательство К. Гёделя [1] дает способ построения контрмодели (т. Е. Модели для отрицания) всякой формулы А, невыводимой в Генцена формальной системе без сечения. Имеются также доказательства, основанные на расширениях систем формул до максимальных, а также доказательства, использующие ал-гебраич. Методы. Теорема вместе с доказательством обобщается на исчисление с равенством.

Другое направление - обобщение на произвольные множества формул. Каждое непротиворечивое множество формул обладает моделью (множество Мнепротиворечиво, если для любых невыводимо ). Гёделевское доказательство дает для непротиворечивого множества формул модель, элементами к-рой являются термы. Такие модели составляют исходный пункт во многих исследованиях по метаматематике теории множеств. Другое приложение моделей из термов - теорема Лёвенхейма - Сколема. Если счетное множество формул имеет какую-то модель, то оно имеет счетную модель. Само гёделевское доказательство проводится средствами теории множеств без аксиомы бесконечности, т. Е. Средствами арифметики. Отсюда получается конструктивная форма Г. Т. О п. (лемма Бернайса).

Для каждой предикатной формулы Аможно указать такую подстановку арифметич. Предикатов вместо предикатных переменных, что выводима в формальной арифметике. Здесь - арифметич. Формула, выражающая, что Авыводима. Таким образом, для выводимости Адостаточна ее истинность на той модели, к-рую задает подстановка Лемма Бернайса применяется для построения моделей формальной системы в системе , если в доказана непротиворечивость . Из Г. Т. О п. Можно извлечь также теорему об устранимости сечения (см. Генцена формальная система).и различные теоремы отделения, напр. Если формула, не содержащая знака равенства, выводима средствами исчисления предикатов с равенством, то она выводима в чистом исчислении предикатов. Если предикатная формула выводима в арифметике со свободными предикатными переменными, то она выводима в исчислении предикатов.

Г. Т. О п. Допускает (при соответствующем обобщении понятия модели) обобщение на неклассич. Исчисления. Интуиционистские, модальные и т. П. Лит.:[1] Godе1 К., "Monatshefte fur Math, und Phys.", 1930, Bd 37, S. 349-60. [2] Hовиков П. С., Элементы математической логики, М., 1959. [3] Клини С. К., Введение в метаматематику, пер. С англ., М., 1957. Г. Е. Минц. .