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

неинтерпретированное Исчисление, класс выражений (формул) которого задаётся обычно индуктивно – посредством задания исходных («элементарных», или «атомарных») формул и правил образования (построения) формул, а подкласс доказуемых формул (теорем) – посредством задания системы аксиом (См. Аксиома) и правил вывода (См. Правило вывода) (преобразования) теорем из аксиом и уже доказанных теорем. Термин «Ф. с.» имеет многочисленные синонимы (иногда, впрочем, этими терминами обозначают родственные, но не совпадающие понятия): формальная теория, формальная математика, формализм, формальное исчисление, абстрактное исчисление, синтаксическая система, аксиоматическая система, логистическая система, Формализованный язык, Формальная логика, кодификат, дедуктивная система и др.

formalism

ФОРМА́ЛЬНАЯ СИСТЕ́МА

неинтерпретированное исчисление, класс выражений (формул) к-рого задается обычно индуктивно – посредством задания исходных ("элементарных", или "атомарных") формул и правил образования (построения) формул, а подкласс доказуемых формул (теорем) – посредством задания системы аксиом и правил вывода (преобразования) теорем из аксиом и уже доказанных теорем. Термин "Ф. с." имеет многочисленные синонимы (иногда, впрочем, этими терминами обозначают родственные, но не совпадающие, понятия): формальная теория, формальная математика, формализм, формальное исчисление, абстрактное исчисление, синтаксическая система, аксиоматическая система, логистическая система, формальный язык, формальная логика, кодификат, дедуктивная система и др. См. Исчисление, Логика высказываний, Математическая логика, Натуральное исчисление, Предикатов исчисление, Формализованный язык.

дедуктивная система,- в математич. логике неинтерпретированное исчисление, задаваемое правилами образования выражений этого исчисления и правилами построения выводов в этом исчислении. Выражения Ф. с. рассматриваются как чисто формальные комбинации символов; правила вывода определяют, в каких случаях одно формальное выражение Авыводится из других формальных выражений В ₁,..., В _п. Если п=0. то Аназ. аксиомой. Выводы представляют собой либо последовательности, либо древовидные фигуры, составленные из формальных выражений согласно правилам вывода. Если в вершинах дерева вывода находятся только аксиомы, то формальное выражение, завершающее вывод, наз. выводимым в Ф. с.

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

Понятие Ф. с. - одно из центральных в математич. логике, оно обслуживает нужды как самой математич. логики, так и смежных с ней областей математики.

Наиболее важный класс Ф. с. - формальные теории 1-го порядка (см. [4]), формализующие какую-либо область содержательной математики. Исторически этот класс Ф. с. возник в связи с программой Д. Гильберта (D. Hilbert) обоснования математики (см. Формализм).

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

См. также Формальный математический анализ.

Лит.:[1] Гильберт Д., Основания геометрии, пер. с нем., М.- Л., 1948; [2] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; [3] Чёрч А., Введение в математическую логику, пер. с англ., М., 1960, с. 15-63; [4] Мас Lanе S., лBull. Amer. Math. Soc.

форма́льна систе́ма

форма́льна систе́ма