Игошин Математическая логика и теория алгоритмов (1019110), страница 68

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 68)

В самом деле, пусть Ф ~ с. Покажем, что тогда множество формул Ф () (- с ) противоречиво. Допустим на время, что это не так. Тогда по теореме 29.10 это множество имеет модель М, т.е. на М выполняется формула — с и все формулы из Ф. Из последнего, ввиду условия Ф ~ с, следует, что на М выполняется и формула Е Получаем противоречие. Итак, множество Ф 0 ( с ) противоречиво.

Значит, из него выводима любая формула, в частности Ф () (- с )»- р. Тогда по теореме о дедукции имеем Ф»- с -» Е Учитывая, что, кроме того, формула ( с -» с ) -» -» с является теоремой ФИВ, по правилу МР заключаем, что Ф»- Е 272 Итак, мы доказали, что если Ф Р, то Ф ь- Г. Объединив это утверждение со следствием 29.1 из теоремы 29.2, приходим к следующей важной метатеореме. Теорема 29.13 (теорема адекватности). Формула Рсинтаксически выводима из множества формул Ф тогда и только тогда, когда она семантически выводима из Ф: Ф ~- с <=> Ф Р П Если теорема оправданности означала, что при выборе аксиом и правил вывода мы не были слишком щедры (настолько, что сможем доказать лишь общезначимые формулы), то обратная теорема — теорема адекватности — означает, что при этом выборе мы не были и излишне скупы (ровно настолько, что сможем доказать всякую общезначимую формулу). Заметим, что нетрудно показать, что теорема о существовании модели вытекает из теоремы адекватности.

В самом деле, предположим, что Ф вЂ” непротиворечивое множество формул, не имеющее модели. Тогда ясно, что для любой формулы р справедливо семантическое следование Ф ~ Р. В силу теоремы адекватности отсюда следует, что Ф ь — г" для любой Р, что означает противоречивость множества Ф, в противоречие с условием. Теорема 29.14 (теорема Геделя о полноте ФИП ). дласс доказуемых замкнутых формул совпадает с классом оби1езначимых (или тождественно истинных) формул: ь — Р~ ~ с"'. Доказательство.

Эта теорема непосредственно вытекает из предыдущей при Ф = И. П Справедлива она и для открытых формул. В самом деле, если Р(хь ..., х„), где хн ..., х„— свободные предметные переменные в формуле Г, то в силу определения квантора общности это будет равносильно тому, что ~ ('Фх,) ... (чх„)(г(хь ..., х„)). По теоРеме 29. 14 это Равносильно томУ, что ь- (Чх~) ... (~Ух„)(с(хь ..., х„)). В силу свойств выводимости последнее утверждение равносильно тому, что ь- р(хь ..., х„). Неполнота формализованного исчисления предикатов в абсолютном и узком смыслах.

В учебнике обсуждаются два понятия полноты аксиоматической теории: абсолютная полнота и полнота в узком смысле (см. определение 27.6). Доказанная теорема 29.14 может быть истолкована как некая внешняя полнота формализованного исчисления предикатов, его полнота относительно логики предикатов: в этой теории могут быть формально доказаны все общезначимые формулы логики предикатов. Рассмотрим вопросы внутренней полноты формализованного исчисления предикатов, т.е.

выясним, будет ли эта теория абсолютно полной и полной в узком смысле (см. определения 27.5 и 27.6). Поскольку на основании теоремы 29.14 множество теорем формализованного исчисления предикатов совпадает с множеством тавтологий (обшезначимых формул) логики предикатов, а в логике предикатов сушествуют выполнимые, но не общезначимые формулы, формализо- 273 ванное исчисление предикатов не является абсолютно полной теорией. Здесь ситуация аналогична соответствующей ситуации в формализованном исчислении высказываний.

Что же касается полноты формализованного исчисления предикатов в узком смысле, то исчисление предикатов (в отличие от исчисления высказываний, см. теорему 28.4) таким свойством не обладает. Для доказательства приведем пример формулы, не являющейся теоремой формализованного исчисления предикатов, добавление которой к аксиомам исчисления предикатов (с сохранением правил вывода) приводит к непротиворечивой формальной аксиоматической теории. Пример 29.15. Рассмотрим формулу (Зх)(Р(х)) -+ (~х)(Р(х)).

Нетрудно убедиться в том, что она не является общезначимой (приведите пример конкретного одноместного предиката, превращающего эту формулу в ложное высказывание). Поэтому на основании теоремы К. Геделя о полноте она не доказуема в формализованном исчислении предикатов. С другой стороны, добавив к аксиомам формализованного исчисления предикатов рассматриваемую формулу, получим непротиворечивую формальную теорию Т.

Ее непротиворечивость можно доказать следующим образом. Рассмотрим модель этой теории на одноэлементном множестве М= (а). Ясно, что данная формула тождественно истинна на М. Далее, учитывая, что на М можно определить для каждого натурального и лишь два и-местных предиката Р, "и Р,", причем ЦР,"(а, ..., а)) = О и ЦР2"(а, ..., а)) = 1, нетрудно доказать, что все аксиомы новой теории Ттождественно истинны на этой модели и правила вывода от тождественно истинных на М формул приводят к тождественно истинным на М формулам. Таким образом, доказывается утверждение: всякая теорема теории Т тождественно истинна на одноэлементном множестве М. Следовательно, если бы для некоторой формулы Робе формулы Ри Р были теоремами теории Т, то они были бы тождественно истинны на одноэлементном множестве М, что невозможно. Поэтому расширенная теория Т непротиворечива, что и доказывает неполноту в узком смысле формализованного исчисления предикатов.

