Исчисление высказываний. Формальная аксиоматическая теория

1.

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

2. СОСТАВ ТОЧНОЙ ТЕОРИИ

Всякая точная теория определяется:
1)Языком
некоторым
множеством
высказываний, имеющих смысл с точки зрения
этой теории;
2)Совокупностью теорем - подмножеством
языка, состоящего из высказываний, истинных в
данной теории.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
2

3. ИСТОРИЯ ТОЧНОЙ ТЕОРИИ

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

4. ИСТОРИЯ ТОЧНОЙ ТЕОРИИ

До середины 19 века:
-математические теории не выделяли явно все исходные
принципы;
-критерии
строгости
доказательств
и
очевидности утверждений в математике в разные
времена были различны и также явно не
формулировались.
Это приводило к необходимости пересмотра
основ той или иной теории(например, основания
дифференциального и интегрального исчислений,
разработанные в 18 веке Ньютоном и Лейбницем, в 19
веке подверглись серьезному пересмотру).
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
4

5. ИСТОРИЯ ТОЧНОЙ ТЕОРИИ

Конец 19 века:
пересмотр
затронул
общие
принципы
организации
математических теорий. Это привело к созданию новой отрасли
математики – оснований математики.
Предмет оснований математики: строение математических
утверждений и теорий.
Цель оснований математики: дать ответы на вопросы
- «как должна быть построена теория, чтобы в ней
не возникало противоречий?»,
-«какими свойствами должны обладать методы
доказательства, чтобы считаться достаточно
строгими?»
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
5

6. ИСТОРИЯ ТОЧНОЙ ТЕОРИИ

Фундаментальная основа исследования по основаниям
математики- идея формализации теории- последовательного
проведения аксиоматического метода построения теории.
При этом
-не допускается пользоваться какими-либо предложениями об
объектах теории, кроме аксиом;
-аксиомы рассматриваются как формальные последовательности
символов (выражения);
-методы доказательств – как методы получения одних
выражений из других с помощью операций над символами.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
6

7. ИСТОРИЯ ТОЧНОЙ ТЕОРИИ

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

8. АЛГОРИТМ ПОСТРОЕНИЯ ИСЧИСЛЕНИЯ

Исчисление- формальная теория.
1.Определяется множество формул, или правильно построенных выражений,
образующее язык теории.
Это множество задается конструктивными средствами (как правило,
индуктивным определением) → перечислимо. Обычно оно и разрешимо.
2.
Выделяется подмножество формул- аксиом теории.
Множество может быть и бесконечным; во всяком случае, оно должно
быть разрешимо.
3.
Задаются правила вывода теории.
Правила вывода R (F1, F2,…, Fn, G) – это отношение на множестве
формул. Если формулы F1, F2,…, Fn, G находятся в отношении R, то
формула G называется непосредственно выводимой из F1, F2,…, Fn по
правилу R.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
8

9. АЛГОРИТМ ПОСТРОЕНИЯ ИСЧИСЛЕНИЯ

Правило R (F1, F2,…, Fn, G) записывается в виде
(1)
Формулы F1, F2,…, Fn - посылки правила R,
G – следствие(заключение правила R)
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
9

10. ВЫВОД ФОРМУЛЫ

Вывод формулы B из формул A1, A2,…, An последовательность формул F1, F2,…, Fm, :
-Fm=B;
- Fi (i=1..m) это:
– аксиома;
– одна из исходных формул A1, A2,…, An;
– формула,
непосредственно
выводимая
формул F1, F2,…, Fi-1 (или какого-то
подмножества) по одному из правил вывода.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
из
их
10

11. ВЫВОД ФОРМУЛЫ

Существует вывод B из A1, A2,…, An
B выводимо из A1, A2,…, An.
Этот факт обозначается так: A1, A2,…, An├ B.
Формулы A1, A2,…, An - гипотезы или посылки
вывода.
Переход в выводе от Fi-1 к Fi -i-й шаг вывода.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
11

12. СВОЙСТВА ПОНЯТИЯ ВЫВОДИМОСТИ ИЗ СИСТЕМЫ ГИПОТЕЗ

Пусть Г – произвольное множество
формул;
A, B, C – произвольные формулы.
1) Г, A ├ A.
Действительно, вывод формулы A из
системы гипотез Г, A состоит из одной
формулы.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
12

13. СВОЙСТВА ПОНЯТИЯ ВЫВОДИМОСТИ ИЗ СИСТЕМЫ ГИПОТЕЗ

2) Если Г,A,B├ C, то Г, B,A├ C.
где Г – произвольное множество
формул;
A, B, C – произвольные формулы.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
13

14. СВОЙСТВА ПОНЯТИЯ ВЫВОДИМОСТИ ИЗ СИСТЕМЫ ГИПОТЕЗ

