СОСТАВ ТОЧНОЙ ТЕОРИИ
ИСТОРИЯ ТОЧНОЙ ТЕОРИИ
ИСТОРИЯ ТОЧНОЙ ТЕОРИИ
ИСТОРИЯ ТОЧНОЙ ТЕОРИИ
ИСТОРИЯ ТОЧНОЙ ТЕОРИИ
ИСТОРИЯ ТОЧНОЙ ТЕОРИИ
АЛГОРИТМ ПОСТРОЕНИЯ ИСЧИСЛЕНИЯ
АЛГОРИТМ ПОСТРОЕНИЯ ИСЧИСЛЕНИЯ
ВЫВОД ФОРМУЛЫ
ВЫВОД ФОРМУЛЫ
СВОЙСТВА ПОНЯТИЯ ВЫВОДИМОСТИ ИЗ СИСТЕМЫ ГИПОТЕЗ
СВОЙСТВА ПОНЯТИЯ ВЫВОДИМОСТИ ИЗ СИСТЕМЫ ГИПОТЕЗ
СВОЙСТВА ПОНЯТИЯ ВЫВОДИМОСТИ ИЗ СИСТЕМЫ ГИПОТЕЗ
СВОЙСТВА ПОНЯТИЯ ВЫВОДИМОСТИ ИЗ СИСТЕМЫ ГИПОТЕЗ
СВОЙСТВА ПОНЯТИЯ ВЫВОДИМОСТИ ИЗ СИСТЕМЫ ГИПОТЕЗ
ДОКАЗАТЕЛЬСТВО ФОРМУЛЫ
ДОКАЗАТЕЛЬСТВО ФОРМУЛЫ
ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ
ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ
СИСТЕМЫ АКСИОМ
СИСТЕМЫ АКСИОМ
СИСТЕМЫ АКСИОМ
СИСТЕМЫ АКСИОМ
ПРАВИЛО ЗАКЛЮЧЕНИЯ
ПРИМЕРЫ ВЫВОДА В ИСЧИСЛЕНИИ ВЫСКАЗЫВАНИЙ
ПРИМЕР ВЫВОДА В ИСЧЕСЛЕНИИ ВЫСКАЗЫВАНИЙ
ПРАВИЛО ВЫВОДА
ПРАВИЛО ВЫВОДА
ПРИМЕРЫ ВЫВОДА В ИСЧИСЛЕНИИ ВЫСКАЗЫВАНИЙ
ОСНОВНЫЕ МЕТАТЕОРЕМЫ ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ
ПРИМЕР
МЕТОД ДОКАЗАТЕЛЬСТВА ОТ ПРОТИВНОГО
МЕТОД ДОКАЗАТЕЛЬСТВА ОТ ПРОТИВНОГО
ЗАКОН ИСКЛЮЧЕННОГО ТРЕТЬЕГО
2.19M
Категория: МатематикаМатематика

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

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
English     Русский Правила