ИсчВ

1.

Исчисление высказываний

2.

• Исчисление высказываний представляет
собой множество выводимых формул в
данном алфавите при данном наборе
аксиом и правил вывода.

3.

• Исчисление высказываний – формальная
теория, в которой заданы:
1. Алфавит:
• переменные - x, y, z, xi ;
• логические связки ,
можно ввести связки
(дополнительно
, т.к.
)
• ( ) – технические символы (, не является
символом алфавита).

4.

2. Язык. Состоит из слов. Словом (формулой
исчисления) называют любую конечную
последовательность символов алфавита.
3. Правильно построенные формулы (ППФ).
других ППФ нет.

5.

4. Аксиомы (Чёрча).
А 1:
А2:
А3: ( А В ) ( В А)

6.

5. Правило вывода.

7.

6. Вывод формулы - конечная
последовательность формул
А1, А2, …, Аn, такая, что:
последняя формула совпадает с выводимой;
каждая формула вывода является либо
аксиомой, либо получена из предыдущих по
МР.

8.

Среди следующих формул укажите те, которые
являются аксиомами (уточнив, какими).

9.

Первые теоремы ИВ
• Д-во первых теорем выглядит громоздко и
непредсказуемо.
• В дальнейшем выводятся некоторые
правила, которые будут предсказывать д-во
теорем.
• Ⱶ А – формула А выводима.

10.

11.

12.

13.

14.

15.

16.

• Выясните, является ли данная последовательность формул
выводом из аксиом. Если является, то обоснуйте каждый
шаг построения этой последовательности.

17.

Выводимость из гипотез
• Пусть даны формулы – гипотезы А1, А2, …, Аn
• Нужно доказать А1, А2, …, Аn Ⱶ F
• Совокупность этих гипотез обозначим Г
• Выводом (доказательством) формулы F из
гипотез Г называется последовательность
формул F1, F2, …, Fn, в которых последняя
формула совпадает с F и каждая Fi – аксиома
или получена из предыдущих по МР.

18.

Свойства выводимости из гипотез
1. Если Г, А⊢А (самовыводимость).
2. Если Г⊢А, то Г, В⊢А (расширение списка
гипотез).
3. Если Г, А⊢В, Г⊢А, то Г⊢В (удаление).
4. Если Г⊢А, А⊢В, то Г⊢В (транзитивность).
5. Если Г, А,В⊢С, то Г, В,А⊢С
(коммутативность).
6. Если Г, А, А⊢В, то Г, А⊢В (сокращение).

19.

Выясните, является ли данная последовательность выводом
из гипотез. Если да, то укажите, выводом из каких формул, и
какой формулы является.

20.

Теорема дедукции (ТД)
• выявляет некоторую общую
закономерность при построении вывода и
облегчает процесс построения
доказательства.
• Если Г, В ├ А, то Г ├ В → А,
где Г - это набор некоторых формул
Г={F1, F2, ..., Fn}.

21.

Связь ⊢ и
• Наличие МР и ТД позволяет взаимно
заменять знаки.
Г, А⊢В Г⊢А В
• МР: А, А В
В
А, А В ⊢ В

22.

• Если ТД применять в качестве аксиомы, то
А1, А2 можно доказать как теоремы.
• Докажем
А1: ⊢А (В А)
Т1
Анализ:
ТД
А ⊢ В А
ТД
А , В ⊢А

23.

• Д-во:
1) А , В ⊢А
2) А ⊢ В А
3) А1: ⊢А (В А)
10
1), ТД
2), ТД

24.

Докажем А2: ⊢(А (В С)) (А В) (А С)
Анализ:
ТД
(А (В С)) ⊢ (А В) (А С)
ТД
А (В С), А В ⊢ А С
ТД
А (В С), А В, А⊢С
Т2

25.

• Д-во:
1) А (В С), А В, А⊢В
МР
2) А (В С), А В, А⊢В С
МР
3) А (В С), (А В), А⊢С
1),2), МР
4) А (В С), А В ⊢ А С
3), ТД
5) (А (В С)) ⊢ (А В) (А С)
4), ТД
6) ⊢(А (В С)) (А В) (А С) 5), ТД

