Теория алгоритмов. Зюзысов В.М. - 25 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

Выводимость
Пусть A
1
, A
2
,…, A
n
, A − формулы теории T. Если существует такое правило вывода
R, что < A
1
, A
2
,…, A
n
, A> ∈ R, то говорят, что формула A непосредственно выводима из
формул A
1
, A
2
,…, A
n
по правилу вывода R. Обычно этот факт записывают следующим
образом:
R
A
AAA
n
,...,,
21
,
где формулы A
1
, A
2
,..., A
n
называются посылками, а формула A − заключением.
Выводом формулы A из множества формул Γ в теории T называется такая
последовательность F
1
, F
2
,..., F
k
, что A = F
k
, а любая формула F
i
(i < k) является либо
аксиомой, либо F
i
∈Γ, либо непосредственно выводима из ранее полученных формул
(j
n
jj
FF ,...,
1
1
,..., j
n
< i). Если в теории T существует вывод формулы A из множества
формул Γ, то это записывается следующим образом:
Γ |−
T
A,
где формулы из Γ называются гипотезами вывода. Если теория T подразумевается, то её
обозначение обычно опускают.
Если множество Γ конечно: Γ = {B
1
, B
2
,..., B
n
}, то вместо {B
1
, B
2
,..., B
n
}|− A пишут
B
1
, B
2
,..., B
n
|− A. Если Γ есть пустое множество ∅, то A называют теоремой (или
доказуемой формулой) и в этом случае используют сокращенную запись |− A («A есть
теорема»).
Отметим, что в соотношении {теоремы} ⊂ {формулы} ⊂ {выражения} включение
множеств является строгим.
Приведем несколько простых свойств понятия выводимости из посылок.
1. Если Γ⊆Σ и Γ |− A, то Σ |− A.
Это свойство выражает тот факт, что если A выводимо из множества гипотез Γ, то
оно остается выводимым, если мы добавим к Γ новые гипотезы.
2. Γ |− A тогда и только тогда, когда в Γ существует конечное подмножество Σ, для
которого Σ |−
A.
Часть «тогда» утверждения 2 вытекает из утверждения 1. Часть «только тогда»
этого утверждения очевидна, поскольку всякий вывод A из Γ использует лишь конечное
число гипотез из Γ.
3. Если Σ |− A и Γ|− B для любого B из множества Σ, то Γ |− A.
Смысл этого утверждения прост: если A
выводимо из Σ и любая формула из Σ
выводима из Γ, то A выводима из Γ.
Понятие формальности можно определить в терминах теории алгоритмов: теорию
T можно считать формальной, если построен алгоритм (механически применяемая
процедура вычисления) для проверки правильности рассуждений с точки зрения
принципов теории T. Это значит, что если
некто предлагает математический текст,
являющийся, по его мнению, доказательством некоторой теоремы в теории T, то,
механически применяя алгоритм, мы можем проверить, действительно ли предложенный
текст соответствует стандартам правильности, принятым в T. Таким образом, стандарт
правильности рассуждений для теории T определен настолько точно, что проверку его
соблюдения можно передать вычислительной машине (следует помнить
, что речь идет о
проверке правильности готовых доказательств, а не об их поиске!). Если проверку
правильности доказательств в какой-либо теории нельзя передать вычислительной
машине, и она доступна в полной мере только человеку, значит, еще не все принципы
теории аксиоматизированы (то, что мы не умеем передать машине, остается в нашей
интуиции и «оттуда» регулирует наши рассуждения).
В качестве несерьезного примера формальной теории можно рассматривать игру в
шахматы – назовем это теорией Ch. Формулами в Ch будем считать позиции

Страницы