Слайд 2
![Определение исчисления предикатов Определение 2.3. Функция одной или нескольких переменных,](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-1.jpg)
Определение исчисления предикатов
Определение 2.3. Функция одной или нескольких переменных, которая принимает
логическое значение ”истина” или ”ложь”, называется предикатом.
Переменные предиката называются предметными переменными.
Слайд 3
![Алфавит](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-2.jpg)
Слайд 4
![Кванторы](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-3.jpg)
Слайд 5
![Множество аксиом исчисления предикатов Аксиомы исчисления предикатов не содержат квантора](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-4.jpg)
Множество аксиом исчисления предикатов
Аксиомы исчисления предикатов не содержат квантора существования.
Для того, чтобы ввести в исчисление квантор существования, свяжем его с квантором всеобщности определением:
Слайд 6
![Правила вывода исчисления предикатов](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-5.jpg)
Правила вывода исчисления предикатов
Слайд 7
![Теорема о дедукции исчисления предикатов](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-6.jpg)
Теорема о дедукции исчисления предикатов
Слайд 8
![Теорема о дедукции исчисления предикатов](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-7.jpg)
Теорема о дедукции исчисления предикатов
Слайд 9
![](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-8.jpg)
Слайд 10
![Теоремы о полноте Мы уже упоминали понятие общезначимости формул, понимая](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-9.jpg)
Теоремы о полноте
Мы уже упоминали понятие общезначимости формул, понимая под
ними такие формулы, которые принимают значение ”истина” при всех значениях входящих в эту формулу переменных высказываний. Любая математическая теория интересна не только сама по себе, но и с точки зрения ее приложения в практических целях.
Формулы исчисления высказываний могут иметь некоторый смысл и обозначать некоторые высказывания естественного языка, если существует какая–либо интерпретация математической теории. Говоря неформально, интерпретировать математическую теорию — это значит связать с ней некоторую предметную область и указать соответствие формальных объектов математической теории и объектов данной предметной области.
Определение 2.5. Формула называется общезначимой, если она истинна при любой интерпретации.
Логическая формальная теория называется полной, если любая формула выводима в этой теории тогда и только тогда, когда она общезначима.
Слайд 11
![Теоремы о полноте](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-10.jpg)
Слайд 12
![Теоремы о полноте](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-11.jpg)
Слайд 13
![Теоремы о полноте В отличие от исчисления высказываний для исчисления](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-12.jpg)
Теоремы о полноте
В отличие от исчисления высказываний для исчисления предикатов существует
недоказуемая там формула, которую без противоречия можно присоединить к системе аксиом:
Теорема 2.8. Исчисление предикатов не полно в узком смысле.
Теорема 2.9. (Теорема о полноте исчисления предикатов – теорема Геделя.) Всякая тождественно истинная формула выводима в исчислении предикатов. Иначе говоря, исчисление предикатов полно только в широком смысле.
Слайд 14
![Логическое следствие](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-13.jpg)
Слайд 15
![Логическое следствие](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-14.jpg)
Слайд 16
![Метод резолюций](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-15.jpg)
Слайд 17
![](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-16.jpg)
Слайд 18
![Примеры применения метода резолюций Пример 1. Методом резолюций доказать теорему](/_ipx/f_webp&q_80&fit_contain&s_1440x1080/imagesDir/jpg/435195/slide-17.jpg)
Примеры применения метода резолюций
Пример 1. Методом резолюций доказать теорему ├¬A→(A→ B)
.
Доказательство. Запишем инверсию исходной формулы:
¬(¬A→(A→ B)).
Заменим все импликации по соответствующей формуле:
¬(¬A→(A→ B)) = ¬(¬¬A∨ (¬A∨ B)).
Применим закон двойного отрицания и закон де Моргана:
¬(¬A→(A→ B)) = ¬(A∨ (¬A∨ B)) = ¬A∧¬(¬A∨ B) =
= ¬A∧¬¬A∧¬B = ¬A∧ A∧¬B .
Получаем предложения: ¬A, A, ¬B. Резольвируем их:
1. ¬A – предложение.
2. A – предложение.
3. ¬B – предложение.
4. Ø R 1, 2.