Теорема компактности. Мы уже отмечали (см. теорему 15.3, б) и неоднократно использовали тот простой факт, непосредственно вытекающий из определения понятия вывода, что Ф ~- Ртогда и только тогда, когда Фо ~- Р, где Фо — некоторое конечное подмножество множества Ф формул. Теорема адекватности, установленная на основании выдающейся теоремы Геделя о существовании модели, позволяет получить из этого тривиального соображения аналогичную теорему семантического содержания, уже отнюдь не столь очевидную. 274 Теорема 29.

1б (теорема К. Геделя — А. И. Мальцева). Если Ф ~ Р, то для некоторого конечного подмножества Фь ~ Ф имеет место Фь Р. Доказательство. Если Ф ~ Р, то по теореме 29.13 (теорема адекватности) Ф ь- Р В силу сделанного перед настоящей теоремой замечания найдется такое конечное подмножество Фь ~ Ф, что Фь ь- Р Отсюда по теореме оправданности (следствие 29.2 из теоремы 29.1) заключаем, что Ф, Р. П Следствие 29. 17 (локальная теорема К.

Геделя — А. И. Мальцева). Множество Х замкнутых формул узкого исчисления предикатов сигнатуры о имеет модель тогда и только тогда, когда каждое его конечное подмножество имеет модель. До к азат ел ь от в о. Необходимость очевидна. Обратно, пусть каждое конечное подмножество множества г. имеет модель. Тогда г, — синтаксически непротиворечиво. (Если бы это было не так, то для некоторой формулы Римелись бы выводимости ь > Ри х ь- Р, а значит, нашлось бы такое конечное подмножество г,, ~ г., что е, ь- Ри Хь ь- Р, т.е.

Хь было бы синтаксически противоречиво, а значит, по теореме 29.12 не имело бы модели, что противоречило бы условию.) Следовательно, по теореме 29.10 о сушествовании модели множество Х имеет модель. Следствие доказано. П В заключение приведем еше одну теорему о формулах узкого исчисления предикатов и их моделях. Теорема 29. 18 (Левенгейм — Сколем). Пусть о — счетная сигнатура и г, — множество замкнутых формул узкого исчисления предикатов сигнатуры о. Если г, имеет модель, то г. имеет счетную модель. Доказательство. Пусть о = (аь, а„...;1ы ун ...; Рь, Р„...) и множество г, формул имеет модель.

Тогда (по теореме 29.12) г, синтаксически непротиворечиво и модель этого множества формул может быть построена, как в доказательстве теоремы 29.10. Построенная таким образом модель будет счетной: она состоит из элементов аь, а„..й сь, с„... и всех теРмов (не содеРжаших пеРеменных), построенных из констант аь с,. Эти термы можно занумеровать, например, по следующему правилу: ч(а ) = 41+ 1, ч(с ) = 41+ 3, ч(1;((„..., г„)) = 2"'"3"оа5на1 ... р„ч, где рь = 2, р, = 3, рз = 5, ..., реп — последовательность простых чисел.

П Эта теорема может быть доказана и в более обшей мошностной формулировке: если множество г, формул имеет бесконечную модель и мощность множества всех букв, из которых составлены формулы из г., равна и, то для любой бесконечной мощности т > п существует модель множества г. мощности т. Укажем два следствия этой теоремы: 1) если Х вЂ” множество формул мощности п, имеющее бесконечную модель, то Х имеет бес- 275 конечные модели любых мощностей, нревыщающих н; 2) всякое конечное множество или счетное непротиворечивое множество формул либо имеет только конечные модели, либо имеет бесконечные модели любых мощностей. Теорема Левенгейма — Сколема дает ряд поразительных следствий двух типов: одни из них гласят, что некоторая теория имеет неожиданно обширные модели, другие — что теория имеет неожиданно узкие модели. Дальнейшее развитие эта мысль получит в следующем параграфе.

й 30. Формальные теории первого порядка В э 25 (см. также Задачник, Э 11) построено чистое формализованное исчисление предикатов первого порядка, а затем в Э 29 рассмотрены его свойства (метатеория). В этом исчислении не участвуют функциональные буквы и предметные константы основного алфавита, хотя язык исчисления (т.е.

его формулы) определен с учетом того, что такие символы в нем будут использоваться. Если в аксиомах и других формулах исчисления предикатов участвуют функциональные буквы и предметные константы, то говорят о прикладном исчислении предикатов, или о формальной аксиоматической теории, или об элементарной теории, или о теории первого порядка. Здесь можно отметить, что термин «теория первого порядка» означает, что в теории кванторы применяются лишь по предметным переменным и не применяются по переменным предикатным. Таким образом, каждая из теорий первого порядка является расширением формализованного исчисления предикатов.

Характеристики

Список файлов книги