3.2. Определение формальной системы

Формальная система представляет собой совокупность чисто абстрактных объектов (не связанных с внешним миром), в которой представлены правила оперирования множеством символов в чисто синтаксической трактовке без учета смыслового содержания (или семантики).

Формальная система определена, если:

1. Задан конечный алфавит (конечное множество символов).

2. Определена процедура построения формул (или слов) формальной системы.

3. Выделено некоторое множество формул, называемых аксиомами.

4. Задано конечное множество правил вывода, которые позволяют получать из некоторого конечного множества формул другое множество формул. Эти правила могут быть представлены в виде

где — формулы формальной системы, а стрелка читается как “влечет” или “следует”.

3.2.1. Дополнительные определения

Формальную систему иногда называют также аксиоматикой, или формальной теорией, или еще проще — множеством формул.

Алфавит, который заранее предполагается конечным, иногда называют словарем. При этом в нем различаются констаиты, переменные и операторы (примеры в разд. 3.2.3).

Способ построения формул (п. 2 определения формальной системы) определяет конкретную синтаксическую конструкцию

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

Формальное доказательство (или просто доказательство) определяется как конечная последовательность формул такая, что каждая формула либо является аксиомой, либо при помощи одного из правил вывода выводима из предшествующих ей формул где

Формула называется теоремой, если существует доказательство, в котором она является последней, т. е. . В частности, всякая аксиома является теоремой. Если есть теорема, то этот факт кратко обозначается так:

Правила вывода определения формальной системы) называют, также правилами словообразования или правилами вывода заключения. В принципе они позволяют определять, является ли данная формула теоремой данной формальной системы. Отметим также, что в соотношении

Различают два типа правил вывода: 1) правила, применяемые к формулам, рассматриваемым как единое целое (в этом случае их называют продукциями, правилами продукций или продукционными правилами), 2) правила, которые могут применяться к любой отдельной части формулы, причем сами эти части являются формулами, входящими в формальную систему. В этом случае говорят о правилах переписывания. Так, в обычной математике следующее правило вывода:

применяется к формуле как к целому (в данном случае к предложению математического анализа) — это продукция (с двумя антецедентами, или посылками). Слово “влечет" для краткости при использовании продукции часто заменяется стрелкой В отличие от предыдущего правило имеет смысл при любом виде входящего в него в качестве подвыражения х. Оно является правилом переписывания, и в этом случае для обозначения слова “влечет” используется специальная стрелка

Разумеется, и продукция, и правило переписывания имеют только одно направление вывода — слева направо. Правило переписывания действует в обоих направлениях, если только заданы два правила: и Иначе при использовании одностороннего правила переписывания как двустороннего

в рассуждениях может получиться порочный круг (что часто случается с детьми).

Замечание. Множества, указанные в пп. 3 и 4 определения формальной системы, не обязательно должны быть конечными: достаточно, чтобы они были рекурсивно перечислимы. Однако в последующем изложении мы будем предполагать, что они являются конечными.

3.2.2. Правило подстановки

Правило подстановки пригодно для использования в любой формальной системе. Чтобы применить правило вывода к какой-нибудь формуле М, принадлежащей к некоторой формальной системе, надо совместить Левый элемент правила Q с М. Это осуществляется при помощи подстановок в Q и/или в М. Подстановка заключается в замещении всех вхождений какой-либо переменной на формулу из формальной системы, которая не содержит этой переменной.

3.2.3. Примеры формальных систем

Пример 1. Формальная система

1. Алфавит

2. Формулы: символ или какая-либо последовательность символов а или или .

3. Одна аксиома: .

4. Одно правило вывода:

Принято, что в этом правиле вывода символы означают какие-то последовательности символов а или формальной системы и могут быть замещены любыми последовательностями символов а или

Символы не являются символами формальной системы Они служат только посредниками для формализации правил вывода. Учитывая способ образования формул незамещаемые символы называют константами, а незамещаемый символ — оператором.

Из определения данной формальной системы непосредственно вытекает следующий способ получения допустимых формул, т. е. формул, выводимых согласно правилу определения данной формальной системы: достаточно рассмотреть лишь все комбинации, получаемые при последовательном применении правила 4 к аксиоме 3 нашего примера. В результате мы имеем

Очевидно, что, например, выражение не могло бы быть допустимой формулой в данной формальной сйбтеме. Мы еще вернемся к рассмотрению этой системы в разд. 3.5.

Пример 2. Формальная система

Хофштедтер в своей объемистой книге Эшер, Бах — золотой венок вечности” прослеживает проявление идеи рекурсии и автоморфизма в логике, теоремах Геделя, информатике, странных рисунках Эшера, фугах, канонах и экспромтах Баха. Приводимая ниже формальная система взята из первой главы этой книги:

1. Алфавит:

2. Формулы: любая последовательность символов данного алфавита.

3. Одна аксиома:

4. Правила вывода:

правило (продукция);

правило (продукция);

правило (правило переписывания);

правило (правило переписывания).

То, что правило 1 является продукцией, означает в данном случае, что оно применяется только, если последняя буква теоремы есть . В этом случае, например, из теоремы выводится теорема Отметим, что символ не принадлежит символам данной формальной системы, а просто играет роль некоего слова.

Правило 2 позволяет из теоремы вывести теорему при условии, что является теоремой. Правило 3 позволяет, например, сделать переход от теоремы к теореме Последнее правило 4 указывает, что всякая цепочка из двух рядом стоящих символов может быть просто удалена из теоремы. Например, теорема равнозначна теореме Ниже приводятся примеры использования правил вывода данной формальной системы:

(аксиома);

б) (правило 2 применено к а);

в) (правило 2 применено к б);

г) (правило 1 применено к в);

д) (правило 3 применено к г);

е) (правило 4 применено к д).

Читателю предлагается; используя правила вывода дайной формальной системы, решить задачу, предложенную Д. Хофштедтером: получить теорему из исходной аксиомы данной формальной системы.