В чистом исчислении предикатов К фл А выводима тогда и только тогда, когда А есть озф

Мы докажем только половину (более лёгкую) этой теоремы. Относительно второй половины скажем только, что она есть следствие следующих двух утверждений: а) лемма Линденбаума: если теория первого порядка непротиворечива (в частности, чистое исчисление предикатов), то существует ее полное непротиворечивое расширение (т.е. расширение, в котором для любой замкнутой фл выводимы либо сама фл, либо её отрицание); в) всякая непротиворечивая теория первого порядка (в частности, чистое исчисление предикатов) имеет счётную модель (модель, у которой область D счётная).

Доказательство первой половины Утверждения 2.2.1.

Легко проверить, что любой пример любой схемы аксиом является озф (проверьте этот факт!). Также, нетрудно видеть (частично это уже делалось в пункте 1.2 в самом конце), что понятие озф сохраняется при применении правил вывода МР и Gen. Следовательно, всякая теорема исчисления К является озф. Также, как следствие первой половины нашего Утверждения 2.2.1, получаем ещё одно доказательство непротиворечивости исчисления К (проделайте это самостоятельно).

Пусть А – фл с одной точно свободной пп (наше ограничение сделано для простоты рассмотрения). Рассмотрим фл А(x) и A(y), где x и y – разные переменные. Фл выше называются подобными, если пп x свободна для пп y в фл А(y) и А(y) не имеет свободных вхождений пп x. Нетрудно видеть, что наше отношение подобия симметрично.

Утверждение 2.2.2. Если фл А(x) и А(y) подобны, то „ "xA(x) º "yA(y).

Доказательство. По схеме аксиом А4 „ "xA(x) ® A(y). Теперь применим правило Gen: „ "y("xA(x) ® A(y)) и, по схеме аксиом А5, имеем „ "xA(x) ® "yA(y). Вторая половина Утверждения 2.2.2 доказывается аналогично в силу симметрии. Применяя тавтологию А®(В®(АÙВ)) (которая выводима в К, Утверждение 2.1.1), завершаем доказательство.

Задача. Докажите, что если фл А(x) и А(y) подобны, то „ $xA(x) º $yA(y).

Указание. Формула $xA(x) = Ø"xØA(x).

Замечание. Теорема о полноте была впервые доказана К. Гёделем (т.н. первая теорема Гёделя) в 1930 г. и её оригинальное доказательство было совсем другим. Мы приведём сейчас несколько следствий из теоремы о полноте, которые очень парадоксальны.

а) фл А истинна в каждой счётной модели Û „ _К А;

в) если фл В является следствием множества фл Г, то Г „ _К А;

с) теорема Сколема – Лёвенгейма: если теория К (любая теория первого порядка!) имеет какую-нибудь модель, то она имеет счётную модель (и это несмотря на то, что в формальной теории К речь может идти о несчётных множествах! Пример: теория множеств Цермело-Френкеля является теорией первого порядка). Следствие (конечно, не прямо из теоремы о полноте, а из доказательства второй её половины) достаточно парадоксальное.

В завершение изучения исчисления предикатов К приведем еще несколько дополнительных метатеорем (метатеоремой называется утверждение о свойствах какой-либо формальной теории) и рассмотрим вопрос о приведении фл языка теории К к некоторому важному стандартному (т.н. предваренному нормальному!) виду.

Утверждение 2.2.3. (правило индивидуализации)

"xА(x) „ А(y) Использовать схему аксиом А4 и правило МР.

Утверждение 2.2.4. Если пп x не свободна в фл А, то следующие фл являются теоремами теории К:

а) А® "xА(x); в) $xА(x)®А; с) "x(A®B)º(A®"xB);

d) "x(В®А)º($xВ®А).

Задача. Докажите последнее Утверждение 2.2.4 самостоятельно.

Указание. Воспользуйтесь исчислением К₄.

Утверждение 2.2.5. (правило существования)

„ А(y)®$xА(x) (пп y не входит свободно в фл $xА(x)).

Доказательство. По аксиоме А4 „ "xØА(x)®ØА(y).

Из тавтологии (А®ØВ)®(В®ØА) по МР получаем „А(y)®Ø"xØА(x) и „ А(y)®$xА(x), ч.т.д.

Приведём теперь ещё без доказательства правило переименования связанных пп.

