Новости    Библиотека    Энциклопедия    Биографии    Карта сайта    Ссылки    О проекте




ГЁДЕЛЯ ТЕОРЕМА О ПОЛНОТЕ

ГЁДЕЛЯ ТЕОРЕМА О ПОЛНОТЕ - утверждение о полноте классического исчисления предикатов: всякая предикатная формула, истинная на всех моделях, выводима (по формальным правилам классич. исчисления предикатов). Г. т. о п. показывает, что множество выводимых формул этого исчисления в определенном смысле максимально: оно содержит все чисто логические законы теоретико-множественной математики. Доказательство К. Гёделя [1] дает способ построения контрмодели (т. е. модели для отрицания) всякой формулы А, невыводимой в Генцена формальной системе без сечения. Имеются также доказательства, основанные на расширениях систем формул до максимальных, а также доказательства, использующие алгебраич. методы. Теорема вместе с доказательством обобщается на исчисление с равенством. Другое направление - обобщение на произвольные множества формул: каждое непротиворечивое множество формул обладает моделью (множество М непротиворечиво, если для любых А1, ..., Ak ∈ М невыводимо ¬(A1 & ... & Ak)). Гёделевское доказательство дает для непротиворечивого множества формул модель, элементами к-рой являются термы. Такие модели составляют исходный пункт во многих исследованиях по метаматематике теории множеств. Другое приложение моделей из термов - теорема Лёвенхейма-Сколема: если счетное множество формул имеет какую-то модель, то оно имеет счетную модель. Само гёделевское доказательство проводится средствами теории множеств без аксиомы бесконечности, т. е. средствами арифметики. Отсюда получается конструктивная форма Г. т. о п. (лемма Бернайса): для каждой предикатной формулы А можно указать такую подстановку ξ арифметич. предикатов вместо предикатных переменных, что ξA → Рr(А) выводима в формальной арифметике; здесь Рr(А) -арифметич. формула, выражающая, что А выводима. Таким образом, для выводимости А достаточна ее истинность на той модели, к-рую задает подстановка ξ. Лемма Бернайса применяется для построения моделей формальной системы S в системе S', если в S' доказана непротиворечивость S.

Из Г. т. о п. можно извлечь также теорему об устранимости сечения (см. Генцена формальная система) и различные теоремы отделения, напр.: если формула, не содержащая знака равенства, выводима средствами исчисления предикатов с равенством, то она выводима в чистом исчислении предикатов; если предикатная формула выводима в арифметике со свободными предикатными переменными, то она выводима в исчислении предикатов.

Г. т. о п. допускает (при соответствующем обобщении понятия модели) обобщение на неклассич. исчисления: интуиционистские, модальные и т. п.

Лит.: [1] Gödеl К., «Monatshefte für Math. und Phys.», 1930, Bd 37, S. 349-60; [2] Hовиков П. С., Элементы математической логики, М., 1959; [3] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957.

Г. Е. Минц.


Источники:

  1. Математическая Энциклопедия. Т. 1 (А - Г). Ред. коллегия: И. М. Виноградов (глав ред) [и др.] - М., «Советская Энциклопедия», 1977, 1152 стб. с илл.




ИНТЕРЕСНО:

Зачем математики ищут простые числа с миллионами знаков?

Задача построения новых оснований математики - унивалентные основания

Многомерный математический мир… в вашей голове

В школах Великобритании введут китайские учебники математики

Найдено самое длинное простое число Мерсенна, состоящее из 22 миллионов цифр

Как математик помог биологам совершить важное открытие

Математические модели помогут хирургам

Почему в математике чаще преуспевают юноши

Физики-практики откровенно не любят математику

В индийской рукописи нашли первое в истории упоминание ноля

Вавилонская глиняная табличка оказалась древнейшей «тригонометрической таблицей» в мире

Ученые рассказали о важной роли игр с пальцами в обучении детей математике
Пользовательского поиска

© Злыгостев Алексей Сергеевич, статьи, подборка материалов, оформление, разработка ПО 2001-2018
При копировании материалов проекта обязательно ставить ссылку на страницу источник:
http://mathemlib.ru/ 'MathemLib.ru: Математическая библиотека'
Рейтинг@Mail.ru