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

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

Основные положения

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

При таком задании теорем говорят, что задана .

Примеры

Геометрия

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

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

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

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

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

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

Полнота

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

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

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

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

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

Важнейшие результаты

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

См. также

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

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

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

Примечания

Литература

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