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

UptoLike

ВУЗ: 

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

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

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 12 из 64
© 2003 Галуев Геннадий Анатольевич
Отметим, что выражения АК1, АК2, АК3 представляют собой не конкретные ак-
сиомы, а схемы аксиом, с помощью которых можно получить бесчисленное множество
аксиом, подставляя в них вместо А, В, С конкретные формулы. Например, если А есть
А
1
→А
2
, В есть ⎤А
3
, то из АК1 получим конкретную аксиому:
А
1
→А
2
→(⎤А
3
→(А
1
→А
2
)).
Отметим также и то, что знаки ⎤ , → в формальной теории выступают просто как
формальные символы, а не как рассматриваемые ранее операции «отрицания», и
«импликации». Учитывая сказанное можно с помощью определений ввести и другие
связки:
А&В есть ⎤(А→⎤В)
А∨В есть ⎤А→В
А↔ есть (А
→В)&(В→А)
Здесь &, ∨, ↔ также трактуются как абстрактные знаки.
Лекция №3
Рассмотрим примеры доказательства теорем в теории L.
Докажем, что для любой формулы А справедливо ├
L
А→А(***).
Для доказательства этого утверждения построим вывод формулы А→А в теории L.
1. (А→((А→А)→А))→((А→(А→А))→(А→А)) (получается подстановкой в схему
аксиом АК2 А→А вместо В и А вместо С)
2. А→((А→А)→А) (получается подстановкой в АК
1 А вместо В)
3. (А→(А→А))→(А→А) (получается из 2 и 1 по правилу МР)
4. А→(А→А) (получается подстановкой в АК! А вместо В)
5. А→А (получается из 4,3 по правилу МР)
Таким образом ├
L
А→А доказано
Докажем, что для любой формулы А справедливо ├
L
(⎤А→А)→А.
1. (⎤А→⎤А)→((⎤А→А)→А) (получаем подстановкой А в АК3 вместо В)
2. ⎤А→⎤А (получаем подстановкой ⎤А в (***) вместо А)
3. (⎤А→А)→А (получаем из 2, 1 по правилу МР)
Таким образом ├
L
(⎤А→А)→А доказано.
Докажем, что для любых А, В, С справедливо А→В, В→С├
L
А→С (****).
1. (А→(В→С))→((А→В)→(А→С)) (схема АК2)
2. (В→С)→((А→(В→С)) (получаем из АК1 подстановкой В→С вместо А и А
вместо В)
3. (В→С) (гипотеза)
4. А→(В→С) (по правилу МР из 3 и 2)
5. (
А→В)→(А→С) (по правилу МР из 4 и 1)
6. (А→В) (гипотеза)
7. А→С (по правилу МР из 6 и 5)
Таким образом (****) доказано.
Важное значение в исчислении высказываний имеет теорема о дедукции. Эта
теорема является теоретическим обоснованием используемого в математических рас-
суждениях приёма: доказывается, что В верно в
предположении о верности некоторо-
го утверждения А, после чего заключается, что верно утверждение «Если А, то В».
Т
Т
е
е
о
о
р
р
е
е
м
м
а
а
(
(
о
о
д
д
е
е
д
д
у
у
к
к
ц
ц
и
и
и
и
)
)
.
. Если Г, А├В, то Г├А
→
В, где: Г – множество формул; А,
В – формулы.
Теорема (о дедукции) впервые явно сформулирована у Эрбрана в 1930г и имела
следующий вид: а) Если А├В, то ├А→В
б) Если А
1
,…,А
m-1
,А
m
├В, то A
1
,…,A
m-1
├A
m
→В
В нашей формулировке теорема учитывает оба случая а) и б) из теоремы Эрбра-
на.

Страницы