Формальные системы. 
Интеллектуальные системы

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

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

Под аксиоматическим методом понимается такой способ построения научной теории, при котором в основу теории кладутся некоторые исходные положения, называемые аксиомами, а все остальные утверждения теории получаются как логические следствия аксиом. Геометрия является исторически первой и вплоть до XIX в. была единственной аксиоматической теорией. Она дает наиболее наглядный образец формальной системы. Именно геометрия в начале XIX в. дала толчок развитию аксиоматического метода. Н. И. Лобачевский (1926 г.) и Я. Бояи (1929 г.) совершили открытие неевклидовой геометрии. Они установили, что, заменив привычный и, казалось бы, единственно «объективно-истинный» V постулат Евклида о параллельных его отрицанием, можно развивать чисто логическим путем геометрическую теорию, столь же стройную и богатую содержанием, как и геометрия Евклида. Этот факт привлек пристальное внимание математиков XIX в. к дедуктивному (от общего к частному) способу построения математических теорий, что привело к появлению новой проблематики, связанной с формальными системами.

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

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

В работах Г. Фреге (1879 г.), Б. Рассела и А. Н. Уайхеда (1910) ставилась глобальная задача сведения всей математики к логике, т. е. к формальным системам. Д. Гильберт ставил перед собой задачу обоснования всей математики (решение вопроса о ее непротиворечивости) средствами аксиоматических систем. Позднее, благодаря результатам К. Гёделя (1930;е гг.), программа полной формализации (аксиоматизации) математики, предложенная Д. Гильбертом, потерпела крах. К такому итогу привели следующие доказанные Гёделем теоремы.

Первая теорема Гёделя о неполноте. Любая непротиворечивая формальная система, содержащая минимум арифметики (операции сложения и умножения и кванторы V и 3), является неполной и непополнимой.

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

Если к двум теоремам Гёделя о неполноте добавить теорему Г. Генцена, доказанную им позднее (1960;е гг.), о том, что формализованная арифметика непротиворечива, то это позволит сделать два вывода. Во-первых (первая теорема Гёделя о неполноте), арифметику никогда нельзя аксиоматизировать «до конца», т. е. арифметика не полна при любой системе аксиом. Это означает, что при любой системе аксиом арифметики в ней будут содержаться утверждения, которые нельзя ни доказать, ни опровергнуть. Во-вторых (вторая теорема Гёделя о неполноте), непротиворечивость арифметики не может быть доказана средствами самой арифметики. Именно на пути построения мета-мета-…-теории арифметики Г. Генцен нашел доказательство непротиворечивости арифметики.

Завершая общую характеристику понятия «формальная система», отметим, что оно возникло в недрах формальной математической логики как средство изучения аксиоматического метода, впервые использованного в «Началах» Евклида при построении геометрии. Сама логика как наука о правильных рассуждениях, начиная с работ Аристотеля (IV в. до н. э.), зародилась и развивалась в рамках философии. И только в XIX в. с развитием методов формализации и символизации рассуждений появляется математическая логика как отдельный раздел математики, изучающий формальные системы.

Точное определение формальной системы будет дано после рассмотрения основных идей аксиоматического метода на примере геометрии.