Похожие презентации:
Исчисление высказываний. Формальная аксиоматическая теория
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,…, AnB выводимо из 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