Глава IV. Теории первого порядка
§ 1. Теории первого порядка
Теория первого порядка T задается тремя условиями:
1) Некоторым языком первого порядка LT .
Сокращения:
(D3) (jÙy) вместо Ø(j®Øy).
(D4) (jÚy) вместо (Øj®y).
(D5) (j«y) вместо ((j®y)Ù(y®j)).
(D6) ($a)j вместо Ø("a)Øj.
2) Некоторым первоначальным перечнем формул – списком аксиом данной теории.
3) Некоторым количеством правил вывода.
Логические и специальные аксиомы.
Логические аксиомы:
(AS-1) Любая формула вида j®(y®j) является аксиомой.
(AS-2) Любая формула вида (j®(y®c))®((j®y)®(j®c)) является аксиомой.
(AS-3) Любая формула вида (Øj®Øy)®((Øj®y)®j) является аксиомой.
(AS-4) Любая формула вида ("a)(j®y)®(j®("a)y) является аксиомой, если aÏ Free j.
(AS-5) Любая формула вида ("a)j®j¢ является аксиомой, где формула j готова для подстановки терма t на месте переменной a и j¢ = j .
Понятие a-частного случая формулы j.
Правила вывода:
(R1) = (MP) (правило отделения): Из j и j®y получается y.
(R2) = (Gen) = (G) (правило обобщения): Из j получается ("a)j.
(Формальное) Доказательство. Теорема. T⊢j.
Теорема 1.1°. (А) Любая аксиома является теоремой.
2°. (Т) Любой частный случай любой тавтологии является теоремой.
3°. (MP) Если T⊢j и T⊢j®y, то T⊢y.
4°. (Gen) Если T⊢j, то T⊢ ("a)j для любой переменной a.
Теорема 2.1°. Если ⊢j или ⊢y, то ⊢jÚy.
2°. Если ⊢Øj, то ⊢j®y для любой формулы y.
3°. Если ⊢y, то ⊢j®y для любой формулы j.
4°. Если ⊢j и ⊢y, то ⊢jÙy и наоборот.
5°. (S) Если ⊢j®y и ⊢y®c, то ⊢j®c.
Теорема 3.1°. Если ⊢j®y и aÏ Free j, то ⊢j®("a)y.
В частности, если ⊢jÚy и aÏ Free j, то ⊢jÚ("a)y.
2°. Если ⊢j®y и aÏ Free y, то ⊢ ($a)jÚy.
Теорема 4.1°. Если j¢ – a-частный случай j и ⊢j, то ⊢j¢.
2°. (GnG) ⊢j тогда и только тогда, когда ⊢ ("a)j.
Теорема 5.Если j¢ – a-частный случай j, то ⊢j¢®($a)j.
§ 2. Некоторые методы доказательства
I. Метод вспомогательной гипотезы
Теорема 1. Метатеорема дедукции Эрбрана-Тарского
Пусть T – теория первого порядка и T ¢ = T +{j} – теория первого порядка, полученная из T добавлением формулы j к перечню аксиом теории T, причём j является формулой языка LT. Тогда если формула y языка LT является теоремой теории T ¢ и в доказательстве y не используется правило обобщения по переменным, входящим свободно в j, то T⊢j®y.
Доказательство индукцией по длине вывода с перебором случаев, в зависимости от обоснования последнего вывода.
Примечание. Ограничение в условии теоремы существенно. Если j = (x = 1) и T¢ = Ar+{j}, то тогда T⊢ ("x)(x = 1). Если бы Ar⊢ (x = 1)®("x)(x = 1), то Ar⊢ ($x)(x = 1)®("x)(x = 1), а потому Ar⊨ ($x)(x = 1)®("x)(x = 1).
II. Метод вспомогательной константы
Теорема 2. Если ⊢j®y и ⊢ ($a)j, и aÏ Free y, то ⊢y.
III. Метод приведения к абсурду
Теорема 3. 1°. Если ⊢Øj®y и ⊢Øj®Øy, то ⊢j.
2°. Если ⊢Øj®yÙØy, то ⊢j.
IV. Метод перебора случаев
Теорема 4. 1°. Если ⊢j®c и ⊢y®c, то ⊢jÚy®c.
В частности,
2°. Если ⊢j®c, ⊢y®c,⊢jÚy, то ⊢c.
3°. Если ⊢j®c, ⊢Øj®c, то ⊢c.
§ 3. Модели теорий первого порядка
Определение модели теории T, общезначимой в теории T формулы, истинного в теории T высказывания. T ⊨j.
Теорема 1. Теорема адекватности
Если T ⊢j, то T ⊨j.
Определение противоречивой теории.
Теорема 2. Любая формула противоречивой теории является теоремой этой теории.
Теорема 3.Противоречивые теории не имеют моделей.
Теорема 4. Теорема Гёделя
Если теория непротиворечива, то она имеет модель.
Теорема 5.Теорема полноты Гёделя
Пусть T – непротиворечивая теория. Тогда T ⊢j если и только если T ⊨j.
Лемма. Если j – высказывание теории T и T ⊢j, то T ¢ = T +{Øj} является непротиворечивой теорией.
Определение исчисления предикатов.
Теорема 6. Исчисление предикатов непротиворечиво (Логика непротиворечива).
План доказательства.
u: pi ® Xi. Продолжить u до : стирает термы и кванторы.
Литература
1. Мадер В.В. Введение в методологию математики. – М.: Интерпракс, 1995.
2. Мендельсон Э. Введение в математическую логику. – М.: Наука, 1973.
3. Назиев А.Х. Вводный курс математики – Рязань: Изд-во РГПУ, ч. 2а – 2000.
4. Назиев А.Х., Моисеев С.А., Математическая логика: задачник-практикум. – Рязань: Изд-во РГУ, 2011.
5. Никольская И.Л. Математическая логика. – М.: Высшая школа, 1981.
6. Столл Р.Р. Множества. Логика. Аксиоматические теории. – М.: Просвещение, 1966.