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

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

Определение. Формальной системой называется четверка объектов М= < Г, Р, Л, Б>, где:

Т — конечный алфавит (конечное множество символов);

Р — множество синтаксических правил построения формул из символов алфавита;

А — конечное множество аксиом, представляющее собой некоторое подмножество множества формул;

В — конечное множество правил вывода, которые позволяют получать из некоторого конечного множества формул ?/, U₂> …, U_p другое множество формул lV_h W₂,…, W_n формальной системы и записываются в виде

Здесь стрелка -> читается как «влечет» или «следует», формулы t/, t/₂,…, U_p называются посылками, а каждая из формул W_h W₂,…, W_n называется

заключение

м правила вывода.

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

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

Синтаксические правила определяют допустимые в формальной системе последовательности символов алфавита. Образованные в соответствии с синтаксическими правилами последовательности символов называются формулами формальной системы. Тем самым множество синтаксических правил определяет, по существу, грамматику формул. Проводя аналогию с естественным, например русским, языком, будем говорить, что алфавит и грамматика (множество синтаксических правил) формальной системы определяют ее формальный язык. Множество формул в формальной системе является аналогом множества определяемых понятий в геометрии.

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

Правила вывода в формальной системе являются аналогом логических законов, используемых в геометрических рассуждениях. Результатом рассуждений в геометрии являются теоремы. В формальной системе правила вывода используются для проведения доказательств. Формальное доказательство, или просто доказательство, определяется как конечная последовательность формул F, Р_ъ …, /^.формальной системы, такая, что каждая формула либо является аксиомой, либо при помощи одного из правил вывода выводима из предшествующих ей формул F_l9 F₂, F_j9 где j < i. Некоторая формула называется теоремой и обозначается [F, если существует доказательство F_]y F_ly …, F_n в котором она является последней, т. е. F = F. Отсюда ясно, что всякая аксиома является теоремой. Доказательства в формальной системе являются аналогами содержательных рассуждений в геометрии и служат для получения теорем. Отметим, что в следующей записи.

{аксиомы} е {теоремы} с {формулы} с {последовательности символов алфавита}.

все включения множеств являются строгими.

Различают два типа правил вывода:

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

являются продукциями, где.

S (х, у) означает, что «х является сыном для у»,

F (x, у) — «х является отцом для у»,.

GS (х, у) — «х является внуком для у»,.

D (х, у) — «х является дочерью для у»,.

В (х, у) — «х является братом для у».

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

являются правилами переписывания. Здесь обычная стрелка -> заменяется на специальную стрелку |=>. Такое обозначение используется именно в правилах переписывания, для того чтобы отличать их от правил продукций, в которых используется обычная стрелка. Второе из указанных правил переписывания означает: где бы ни встретилась формула tgx внутри другой тригонометрической формулы или как отдельная формула, ее можно заменить дробью , оставляя остальные выражения формулы без изменения. Применение обоих правил переписывания, приведенных выше в качестве примеров, позволяет упростить тригонометрическую формулу cos х ? tg х в два этапа:

На практике формальные системы возникают из потребности представления знаний и рассуждений конкретных содержательных научных теорий. В этом случае формальные системы служат средством для более углубленного изучения математическими методами соответствующей научной теории. Однако вполне возможно определение формальной системы чисто абстрактно, безотносительно к некоторой содержательной теории. И только потом, когда формальная система определена и достаточно изучена, для нее может быть найдена подходящая содержательная интерпретация. Конкретная формальная система является тем более интересной, чем больше существует для нее различных интерпретаций в виде содержательных научных теорий. В таком случае наличие даже какого-то одного формального доказательства уже обеспечивает получение различных конкретных результатов во множестве содержательных научных теорий. В современной математике большой интерес вызывают формальные системы самого общего характера, которые исследуются в теории категорий и теории моделей.

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

Пример. Формальная система (JP).

• 1. Алфавит {а, Ь, ?}.
• 2. Формулы — это символ или какая-либо последовательность символов алфавита.
• 3. Одна аксиома: а? а
• 4. Одно правило вывода: с,? с₂ -> Ьс_х? Ьс₂

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

