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

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

Формальная система — это совокупность абстрактных объектов, не связанных с внешним миром, в котором представлены правила оперирования множеством символов в строго синтаксической трактовке без учета смыслового содержания, то есть семантики. Строго описанные формальные системы появились после того, как была поставлена задача Гильберта. Первые ФС появились после выхода книг Рассела и Уайтхеда «Формальные системы». Этим ФС были предъявлены определенные требования.

Основные определения

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

1. Задано конечное или счётное множество произвольных символов. Конечные последовательности символов называются выражениями теории.
2. Имеется подмножество выражений, называемых формулами.
3. Выделено подмножество формул, называемых аксиомами.
4. Имеется конечное множество отношений между формулами, называемых правилами вывода.

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

Чаще всего имеется возможность эффективно выяснять, является ли данная формула аксиомой; в таком случае теория называется эффективно аксиоматизированной или аксиоматической. Множество аксиом может быть конечным или бесконечным. Если множество аксиом бесконечно, то, как правило, оно задаётся с помощью конечного числа схем аксиом и правил порождения конкретных аксиом из схемы аксиом. Обычно аксиомы делятся на два вида: логические аксиомы (общие для целого класса формальных теорий) и нелогические или собственные аксиомы (определяющие специфику и содержание конкретной теории).

Для каждого правила вывода R и для каждой формулы A эффективно решается вопрос о том, находится ли выбранный набор формул в отношенни R с формулой A, и если да, то A называется непосредственным следствием данных формул по правилу R.

Выводом называется всякая последовательность формул такая, что всякая формула последовательности есть либо аксиома, либо непосредственное следствие каких-либо предыдущих формул по одному из правил вывода.

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

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

Теория, в которой не все формулы являются теоремами, называется абсолютно непротиворечивой.

Определение и разновидности

Дедуктивная теория считается заданной, если:

1. Задан алфавит (множество) и правила образования выражений (слов) в этом алфавите.
2. Заданы правила образования формул (правильно построенных, корректных выражений).
3. Из множества формул некоторым способом выделено подмножество T теорем (доказуемых формул).

Разновидности дедуктивных теорий

В зависимости от способа построения множества теорем:

Задание аксиом и правил вывода

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

Задание только аксиом

Задаются только аксиомы, правила вывода считаются общеизвестными.

При таком задании теорем говорят, что задана полуформальная аксиоматическая теория.

Примеры

Геометрия

Задание только правил вывода

Аксиом нет (множество аксиом пусто), задаются только правила вывода.

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

Свойства дедуктивных теорий

Непротиворечивость

Теория, в которой множество теорем покрывает всё множество формул (все формулы являются теоремами, «истинными высказываниями»), называется противоречивой. В противном случае теория называется непротиворечивой. Выяснение противоречивости теории — одна из важнейших и иногда сложнейших задач формальной логики. После выяснения противоречивости теория, как правило, не имеет дальнейшего ни теоретического, ни практического применения.

Полнота

Теория называется полной, если в ней для любой формулы $F$ выводима либо сама $F$, либо ее отрицание $\neg F$. В противном случае, теория содержит недоказуемые утверждения (утверждения, которые нельзя ни доказать, ни опровергнуть средствами самой теории), и называется неполной.

Независимость аксиом

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

Разрешимость

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

Важнейшие выводы

• В 30-е гг. XX века Курт Гёдель показал, что есть целый класс теорий первого порядка, являющихся неполными. Более того, формула, утверждающая непротиворечивость теории, также невыводима средствами самой теории (см. Теоремы Гёделя о неполноте). Этот вывод имел огромное значение для математики, так как формальная арифметика (а на ней базируется теория действительных чисел, без которой нельзя представить современную математику) является как раз такой теорией первого порядка, а следовательно, формальная арифметика и все теории, содержащие ее, в том числе теория действительных чисел, являются неполными.
• Проблема неразрешимости логики предикатов. Чёрчем доказано, что не существует алгоритма, который для любой формулы логики предикатов устанавливает, логически общезначима формула или нет.
• Исчисление высказываний является непротиворечивой, полной, разрешимой теорией, причем все три утверждения доказуемы в рамках самой логики высказываний.

Литература

• Галиев Ш. И. Математическая логика и теория алгоритмов. — Казань: Издательство КГТУ им. А. Н. Туполева. 2002.
• Клини С. К. Введение в метаматематику. — М.: ИЛ, 1957. — 526 с.
• Клини С. К. Математическая логика. — М.: «Мир», 1973. — 480 с.
• Мендельсон Э. Введение в математическую логику. — М.: «Наука», 1971. — 320 с.
• Новиков Ф. А. Дискретная математика для программистов. — СПб.: Питер, 2000. — 304 с.: ил. ISBN 5-272-00183-4.
• Яновская С. А. Из истории аксиоматики // Историко-математические исследования. — М.: ГИТТЛ, 1958. — № 11. — С. 63-96.

См. также

• Теория множеств
• Формальная логика
• Формализм (математика)
• Система кодирования

Примеры формальных теорий

• Теории первого порядка
  • Исчисление высказываний
  • Исчисление предикатов первого порядка
  • Формальная арифметика
  • Аксиоматическая теория множеств
  • Теория групп
• Теории высших порядков
• Лямбда-исчисление
  • Лямбда-исчисление с типами
  • Исчисление конструкций
  • Исчисление индуктивных конструкций