4.5. Исчисление предикатов

В логике предикатов, в отличие от логики высказываний, нет эффективного способа для распознавания общезначимости формул. Поэтому аксиоматический метод становится существенным при изучении формул, содержащих кванторы. Выделение общезначимых формул, так же как и в исчислении высказываний, осуществляется путем указания некоторой совокупности формул, которые называются аксиомами, и указания правил вывода, позволяющих из одних общезначимых формул получать другие общезначимые формулы.

Исчисление предикатов – это аксиоматическая теория:

Алфавит– те же символы, что и в логике предикатов.

Понятие формулы –совпадает с понятием формулы в логике предикатов.

Аксиомы:

1…10 – аксиомы Клини исчисления высказываний;

11) xA(x)A(y) (-схема);

12) A(y)xA(x) (-схема).

Система правил вывода:

1) modus ponens (m.p.);

2) правило обобщения (-правило);

3) правило введения(-правило).

4) Правило переименования связанной переменной. Связанную переменную формулы Aможно заменить (в кванторе и во всех вхождениях в области действия квантора) другой переменной, не являющейся свободной вA.

Понятия вывода, теоремы и доказательства определяются в исчислении предикатов точно так же, как и в любой аксиоматической теории.

Теорема 6. Аксиомы исчисления предикатов – общезначимые формулы.

Теорема 7. Формула, получающаяся из общезначимой по любому из правил вывода 1–3, является общезначимой.

Теорема 8. Любая выводимая в исчислении предикатов формула общезначима.

Теорема 9. Исчисление предикатов непротиворечиво.

Теорема Гёделя.Всякая общезначимая формула выводима в исчислении предикатов.

Теорема о дедукции. Если имеется вывод в исчислении предикатов формулыBиз последовательности формул,A, то можно построить вывод формулыABиз последовательности формул(символически: Если,AB, тоAB, где – набор некоторых формулA₁,A₂,...,A_n.

Пример 45.Построить вывод.

 1. посылка,

2. -схема,

3. акс. 1,,

4. m.p.1 и 3,

5.

акс. 9, ,

6. m.p.2 и 5,

7. m.p.4 и 6,

8. акс. 1,

,

9. m.p.7 и 8,

10. -правило к 9,

11. m.p.1 и 10.

Пример 46.Построить вывод.

 1. посылка,

2. -схема,,

3. m.p.1 и 2,

4. -схема,,

5. m.p.3 и 4.

Литература

1. Виленкин Н.Я. Рассказы о множествах. – М.: Наука, 1969.

2. Гаврилов Г.П., Сапоженко А.А.Сборник задач по дискретной математике. – М.: Наука, 1977.

3. Касаткин В.Н.Новое о системах счисления. – Киев: Вища школа. Головное изд-во, 1982.

4. Клини С.К.Математическая логика. – М.:Мир, 1973.

5. Кондаков Н.И.Логический словарь. – М.: Наука, 1971.

6. Кук В.,Бейз Г.Компьютерная математика. – М.: Наука, 1990.

7. Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов. – М.: Наука, 1975.

8. Москинова Г.И. Дискретная математика. Математика для менеджера в примерах и упражнениях: Учебное пособие. – М.: Логос, 2000.

9. Нефедов В.Н., Осипова В.А.Курс дискретной математики: Учеб. пособие. – М.: Изд-во МАИ, 1992.

10. Новиков Ф.А. Дискретная математика для программистов. – СПб: Питер, 2000.

11. Яшин Б.Л.Задачи и упражнения по логике. – М.: Гуманит. Изд. центр ВЛАДОС, 1996.