ВУЗ:
Составители:
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 будем считать позиции (всевозмож-
ные расположения фигур на доске вместе с указанием «ход белых» или «ход черных»).
Тогда аксиомой теории Ch естественно считать начальную позицию, а правилами выво-
да – правила игры, которые определяют, какие ходы допустимы в каждой позиции. Пра-
вила позволяют получать из одних формул другие. В частности, отправляясь от нашей
единственной аксиомы, мы можем получать теоремы Ch. Общая характеристика теорем
Ch состоит, очевидно, в том, что это – всевозможные позиции, которые могут получиться,
если передвигать фигуры, соблюдая правила.
9
Страницы
- « первая
- ‹ предыдущая
- …
- 7
- 8
- 9
- 10
- 11
- …
- следующая ›
- последняя »
