Математическая логика и теория алгоритмов. Галуев Г.А. - 14 стр.

UptoLike

ВУЗ: 

ТТИ ЮФУ | Таганрог

Составители: 

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 14 из 64
© 2003 Галуев Геннадий Анатольевич
4. (⎤А→⎤⎤А)→((⎤А→⎤А)→А) (по схеме АК3 с А вместо В, и ⎤А вместо А)
5. ⎤А→⎤А (из (***), т.е. ├
L
А→А с ⎤А вместо А)
6. (⎤А→⎤⎤А)→А (из 4,5 и (*****), т.е. А→(В→С), В├А→С с (⎤А→⎤⎤А) вместо А,
(⎤А→⎤А) вместо В, и А вместо С)
7. ⎤⎤А→(⎤А→⎤⎤А) (по схеме АК1 с ⎤⎤А вместо А и
⎤А вместо В)
8. ⎤⎤А→А (из 6,7 и (****), т.е. А→В, В→С├А→С с ⎤⎤А вместо А, (⎤А→⎤⎤А) вместо В
и А вместо С)
9. ⎤⎤А (гипотеза)
10.А (по правилу МР из 9 и 8)
Таким образом доказано, что ⎤⎤А→А. Теперь нетрудно доказать, что
А→В├⎤⎤А→⎤⎤В.
11.А→В (гипотеза)
12.В (по правилу МР из 10,11)
Если В├⎤⎤В, то отсюда будет вытекать, что ⎤⎤А, А→В├⎤⎤В.
13.(⎤⎤⎤В→⎤В)→((⎤⎤⎤В→В)→⎤⎤В) (по схеме АК3 с ⎤⎤В вместо В, и В вместо А)
14.⎤⎤⎤В→⎤В (из
(1) с ⎤В вместо А)
15.(⎤⎤⎤В→В)→⎤⎤В (по правилу МР из 14,13)
16.В→(⎤⎤⎤В→В) (из схемы АК1 с В вместо А и ⎤⎤⎤В вместо В)
17.В→⎤⎤В (из 16,15 и (****), т.е. А→В, В→С├А→С с В вместо А, ⎤⎤⎤В вместо В и
⎤⎤В
вместо С)
18.В (гипотеза)
19.⎤⎤В (по правилу МР из 18,17)
Таким образом доказано, что В├⎤⎤В (2)
Следовательно, ⎤⎤А, А→В├⎤⎤В, откуда по теореме о дедукции следует:
20.А→В├⎤⎤А→⎤⎤В
21.(⎤⎤А→⎤В)→⎤А (из 20 и 3 по правилу МР)
Докажем теперь, что А→⎤В├⎤⎤
А→⎤В.
22.⎤⎤А, А→⎤В├⎤В (из (1) по правилу МР)
23.А→⎤В├⎤⎤А→⎤В (из 22 по теореме о дедукции)
24.⎤А (из 23 и 21 по правилу МР)
Таким образом доказано, что Г├⎤А или Г, А├В и Г, А├⎤В, что и требовалось дока-
зать.
Рассмотрим ещё
одно утверждение, показывающее, что из противоречия А и ⎤А
выводима любая формула В.
Утверждение 2.
Для любых формул А и В справедливо: А, ⎤А├В
(3)
Доказательство.
1. А, ⎤А, ⎤В├А приведение к абсурду в
2. А, ⎤А, ⎤В├⎤А соответствии с утверждением 1
3. А, ⎤А├⎤⎤В (из 1 и 2 в соответствии с утверждением ├
L
А→А (***))
4. А, ⎤А├В (из 3 и (1) (⎤⎤А├А) с В вместо А)
Непротиворечивость и полнота исчисления высказываний.
Непротиворечивость. Исчисление высказываний (как и вообще любая формаль-
ная система, имеющая символ ⎤ - отрицания) называется непротиворечивой системой,
если ни для какой формулы А, формулы А и ⎤А не являются обе
доказуемыми в этой
системе, и противоречивой в противном случае.
Для исчисления высказываний это определение эквивалентно следующему. Сис-
тема непротиворечива, если в ней имеется некоторая недоказуемая формула; проти-
воречива, если любая формула доказуема.
Действительно, если ├А (А – теорема) и ├⎤А (⎤А – теорема), то в силу доказанно-
го утверждения 2 имеем ├
В и для любой формулы В.
⎭
⎬
⎫

Страницы