26.

• Докажем А В, В С ⊢ А С
Т3
Анализ:
ТД
А В, В С, А⊢С
Д-во:
1) А В, В С, А⊢В
МР
2) А В, В С, А, В⊢С
1), МР
3) А В, В С, А⊢С
1), 2), 30
4) А В, В С ⊢ А С
4), ТД

27.

• Докажем А В⊢ В А
Д-во:
Т4
1) А А, А В⊢ А В
Т3
2) А В, В В⊢ А В
Т3
3) А В⊢ А В
1), 2), 40

28.

4) А В⊢ В А
А3
5) А В⊢ В А
3), 4), 40

29.

Т5

30.

Производные правила вывода
• Лемма – доказанное утверждение,
полезное для доказательства других
утверждений.

31.

Lemma 1 (удаление &)
Из & двух высказываний выводится каждый член
АВ ⊢А
Анализ:
А В ⊢ А
Д-во:
закон контрапозиции
1) А, В А 10
А ⊢ А В
2) А , А В 1),конт.
ТД
3) А ⊢ А В 2),ТД
А,А⊢В
4) А В ⊢ А 3), конт.
закон контрапозиции
А, В ⊢ А
5) АВ ⊢А

32.

Lemma 2 (удаление &)
Анализ:
АВ ⊢В
А В ⊢ В
закон контрапозиции
В ⊢ А В
ТД
В , А В
Д-во:
1) В, А ⊢ В 10
2) В ⊢ А В 1), ТД
3) А В ⊢ В 2), конт.
4) АВ ⊢В

33.

Lemma 3 (введение &)
А,В ⊢АВ
Анализ: А, В⊢ А В
закон контрапозиции
А, А В⊢В
Д-во:
1) А, А В⊢В
(МР)
2) А, В⊢ А В 1), контр.
3) А,В ⊢АВ

34.

Lemma 4 (введение V)
Анализ:
А ⊢АvB
А ⊢ А В
ТД
А, А ⊢ В
контр.
А, В ⊢ А
Д-во:
1) А, В А 10
2) А , А В 1),конт.
3) А ⊢ А В 2), ТД
4) А ⊢АvB
Lemma 5 (введение V) В ⊢АvB (ВvA)

35.

Lemma 6 (удаление v)
Если А ⊢С, В ⊢С, то АvB⊢С
Д-во:
1) А ⊢С – дано
2) С⊢А
3) В ⊢С – дано
4) С⊢В
5) А,В ⊢А∙В (А В)
6) С⊢ А В
7) А В ⊢С
8) АvB⊢С
1), контр.
3), контр.
введ. &
2),4),5),40
6), контр.

36.

Операции
→
&
V
┐
Введение
Удаление

37.

Доказать: АvBC⊢(AvB)∙(AvC)
Анализ:вв.&
АvBC⊢AvB,
АvBC⊢AvC
уд. V
уд. V
А⊢AvB, BC⊢AvB
А⊢AvC, BC⊢AvC
уд. &уд. &
B,C⊢AvB
B,C⊢AvC
Д-во:
1) А⊢AvB(вв. v)
2) B,C⊢AvB (вв. v)
Обоснование замены
3) BC⊢B (уд. &)
B,C на ВC
4) BC⊢C (уд. &)
5) BC⊢AvB (2), 3),40)
6) АvBC⊢AvB (5), уд.&)
7) А⊢AvC(вв. v)
10) АvBC⊢AvC (7), 9), уд. v)
8) B,C⊢AvС(вв. v)
11) АvB, AvC⊢(AvB)∙(AvC) (10), вв. &)
9) BC⊢AvC (8), уд.&)
12) АvBC⊢(AvB)∙(AvC) (6), 10),11),40)

38.

Теорема о полноте
• Если формула F является тавтологией, то
тогда F — выводима.