3) Если Г├ A и B – произвольная формула, то
Г, B├A.
Действительно, в качестве вывода формулы A из
системы гипотез Г,B можно взять вывод
формулы A из системы гипотез Г,
где Г – произвольное множество формул;
A, B, C – произвольные формулы.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
14

15. СВОЙСТВА ПОНЯТИЯ ВЫВОДИМОСТИ ИЗ СИСТЕМЫ ГИПОТЕЗ

4) Если Г├ А, Г├ B и A,B ├ C, то Г├ С,
где Г – произвольное множество
формул;
A, B, C – произвольные формулы.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
15

16. СВОЙСТВА ПОНЯТИЯ ВЫВОДИМОСТИ ИЗ СИСТЕМЫ ГИПОТЕЗ

5) Если Г ├ A, A ├ B, то Г├ B –
транзитивность.
Непосредственно следует из определения
выводимости.
где Г – произвольное множество формул;
A, B, C – произвольные формулы.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
16

17. ДОКАЗАТЕЛЬСТВО ФОРМУЛЫ

Доказательство формулы B в теории Т -
вывод B из пустого множества
формул- вывод, в котором в качестве
исходных формул используются только
аксиомы.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
17

18. ДОКАЗАТЕЛЬСТВО ФОРМУЛЫ

Формула, доказуемая в теории T
(теорема теории Т)- формула B, для
которой существует доказательство.
Факт доказуемости B обозначается├ B.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
18

19. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

Объект исчисления высказываний- формулы алгебры
логики.
Но
в
исчислении
высказываний
формулы
рассматриваются не как способ представления функций, а
как
составные
высказывания,
образованные
из
элементарных высказываний (переменных) с помощью
логических операций ( v ,&, ,¬).
Истинные высказывания входят в теорию в качестве
общелогических законов.
Задача исчисления высказываний- порождение новых
законов.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
19

20. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

Исчисление высказываний определяется :
1.Алфавит
состоит
из
переменных
высказываний
(пропозициональных букв): A,В,C,…, знаков, логических
связок V,& ,
,¬ ,скобок ( );
2.Формулы:
a) высказывание – есть формула;
b) если А и В – формулы, то AB, A&B, A B, ¬A – формулы;
c) других формул нет;
3.Аксиомы;
4.Правило заключения(modus ponens)- единственное правило
вывода.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
20

21. СИСТЕМЫ АКСИОМ

Cистема аксиом I:
I1. A (B A);
I2. (A B) ((A (B C)) (A C));
I3. (A&B) A;
I4. (A&B) B;
I5. A
(B (A&B));
I6. A (AVB);
I7. B (AVB);
I8. (A C) ((B C)
((AB)
C));
I9. (A C) ((A ¬B)
¬A);
I10. ¬ ¬A A.
Особенность:
использует все логические связки.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
21

22. СИСТЕМЫ АКСИОМ

Система аксиом II:
II1. A (B A)
II2. (A (B C)) ((A B) (A C))
II3. (¬A ¬B) ((¬A B) A)
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
22

23. СИСТЕМЫ АКСИОМ

Система аксиом I и система аксиом II- это схемы
аксиом: вместо пропозициональных букв можно
подставлять произвольные формулы.
Число схем аксиом- конечно.
Число аксиом- бесконечно.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
23

24. СИСТЕМЫ АКСИОМ

Система аксиом I и система аксиом II
порождают одно и то же множество формул
они равносильны.
Доказательство следует из выводимости
аксиом системы II из системы аксиом I и,
наоборот.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
24

25. ПРАВИЛО ЗАКЛЮЧЕНИЯ

Если α и α
β – выводимые
формулы, то β – выводима.
(2)
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
25

26. ПРИМЕРЫ ВЫВОДА В ИСЧИСЛЕНИИ ВЫСКАЗЫВАНИЙ

Пример 1: Покажем, что формула А А выводима из систем аксиом II.
├А А
1. Подставим в аксиому II2 вместо В А А ,
вместо С А.
(А ((А А) А)) ((А (А А)) (А А))
2. Подставим в II1 вместо В
А ((А А) А)
А А:
3. Из шагов 2 и 1 по правилу m. р.:
(А (А А)) (А А)
4. Подставим в II1 вместо В
А (А А)
А:
5. Из шагов 4 и 3 по правилу m. р.:
А А.
Что и требовалось вывести.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
26

27. ПРИМЕР ВЫВОДА В ИСЧЕСЛЕНИИ ВЫСКАЗЫВАНИЙ

Пример 2: Вывести А├ В А.
Пусть А – выводима.
Тогда из А и аксиомы II1 по правилу
m. р. получаем:
А, А ( В А) ├ В А,
что доказывает искомую выводимость.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
27

