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

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

(всевозможные расположения фигур на доске вместе с указанием «ход белых» или «ход
черных»). Тогда аксиомой теории Ch естественно считать начальную позицию, а
правилами вывода – правила игры, которые определяют, какие ходы допустимы в
каждой позиции. Правила позволяют получать из одних формул другие. В частности,
отправляясь от нашей единственной аксиомы, мы можем
получать теоремы Ch. Общая
характеристика теорем Ch состоит, очевидно, в том, что это – всевозможные позиции,
которые могут получиться, если передвигать фигуры, соблюдая правила.
В чем выражается формальность теории Ch? Если некто предлагает нам
«математический текст» и утверждает, что это – доказательство теоремы A в теории Ch, то
ясно, что речь идет
о непроверенной записи шахматной партии, законченной (или
отложенной) в позиции A. Проверка не является, однако, проблемой: правила игры
сформулированы настолько точно, что можно составить программу для вычислительной
машины, которая будет осуществлять такие проверки. (Еще раз напомним, что речь идет о
проверке правильности записи шахматной партии, а не о проверке того,
можно ли
заданную позицию получить, играя по правилам, – эта задача намного сложнее!)
Несколько серьезнее другой пример формальной теории. Пусть {a, b} есть алфавит
теории L. Формулами в теории L являются всевозможные цепочки, составленные из букв
a, b, например a, aa, aba, abaab. Единственной аксиомой L является цепочка a, наконец, в
L имеется два правила вывода:
aXa
X
и
Xb
X
.
Такая запись означает, что в теории L из цепочки X непосредственно выводятся Xb и aXa.
Примером теоремы L является цепочка aababb; вывод для нее есть
a, ab, aaba, aabab, aababb.
Формальные теории являются не просто игрой ума, а всегда представляют собой
модель какой-то реальности (либо конкретной, либо математической).
Вначале математик
изучает реальность, конструируя некоторое абстрактное представление о ней, т. е.
некоторую формальную теорию. Затем он доказывает теоремы этой формальной теории.
Вся польза и удобство формальных теорий как раз и заключается в их абстрагировании от
конкретной реальности. Благодаря этому одна и та же формальная теория может служить
моделью многочисленных конкретных
ситуаций. Наконец, он возвращается к исходной
точке всего построения и дает интерпретацию теорем, полученных при формализации.
При изучении формальных теорий нужно различать теоремы формальной теории и
теоремы о формальной теории, или метатеоремы. Это различие не всегда явно
формализуется, но всегда является существенным.
Множество теорем формальной теории является точно определенным объектом
(обычно бесконечным) и поэтому можно доказывать утверждения, относящиеся ко всем
теоремам одновременно. Например, в теории Ch множество всех теорем оказывается,
правда, конечным (хотя конечность эта с практической точки зрения ближе к
бесконечности). Легко доказать следующее утверждение, относящееся ко всем теоремам
Ch: ни в одной теореме белые не имеют 10 ферзей. В
самом деле, достаточно заметить,
что в аксиоме Ch белые имеют одного ферзя и восемь пешек и что по правилам игры
белым ферзем может стать только белая пешка. Остальное решает арифметика: 1+8<10.
Таким образом, мы подметили в системе аксиом и правил вывода теории Ch особенности,
которые делают справедливым наше общее утверждение о теоремах
Ch.
Аналогичные возможности имеем в случае теории L. Можно доказать, например,
следующее утверждение, относящееся ко всем теоремам L: если X – теорема, то aaX –
тоже теорема.

Страницы