WikiSort.ru - Программирование

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

См. также

• Автоформализация

Примечания

Литература

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

См. также

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

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

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

Для улучшения этой статьи желательно: Викифицировать статью. Найти и оформить в виде сносок ссылки на независимые авторитетные источники, подтверждающие написанное. Проставив сноски, внести более точные указания на источники.