28. ПРАВИЛО ВЫВОДА

Всякую
доказанную
в
исчислении
высказываний выводимость вида Г├ α ,
где Г – список формул,
α – формула,
можно рассматривать как правило вывода
которое можно присоединить к уже имеющимся.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
28

29. ПРАВИЛО ВЫВОДА

Полученную выводимость А├ В А можно
рассматривать, как правило
:
«если формула α – выводима, то выводима и ,
где - любая формула».
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
29

30. ПРИМЕРЫ ВЫВОДА В ИСЧИСЛЕНИИ ВЫСКАЗЫВАНИЙ

Пример 3:
А В, В С ├ А (А С)
1. По новому правилу
. Пусть В С – выводимая формула, тогда:
В С├ А (В С), где А– любая формула.
2. Из шага 1 и аксиомы ΙΙ2: А (В С)
(А (В С)) ((А В) (А С))
по правилу m.р. следует выводимость (А В) (А С).
3. Из шага 1 и шага 2: В С├ (А В) (А С).
4. Пусть А В выводимая формула, используем результат шага 3 по правилу m.р.:
А В
(А В) (А С)
Отсюда следует выводимость (А С)
5. Учитывая пример 2, получим искомую выводимость:
А С├ А (А С), где А –– любая формула.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
30

31. ОСНОВНЫЕ МЕТАТЕОРЕМЫ ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ

Теорема дедукции
Если Г, α├ β, то Г├ α β ,
(где Г – множество формул; α, β –
формулы)
и, наоборот.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
31

32. ПРИМЕР

В качестве первого применения теоремы дедукции покажем, что аксиома ΙΙ3
выводима из системы аксиом Ι.
Аксиома ΙΙ3: (¬А ¬В) ((¬А В) А)
1 шаг: Подставим в Ι9 вместо А ¬А.
(¬А В) ((¬А ¬В) ¬ ¬А).
2 шаг: Двойное применение теоремы дедукции к шагу 1:
¬А В├ (¬А ¬В) ¬ ¬А
¬А В, ¬А ¬В├ ¬ ¬А.
3 шаг: Из аксиомы Ι10 ¬ ¬АА А следует по m.р., что ¬ ¬А├ А, то по транзитивности
выводимости получим:
¬А В; ¬А ¬В├А.
4 шаг: Переставим гипотезы в полученной выводимости (их порядок неважен, как видно из
определения выводимости):
¬А ¬В; ¬А В├ А.
5 шаг: Применяя 2 раза к шагу 4 теорему дедукции, получим аксиому ΙΙ3:
(¬А ¬В)├ (¬А В) А
├ (¬А ¬В) ((¬А В) А).
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
32

33. МЕТОД ДОКАЗАТЕЛЬСТВА ОТ ПРОТИВНОГО

Предполагаем, что А - верно, и показываем, что
1)из А выводится В;
2)из А выводится ¬В;
Это невозможно А – неверно, т.е. верно ¬А.
Этот метод формулируется как правило:
если Г, А├ В и Г, А├ ¬ В, то Г├ ¬А.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
33

34. МЕТОД ДОКАЗАТЕЛЬСТВА ОТ ПРОТИВНОГО

Доказательство:
1.По теореме дедукции, если Г, А├ В и Г, А├ ¬В,
то
Г├ А В и Г├ А ¬В.
2. Из этих импликаций и Ι9 двойным применением правила m.р.:
А В, (А В) ((А ¬В) ¬А)├ (А ¬В) ¬А
А ¬В, (А ¬В) ¬А├ ¬А, т.е. Г├ ¬А
Это правило введения отрицания.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
34

35. ЗАКОН ИСКЛЮЧЕННОГО ТРЕТЬЕГО

Докажем закон исключенного третьего:├А V ¬А.
1. По аксиоме Ι6 (А (А V В)) при подстановке вместо В ¬А и
правилу m.р.:
А (А V ¬А), А├А V ¬А.
2. Очевидно, ¬(А V ¬А), А├ ¬(А V ¬А).
3. Применим к шагу 1, 2 только что доказанное правило введения отрицания:
¬(А V ¬А)├ ¬А.
4. Аналогично, доказывается ¬(А V ¬А)├ ¬ ¬А.
5.Применяя к шагу 3 и 4 введение отрицания, получим:├ ¬ ¬(А V ¬А).
6. С помощью аксиомы Ι10 и правила m.р. снимаем двойное отрицание
в шаге 5:
├ А V ¬А.
Курс «Математическая логика и теория алгоритмов»
Тема «Исчисление высказываний. Формальная аксиоматическая теория»
35

36.

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