Из определения данной формальной системы непосредственно вытекает, что ее теоремами являются только следующие формулы:

Очевидно, что, например, формула baab? abba не является теоремой.

Когда формальная система М= определена, т. е. заданы алфавит Г, грамматика Р, аксиомы А и правила вывода В, представляется естественным ответить на следующие вопросы относительно системы М:

• 1. Есть ли аксиомы в А, которые могут быть выведены из остальных аксиом?
• 2. Есть ли противоречия в системе Л/, т. е. имеется ли формула У⁷, что формула У⁷ и ее отрицание -.У⁷обе доказуемы в Ml
• 3. Верно ли, что для любой формулы У⁷системы М доказуемой является либо сама формула У⁷, либо ее отрицание -.У⁷?
• 4. Существует ли такая процедура, которая для каждой формулы деисте — мы М позволяет установить за конечное число шагов, является ли она теоремой или нет?
• 5. Существует ли такая интерпретация формальной системы А/, что все ее теоремы становятся истинными утверждениями в этой интерпретации?

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

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

В зависимости от того, каким будет ответ на третий вопрос, говорят о полной или неполной формальной системе (теории). Если в системе любая формула либо сама система является доказуемой, либо доказуемо ее отрицание, то такая формальная система называется полной, иначе она называется неполной. В полной теории все формулы можно разбить на два непустых и непересекающихся класса: теоремы и не-теоремы (для них не существует доказательства). В неполной теории либо может встретиться формула, что она сама и ее отрицание недоказуемы, либо может встретиться формула, что она сама и ее отрицание доказуемы. Последнее означает противоречивость соответствующей формальной теории. Ценность полной теории заключается в том, что такая ситуация «неопределенности» — недоказуемости формулы и ее отрицания — ни для одной формулы не возникает.

Со свойством полноты теории тесно связано свойство разрешимости теории. Если для формальной теории существует процедура, позволяющая для любой формулы за конечное число шагов решить, является ли она теоремой или не-теоремой, то теория называется разрешимой, а сама такая процедура называется процедурой решения. При ответе на четвертый вопрос основная трудность заключается в отыскании процедуры решения. Такая процедура существует далеко не всегда, даже для таких простых и фундаментальных теорий, какой является исчисление предикатов первого порядка. Примером разрешимой формальной теории может служить система (JP). Для нее процедура решения может быть такой:

• 1) просматриваются слева направо символы анализируемой формулы и ведется подсчет символов Ь до символа а
• 2) затем сразу за символом а должен следовать символ ?:
• 3) после него должны следовать символы b в том же количестве, что и в начале формулы;
• 4) за ними должен следовать один символ а, после которого формула заканчивается.

Если эти четыре условия выполнены, то анализируемая формула теории является теоремой. В противном случае она является не-теоремой.

Наконец, в пятом вопросе выясняется, можно ли формальной теории придать такой содержательный смысл, чтобы ее теоремы соответствовали истинным утверждениям. Иначе говоря, имеется ли модель формальной теории. По существу содержательная модель представляет собой обычную выраженную естественным русским языком научную теорию в привычном понимании этого слова: со своими объектами исследования, методами и специфическими понятиями и идеями. Не следует, правда, считать, что моделью обязательно должна быть какая-нибудь известная содержательная научная теория. Роль модели одной формальной теории вполне может выполнять другая формальная теория или ее часть. Если утвердительно ответить на пятый вопрос, то это будет означать, что соответствующей формальной теории М сопоставляется некая другая (возможно также формальная) теория А/', в которой имеет смысл говорить об истинности и ложности ее утверждений. В этом случае теорию М', какая бы она ни была, формальная или содержательная, называют моделью теории М. Так, обычная арифметика, известная из школьного курса, служит моделью для формальной арифметики. Другой интересный пример модели будет рассмотрен ниже. Он относится к содержательной интерпретации неевклидовой геометрии средствами евклидовой геометрии.