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

Дедуктивная система,- в математич. логике неинтерпретированное исчисление, задаваемое правилами образования выражений этого исчисления и правилами построения выводов в этом исчислении. Выражения Ф. с. рассматриваются как чисто формальные комбинации символов; правила вывода определяют, в каких случаях одно формальное выражение Авыводится из других формальных выражений В 1, . . ., В п. Если п=0. то Аназ. аксиомой. Выводы представляют собой либо последовательности, либо древовидные фигуры, составленные из формальных выражений согласно правилам вывода. Если в вершинах дерева вывода находятся только аксиомы, то формальное выражение, завершающее вывод, наз. выводимым в Ф. с. Наиболее интересны Ф. с., удовлетворяющие требованиям эффективности языка н понятия вывода. Это означает, что должна иметься эффективная процедура для распознавания того, является ли произвольная последовательность символов выражением Ф. с. или нет. Такому же требованию должно удовлетворять понятие вывода. Понятие выводимого выражения в эффективных Ф. с., вообще говоря, не является эффективным. Понятие Ф. с. — одно из центральных в математич. логике, оно обслуживает нужды как самой математич. логики, так и смежных с ней областей математики. Наиболее важный класс Ф. с. — формальные теории 1-го порядка (см. [4]), формализующие какую-либо область содержательной математики. Исторически этот класс Ф. с. возник в связи с программой Д. Гильберта (D. Hilbert) обоснования математики (см. Формализм). Понятия и методы, выработанные математич. логикой при изучении Ф. с., нашли применения в различных областях математики, напр. в теории групп и теории категорий. Ценность понятия Ф. с. определяется плодотворностью способа исследования, основанного на идеях, связанных с этим понятием. См. также Формальный математический анализ. Лит.:[1] Гильберт Д., Основания геометрии, пер. с нем., М.- Л., 1948; [2] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; [3] Чёрч А., Введение в математическую логику, пер. с англ., М., 1960, с. 15-63; [4] Мас Lanе S., лBull. Amer. Math. Soc.