Утверждение 2.2.6. (правило переименования связанных пп).

Если "xВ(x) есть подформула фл А, фл В(y) подобна фл В(x) и А^· есть результат замены по крайней мере одного вхождения "xВ(x) в А на "yВ(y), то „ АºА^·.

Наконец, приведем т.н. правило С, сделав предварительно небольшой комментарий. В математике распространены выводы следующего типа. Пусть доказано утверждение вида $xА(x). Тогда рассуждают так: если а есть объект такой, что верно А(а), то… (проводим некоторое рассуждение)… получим фл В, которая уже не содержит произвольно выбранного объекта а. Отсюда заключают, что верно утверждение $xА(x) ® В. На самом деле выбор элемента а со свойством А не нужен и в выводе в К можно обойтись без этого выбора. Мы не будем приводить как точную формулировку, так и обоснование правила С, а заметим только, что можно определить понятие вывода в К с правилом С и доказать, что если есть вывод в теории К с правилом С, то есть вывод просто в теории К (за более точными формулировками и доказательствами относительно правила С отсылаем читателя к книге Мендельсона «Введение в математическую логику», М., Мир, 1971 г., стр. 83-85).

Завершая изучение чистого исчисления предикатов К, докажем, что всякую фл А языка теории К можно привести к следующему, назовём его предваренным нормальным, виду: Q₁x₁Q₂x₂…Q_nx_nB, где каждое Q_i есть либо квантор ", либо Ø", а фл В кванторов не содержит.

Утверждение 2.2.7. Всякая фл равносильна (в смысле общезначимости, а значит и в смысле выводимости в К) некоторой фл в предваренной нормальной форме.

Доказательство. Следующие фл являются озф при условии, что y не входит свободно ни в А, ни в В:

I) ("xA(x)®B) º $y(A(y)®В);

II) $xА(x)®В º "y(A(y)®B);

III) В®"xА(x) º "y(B®A(y);

IV) B®$xA(x) º $y(B®A(y)).

На фл в пунктах Y и YI предыдущее ограничение на y не распространяется.

Y) Ø"xA º $xØA; YI) Ø$xA º "xØA.

Общезначимость фл в Y) и YI) доказывается очень просто (докажите самостоятельно). Докажем, что фл из I) есть озф. Пусть фиксированы интерпретация и оценка. Предположим, что истинна (при данных интерпретации и оценке) фл $y(A(y)®B) (напомним, что переменая y не входит свободно в В. Без ограничения общности считаем, что В – замкнутая фл и что в фл А свободно входит только переменная х. Это означает, что найдется элемент dÎ D (D – область интерпретации) такой, что истинна фл А(d)®В. Если для всякого dÎ D. А(d) – истинная фл, то и В – то же истинная фл и тогда истинна фл "хА(х)®В. Если же А(d) истинна не для всякого d, то истинна фл "хА(х)®В в силу ложности посылки. Обратно, предположим, что "хА(х) – ложная фл. Но тогда для некоторого d фл А(d) – ложна и, следовательно, фл $y(A(y)®B) – истинна. Если же "хА(х) – истинная фл, то В – истинная фл и фл $y(A(y)®B) также истинна. Общезначимость фл из пункта II доказывается аналогично.

Задача. Докажите, что фл III и IV также есть озф.

Утверждение 2.2.7 доказано. Это доказывает возможность приведения каждой фл исчисления К к предваренной нормальной форме.

Вопросы и упражнения к Лекции 2.

1. Какие свойства исчисления предикатов Вы знаете?

2. Верно ли, что исчисления предикатов непротиворечиво? Полно?

(заметим, что в 1936 г. А.Чёрч доказал, что исчисление предикатов

неразрешимо; но исчисление одноместных предикатов оказывается

всё же разрешимо!)

3. Докажите, что исчисление предикатов непротиворечиво.

4. Сформулируйте теорему о дедукции для исчисления предикатов.

5. Что такое предваренный нормальный вид для формулы?

6. Верно ли, что любая формула исчисления предикатов приводима

к этому виду (эквивалентным образом)?

7. Что такое правило индивидуализации?

8. Что такое правило переименования связанных переменных?

9. Сформулируйте правило существования.

10.Тот же вопрос для правила С.

Дата добавления: 2014-01-06