Кузнецов О.П., Адельсон-Вельский Г.М. - Дискретная математика для инженеров (1048837), страница 51
Текст из файла (страница 51)
По существу при этом ставится под сомнение первоначальная, кмаксималистская» программа финитного подхода: нельзя построить математику как некоторую фиксированную совокупность средств, которые можно было бы объявить единственно законными и с их помощью строить метатеории любых теорий. С другой стороны, не следует истолковывать результаты Геделя (как это иногда делается, в основном среди непрофессионалов) как крах формального подхода. Наличие алгоритмически неразрешимых проблем вовсе не бросает тень на теорию алгоритмов, а лишь сообшает «суровую правду» об устройстве мира, изучаемого этой теорией. Из этой правды не вытекает, что алгоритмический, конструктивный подход к решению проблемы не пригоден; хотя он чего-то и не может, но лишь потому, что этого не может никто.
Точно так же невозможность полной формализации содержательно определенных теорий — это не недостаток подхода или концепции, а объективный факт, неустранимый никакой концепцией. Формальный подход остается основным конструктивным средством изучения множеств высказываний. Невозможность адекватной формализации теории означает, что надо либо искать формализуемые ее фрагменты, либо строить какую-то более сильную формальную теорию, которая, правда, снова будет неполна, но, быть может, будет содержать всю исходную теорию. В частности, методами, не формализуемыми в формальной арифметике, Генцен доказал непротиворечивость формальной арифметики.
64, АБСТРАКТНЫЕ ФОРМАЛЬНЫЕ СИСТЕМЫ Дальнейшие примеры формальных систем. Исторически формальные системы создавались с конкретной целью более точного обоснования методов построения математических теорий, Однако постепенно стало ясно, что на основе тех же принципов — исходного набора аксиом, правил вывода и понятия выводимости — можно описывать не только множества выражений, интерпретируемых как высказывания, но н перечислимые множества объектов произвольного вида.
Основы теории' таких формальных систем были заложены Э. Постом, Эту теорию можно назвать абстрактной (хотя этот термин и не является общеприыятым) или общей, так как она — в отличие от метатеории логических исчислений — не рассматривает свойства формальных систем относительно их конкретных интерпретаций, а изучает лишь их внутренние, синтаксические свойства.
Прежде чем перейти к самой теории, рассмотрим некоторые примеры формальных систем, не связанных с логическими интерпретациями. Пример 6.6. а. Множество допустимых шахматных позиций можно описать как формальную систему, в которой единственной аксиомой является начальная позиция, правилами вывода — правила игры, а теоремами — позиции, полученные по правилам игры из начальной.
Однако эта идея требует уточнения. Пусть дана позиция, скажем, ее диаграм- ' Начиная с этого момента понятие «теория» употребляется в обычном интуитивном смысле и не имеет прямого отношения к точному понятию «формальной теории», рассмотренному в прелыдущнх параграфах. 246 ма или описание в шахматной нотации. Для того, чтобы однозначно получить все позиции, достижимые из данной за один ход, недостаточно знать правила хода всех фигур, в том числе правила взятия и правило превращения пешки; может понадобиться информация, пе содержащаяся явно в позиции, нужно знать: 1) чей ход; 2) ходил ли раньше король (если он стоит на своем начальном поле, позиция на этот вопрос не отвечает) — это нужно для определения допустимости рокировки; 3) не был ли последний ход ходом пешки через два поля — это нужно для определения взятия пешки на проходе. Чтобы превратить множество шахматных позиций в формальную систему, нужно за позицию принять такое ее описание, которое в явном виде содержит ответы на все три вопроса.
Для исключения позиций, получающихся после взятия королей, надо ввести правила, запрещающие игнорировать шах, и понятие заключительных позиций (матовых и патовых), после которых ппкакис ходы не разрешаются. б. Многие индуктивные определения можно превратить в формальные системы, аксиомы которых перечислены в базисе (первом пункте) определения, а правила вывода— в индуктивном шаге.
Необходимым условием перехода к формальной системе является конструктивность задания аксиом и правил вывода, точнее, разрешимость множества аксиом и отношения непосредственной выводимости. Рассмотрим, например, индуктивное определение абстрактной ориентированной двухполюсной схемы. 1. Пусть зафиксировано конечное число объектов, которые назовем элементами; в каждом элементе выделены два полюса: вход и выход.
Элемент является схемой, полюсы которой совпадают с полюсами элемента. 2. Пусть 5~ и 5,— схемы. Тогда объекты, получающиеся; а) путем отождествления выхода 5, со входом 5з (правило последовательного соединения); б) путем отождествления входа 5~ со входом 5з и выхода 5, с выходом 5з (правило параллельного соединения), также являются схемами. В случае 2а входом схемы является вход 5ь выходом — выход 5,.
В случае 26 входом является объединенный вход 5ь 5,, выходом — объединенный выход 5ь 5, Это определение описывает формальную систему, в которой аксиомами являются элементы с выделенными полюсами, а правилами вывода — правила соединения схем.
Лю- бой инженер даст этой системе обычную схемную (в инженерном смысле слова, как правило, электротехническую) интерпретацию; однако такая интерпретация вовсе не вытекает из определения. В понятие элемента не вкладывается никакого содержания; единственное, что от него требуется, — возможность эффективно распознавать полюсы. Элементом может быть ориентированное ребро, полюсы которого — вершины; тогда схемы — это просто графы с выделенным входом (источником) и выходом (стоком).
(Вопрос к читателю: все ли такие графы порождаются данной формальной системой?) Другая возможная интерпретация: элементы — одноместные функции; последовательное соединение — композиция функций, т. е. их последовательное вычисление, а параллельное соединение — параллельное вычисление двух функций с одинаковыми исходными данными и суммированием результатов в конце. При описании формальных систем в примере 6.6 была допущена одна вольность, которая, строго говоря, недопустима.
Дело в том, что ни в одном из этих описаний не зафиксирован алфавит; соответственно и правила вывода не сформулированы как операции над символами в словах. Можно, конечно, сказать, что «примерно понятно, как это сделать; детали не уточняются», но способы уточнения могут быть различными и приведут к различным формальным системам. Это обстоятельство известно всем, кто занимался программированием игры в шахматы или машинными преобразованиями схем. Да и вообще любой, кто программировал содержательно сформулированные алгоритмы, знает, что начинать приходится с выбора формы представления данных, т. е. символического кодирования объектов в терминах языка программирования (а в случае автокода — просто машинными словами), причем различные выборы приводят к формальным системам, совершенно различным по своему виду и качествам. Этот выбор — предыстория формальной системы, возникающей лишь тогда, когда он уже сделан, Общая теория формальных систем не рассматривает все возможные свойства конкретных систем подобно тому, как теория алгоритмов не учит строить конкретные алгоритмы.
Одной из ее главных целей является цель, в некотором смысле противоположная: выяснить, каков необходимый минимум средств, с помощшо которых можно описать любую формальную систему. Сюда же примыкает вопрос, центральный для любой математической теории: каковы воз- 248 можности объектов, изучаемых в данной теории? Для теории формальных систем он выглядит так: какие множества могут порождаться формальными системами? Опыт изучения теории алгоритмов говорит о том, что такого рода задачи решаются путем выбора конкретных средств, приводящих к конкретным моделям, общность которых показывается затем путем сравнения их с другимт( моделями.
Средства формальных систем — это аксиомы и правила вывода. В абстрактных формальных системах в отличие от логических исчислений не выделяется понятие формулы («осмысленного выражения»); их объекты — произвольные слова в фиксированном алфавите, Итак, формальная система Ю определяется: 1) алфавитом А (множество всех слов в алфавите А, как и в примере 1.5, обозначим А'); 2) разрешимым множеством А,ыА', элементы которого называются аксиомами; 3) конечным множеством вычислимых отношений )?,(ссь ..., а„, р) на множестве А", называемых правилами вывода', слово 6 называется выводимым нз ось ..., сс„по правилу )?о Понятия вывода, выводимости и доказательства — те же, что и для формальных теорий (см. 9 6.1).
Иногда, впрочем, конкретное множество аксиом в системе не фиксируется, а рассматривается выводимость из произвольных разрешимых множеств слов; в этом случае понятия вывода и доказательства не различаются. Конкретные виды формальных систем определяются в основном видом правил вывода, Здесь будут рассмотрены два способа представления формальных систем: системы подстановок и системы продукций Поста.
Однако уже общего определения формальной системы оказывается достаточным, чтобы получить простой, но важный факт. Теорема 6.14. Для любой формальной системы ГБ множество всех доказуемых в ней слов перечислимо. Рассмотрим множество А"* всех конечных последовательностей ссь ..., сс„, где оп — слова в алфавите А. Множество Ае", очевидно, перечислимо. Ввиду разрешимости множества аксиом и вычислимости правил вывода по любой последовательности аь ..., ак можно эффективно узнать, является она выводом в Р5 или нет.
Поэтому если в процессе перечисления А»е выбрасывать все последовательности аь ..., я, не являющиеся выводами, то получим пере- ' Аксиомы также можно задать краником вывода (одноместным отношением): Й;(р) кй — вксиомз», 249 числение множества выводов.
Следовательно, множество последних слов выводов, т. е. слов, выводимых в Р5, перечислимо. П Отметим, что описанная процедура перечисляет выводимые слова, вообще говоря, с повторениями, поскольку одно и то же выводимое слово может иметь много выводов (например, любая последовательность, заканчивающаяся аксиомой, есть вывод этой аксиомы). Верно ли обратное — можно ли для перечислимого множества М построить перечисляющую его формальную систему, т. е. систему, в которой множество выводимых слов совпадает с М? Из предварительных соображений можно ответить утвердительно; представляется, например, правдоподобным, что машину Тьюринга можно представить в виде формальной системы.
Точный ответ на этот вопрос будет дан при рассмотрении конкретных видов формальных систем. Системы подстановок. Система подстановок, или полу- система Туз,— это формальная система, определяемая алфавитом А и конечным множеством подстановок вида ои )3ь где ач )1; — слова, возможно пустые, в А. Подстановка аг-эф интерпретируется как правило вывода Р; следующим образом; у /= 6 по правилу )?ь если слово 6 получается из у путем подстановки слова 6; вместо какого-нибудь вхождения ои в слово у.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
