Гёделя теорема о полноте

утверждение о полноте классического исчисления предикатов: всякая предикатная формула, истинная на всех моделях, выводима (по формальным правилам классич. исчисления предикатов). Г. т. о п. показывает, что множество выводимых формул этого исчисления в определенном смысле максимально: оно содержит все чисто логические законы теоретико-множественной математики. Доказательство К. Гёделя [1] дает способ построения контрмодели (т. е. модели для отрицания) всякой формулы А, невыводимой в Генцена формальной системе без сечения. Имеются также доказательства, основанные на расширениях систем формул до максимальных, а также доказательства, использующие ал-гебраич. методы. Теорема вместе с доказательством обобщается на исчисление с равенством. Другое направление - обобщение на произвольные множества формул: каждое непротиворечивое множество формул обладает моделью (множество Мнепротиворечиво, если для любых [img: http://localhost:8080/file/010408-225.jpg] невыводимо [img: http://localhost:8080/file/010408-226.jpg]). Гёделевское доказательство дает для непротиворечивого множества формул модель, элементами к-рой являются термы. Такие модели составляют исходный пункт во многих исследованиях по метаматематике теории множеств. Другое приложение моделей из термов - теорема Лёвенхейма - Сколема: если счетное множество формул имеет какую-то модель, то оно имеет счетную модель. Само гёделевское доказательство проводится средствами теории множеств без аксиомы бесконечности, т. е. средствами арифметики. Отсюда получается конструктивная форма Г. т. о п. (лемма Бернайса): для каждой предикатной формулы Аможно указать такую подстановку [img: http://localhost:8080/file/010408-227.jpg] арифметич. предикатов вместо предикатных переменных, что [img: http://localhost:8080/file/010408-228.jpg] выводима в формальной арифметике; здесь [img: http://localhost:8080/file/010408-229.jpg] - арифметич. формула, выражающая, что Авыводима. Таким образом, для выводимости Адостаточна ее истинность на той модели, к-рую задает подстановка [img: http://localhost:8080/file/010408-230.jpg] Лемма Бернайса применяется для построения моделей формальной системы [img: http://localhost:8080/file/010408-231.jpg] в системе [img: http://localhost:8080/file/010408-232.jpg], если в [img: http://localhost:8080/file/010408-233.jpg] доказана непротиворечивость [img: http://localhost:8080/file/010408-234.jpg]. Из Г. т. о п. можно извлечь также теорему об устранимости сечения (см. Генцена формальная система).и различные теоремы отделения, напр.: если формула, не содержащая знака равенства, выводима средствами исчисления предикатов с равенством, то она выводима в чистом исчислении предикатов; если предикатная формула выводима в арифметике со свободными предикатными переменными, то она выводима в исчислении предикатов. Г. т. о п. допускает (при соответствующем обобщении понятия модели) обобщение на неклассич. исчисления: интуиционистские, модальные и т. п.