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

1.

Федеральное государственное бюджетное образовательное учреждение
высшего профессионального образования
«Ижевский государственный технический университет
имени М. Т. Калашникова»
Кафедра «АСОИУ»
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
Автор Исенбаева Е.Н., старший преподаватель
Ижевск
2013

2. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ

Исчисление предикатов – это аксиоматическая
.
теория, в которой выделение
общезначимых
формул осуществляется путём указания:
- некоторой совокупности формул- аксиом;
- правил вывода, позволяющих из общезначимых
формул получить общезначимые.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
2

3.

I. Алфавит исчисления предикатов
1) Предметные переменные: х1, х2, … , хn
2) Предикатные буквы: Р1(к), Р2(к), Р3(к),
… , Рn(к)
3) Знаки логических связок: ¬, &, ˅,→
4) Кванторы ,
5) Скобки ( , ) , запятые.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
3

4.

II. Формула исчисления предикатов
Определение предикатной формулы
остаётся таким же, как
и в исчислении высказываний.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
4

5.

III. Аксиомы
Аксиомы делятся на две группы:
1) аксиомы исчисления высказываний (можно
взять любую из систем I или II)
2) аксиомы предикатные:
Р1: xF(x) F(y)
Р2: F(y)
xF(x)
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
5

6.

Аксиомы
где - F(x) – любая формула, содержащая свободные вхождения x, причём,
ни одно из них не находится в области действия квантора по y;
-Формула F(y) получена из F(x) заменой всех свободных
вхождений x на y.
Чтобы пояснить существенность требования к вхождению x в F,
рассмотрим в качестве F(x) формулу Ǝ yP(у,х), где это требование
нарушено: свободное вхождение x находится в области действия Ǝ y.
Подстановка этой формулы в аксиому Р1 даёт формулу:
˅xƎ y P(y,x) →ƎyP(y,y)
При интерпретации на множестве N натуральных чисел с
предикатом P(a, b) = [a > b] получим высказывание: «если для
всякого x найдётся y больший, чем x, то найдётся y больший самого себя»
Посылка этой импликации истина на N, а её заключение ложно, →
само высказывание ложно.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
6

7.

IV. Правила вывода
1)Правило заключения;
2)Правило обобщения(правило -введения);
3)Правило - введения;
4)Правило переименования свободных
переменных;
5)Правило переименования связанных
переменных.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
7

8.

Правило заключения
-правило заключения (modus ponens) – то же
что и в исчислении высказываний
(1)
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
8

9.

Правило обобщения (правило- введения квантора общности)
правило обобщения (правило введения квантора
общности)
(2)
где G(x) содержит свободные вхождения x, а F их не содержит.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
9

10.

Правило
Ǝ- введения
правило - введения
(3)
при тех же требованиях к F и G. Нарушение этих
требований может привести к ложным выводам из
истинных высказываний.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
10

11.

Пример
Пусть
P(x) – предикат «x делится на 6»
Q(x) – предикат «x делится на 3»
Высказывание P(x) Q(x), очевидно, истинно для любого x,
однако применение к нему правила обобщения даёт
высказывание:
P(x)
xQ(x), являющееся не всегда истинным.
Если же к P(x) Q(x)применить правило - введения, то получим:
xP(x)
Q(x), из которого путём (уже корректного) применения
правила обобщения получим высказывание: xP(x)
xQ(x) ложное на множестве натуральных чисел.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
11

12. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ

Возможны и другие системы аксиом и правил.
.
В исчислении предикатов принцип минимизации
числа логических операторов выражается в том,
что квантор Ǝ не является самостоятельным
символом, а рассматривается как сокращение
выражения: ¬ x¬P(x)
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
12

13.  

Правило переименования свободных
переменных
Правило переименования свободных переменных
В исчислении предикатов из выводимости
формулы F(x), содержащей свободные
вхождения x, ни одно из которых не находится в
области действия квантора по y, следует
выводимость F(y).
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
13

14.

Доказательство
1. ├ F(x) выводима (по условию)
2. F(x) (G F(x)) - в качестве G выбираем любую
доказуемую формулу (это понадобится в п.5), не
содержащую свободных вхождений x (понадобится в
п.4).
3. G
F(x) (применяем m.p. к п.1 и п.2).
4. G
xF(x) (применяем правило - введения к
п.3) , учитывая, что G не содержит свободных
вхождений x.
5. xF(x)(применяем m.p. к п.1 и аксиоме Р1).
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
14

15.

Правило переименования связанных переменных
Правило переименования связанных переменных.
В исчислении предикатов
-из выводимости xF(x) следует выводимость
yF(y),
- из выводимости xF(x) - выводимость yF(y) при
условии, что F(x) не содержит свободных вхождений y и
содержит свободные вхождения x, ни одно из которых не
входит в область действия квантора по y.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
15

16.  

Доказательство (для квантора общности )
1. ├ xF(x) выводимо (по условию)
2. xF(x) F(y) (аксиома Р1)
3. xF(x)
yF(y) (применяем правило
введения
к п.2)
4. yF(y)(применяем m.p. к п.1. и п.3)
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
16

17.

Теорема дедукции
Если Г, А├ В и существует вывод в
исчислении предикатов,
построенный с применением только
правила 1, то Г├ А В.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
17

18.

Пример
Доказать общезначимость формулы:
x yA(x,y)
y xA(x,y) ,
т.е. докажем, что эта формула – теорема исчисления предикатов.
1.├ yA(x,y)
A(x,z) (применяем аксиому Р1)
2.├ A(x,z)
tA(t,z) (применяем аксиому Р2)
3. применим правило силлогизма к п.1 и п.2
(A
B, B
C├ A
C)
yA(x,y)
tA(t,z)
4. применим правило введения
к п.3:
x yA(x,y)
tA(t,z)
5. применим правило - введения к п.4:├ x yA(x,y)
z tA(t,z)
6. применим правило переименования связанных переменных к п.5:
├ x yA(x,y)
y tA(t,y)
7. применим правило переименования связанных переменных к п.6:
├ x yA(x,y)
y xA(x,y)
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
18

19.  

Полнота исчисления предикатов
Теорема 1.
Всякая доказуемая формула исчисления
предикатов тождественно –
истинна
(общезначима).
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
19

20.

Полнота исчисления предикатов
Теорема 2.
Всякая общезначимая предикатная
формула доказуема в исчислении
предикатов.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
20

21.

Полнота исчисления предикатов
Теорема 3(теорема Гёделя).
Исчисление предикатов – полная
аксиоматическая теория
относительно логики предикатов.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
21

22.

Теорема 4 исчисления
(теорема Чёрча)предикатов
Разрешимость
Теорема 4. (Теорема Чёрча).
Исчисление предикатов
неразрешимо.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
22

23.

Теорема 4 исчисления
(теорема Чёрча)предикатов
Разрешимость
В исчислении предикатов, несмотря на
полноту, разрешающий алгоритм, связанный с
вычислением значений истинных
предикатных формул, построить не удаётся по
причине бесконечности предметной области,
которая приводит в общем случае к
бесконечным таблицам истинности.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
23

24.

Разрешимость исчисления предикатов
Теорема 5.
Исчисление одноместных
предикатов разрешимо.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
24

25.

Непротиворечивость исчисления предикатов
Теорема 6.
Исчисление предикатов
непротиворечиво.
В силу Теоремы 1 невозможно
одновременно
├А и├ ¬А .
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление предикатов»
25

26. Спасибо за внимание

© ФГБОУ ВПО ИжГТУ имени М.Т. Калашникова, 2013
© Исенбаева Елена Насимьяновна, 2013