37. Примеры формальных теорий. Теоремы и метатеоремы.

Шахматы - пример формальной теории

• Игра в шахматы – назовем это теорией Ch. Формулами в Ch будем считать позиции (всевозможные расположения фигур на доске вместе с указанием «ход белых» или «ход черных»). Тогда аксиомой теории Ch естественно считать начальную позицию, а правилами вывода – правила игры. Правила позволяют получать из одних формул другие. В частности, отправляясь от нашей единственной аксиомы, мы можем получать теоремы Ch. Общая характеристика теорем Ch состоит, очевидно, в том, что это – всевозможные позиции, которые могут получиться, если передвигать фигуры, соблюдая правила.

• В чем выражается формальность теории Ch? Если некто предлагает нам «математический текст» и утверждает, что это – доказательство теоремы A в теории Ch, то ясно, что речь идет о непроверенной записи шахматной партии, законченной (или отложенной) в позиции A.

• Правила игры сформулированы настолько точно, что можно составить программу для вычислительной машины, которая будет осуществлять такие проверки. (Еще раз напомним, что речь идет о проверке правильности записи шахматной партии, а не о проверке того, можно ли заданную позицию получить, играя по правилам, – эта задача намного сложнее!)

Формальная теория L

Пусть {a, b} есть алфавит теории L. Формулами в теории L являются всевозможные цепочки, составленные из букв a, b, например a, aa, aba, abaab.

Единственной аксиомой L является цепочка a, наконец, в L имеется два правила вывода: Такая запись означает, что в теории L из цепочки X непосредственно выводятся Xb и aXa. Примером теоремы L является цепочка aababb;

вывод для нее есть a, ab, aaba, aabab, aababb.

Формальные теории являются не просто игрой ума, а всегда представляют собой модель какой-то реальности (либо конкретной, либо математической).

• Вначале математик изучает реальность, конструируя некоторое абстрактное представление о ней, т. е. некоторую формальную теорию.

• Затем он доказывает теоремы этой формальной теории. Вся польза и удобство формальных теорий как раз и заключается в их абстрагировании от конкретной реальности. Благодаря этому одна и та же формальная теория может служить моделью многочисленных конкретных ситуаций.

• Наконец, он возвращается к исходной точке всего построения и дает интерпретацию теорем, полученных при формализации.

Теоремы и метатеоремы

• При изучении формальных теорий нужно различать теоремы формальной теории и теоремы о формальной теории, или

метатеоремы. Это различие не всегда явно формализуется, но всегда является существенным.

• Множество теорем формальной теории является точно определенным объектом (обычно бесконечным) и поэтому можно доказывать утверждения, относящиеся ко всем теоремам одновременно.

• Например, в теории Ch множество всех теорем оказывается, правда, конечным (хотя конечность эта с практической точки зрения ближе к бесконечности). Легко доказать следующее утверждение, относящееся ко всем теоремам Ch: ни в одной теореме белые не имеют 10 ферзей. В самом деле, достаточно заметить, что в аксиоме Ch белые имеют одного ферзя и восемь пешек и что по правилам игры белым ферзем может стать только белая пешка. Остальное решает арифметика:

1+8<10. Таким образом, мы подметили в системе аксиом и правил вывода теории Ch особенности, которые делают справедливым наше общее утверждение о теоремах Ch.

• Аналогичные возможности имеем в случае теории L. Можно доказать например, следующее утверждение, относящееся ко всем теоремам L: если X – теорема, то aaX – тоже теорема.