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

UptoLike

ВУЗ: 

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

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

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 11 из 64
© 2003 Галуев Геннадий Анатольевич
Под словом «эффективно» подразумевается то, что существует некоторая предо-
пределённая последовательность действий (т.е. алгоритм, процедура), позволяющая
за конечное число шагов ответить на требуемый вопрос положительно или отрица-
тельно.
Выводом в теории Т называется всякая конечная последовательность А
1
,…,А
n
формул такая, что для любого i формула А
i
есть либо аксиома теории Т, либо непо-
средственное следствие каких-либо предыдущих формул по одному из правил выво-
да.
Формула А теории Т называется теоремой этой теории, если существует вывод в
Т, в котором последней формулой является А. Такой вывод называется доказательст-
вом (выводом) формулы А.
Следует отметить, что понятие
теоремы не обязательно эффективно, т.е. может и
не существовать эффективной процедуры, позволяющей определить по данной фор-
муле, существует ли её вывод в теории Т. Теория, для которой такой алгоритм суще-
ствует называется разрешимой, в противном случае – неразрешимой.
Формула А является следствием множества формул Г в теории Т тогда и только
тогда, когда существует такая конечная последовательность формул А
1
,…,А
n
, что А
n
есть А и для каждого i A
i
есть либо аксиома, либо элемент Г, либо непосредственное
следствие некоторых предыдущих формул по одному из правил вывода. Такая после-
довательность называется выводом А из Г. Члены множества формул Г называются
гипотезами или посылками вывода. Утверждение типа «А есть следствие Г» обозна-
чают Г├А (можно читать «Г даёт А»). Для
указания того, что А есть следствие Г имен-
но в теории Т пользуются обозначением Г├
т
А. Для конечного множества Г={В
1
,…,В
n
},
(где В
i
∈
Г элементы множества Г) вместо {В
1
,…,В
n
}├
т
А обычно пишут В
1
,…,В
n
├
т
А.
Если Г пустое множество ∅ (т.е. множество не содержащее ни одного элемента),
то Г├А тогда и только тогда, когда А является теоремой (т.е. аксиомой или формулой
выводимой из аксиомы). Вместо ∅├А пишут ├А (т.е. А теорема).
Очевидными являются следующие свойства понятия выводимости:
1. Если
Г Δ⊆ (т.е. «Г подмножество
Δ
», «Г включается в
Δ
») и Г├А, то Δ├А. Т.е.
если А выводимо из Г, то оно выводимым будет если к Г добавить новые
посылки.
2. Г├А тогда и только тогда, когда в Г существует конечное подмножество Δ, для
которого Δ├А. Достаточность условия вытекает из предыдущего свойства.
Необходимость вытекает из
того, что каждый вывод А из Г использует
лишь конечное число посылок из Г.
3. Если Δ├А и Г├В для любого В из множества Δ, то Г├А, т.е. если А выводима из
Δ и каждая формула из Δ выводима из Г, то А выводима из Г.
Рассмотрим
теперь формальную аксиоматическую теорию L для классического
исчисления высказываний (Д. Гильберт, П. Бернайс, С. Клини):
I. Символами L являются ⎤, →, (,) и буквы А с целыми положительными
числами в качестве индексов: А
1
, А
2
,… Символы ⎤ , → называют при-
митивными связками, а буквы А
1
, А
2
,… - пропозиционными буквами;
II. а) Все пропозиционные буквы А
i
б) Если А и В формулы, то (⎤А) и (А→В) – тоже формулы
в) Никаких других формул, кроме определённых согласно а) и б)
нет.
III. Каковы бы ни были формулы А, В, С теории L, следующие формулы
есть аксиомы L:
(АК1) А→(В→А)
(АК2) (А→(В→С))→((А
→В)→(А→С))
(АК3) (⎤В→⎤А)→((⎤В→А)→В)
IV. Единственное используемое правило вывода: В есть непосредствен-
ное следствие А и А→В. Это записывают в виде:
А и А→В – посылки А, А→В
Это правило называют modus В – за-
ключение В ponens (МР) или правило отделения

Страницы