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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

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

Основные определения[править | править вики-текст]

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

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

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

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

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

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

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

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

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

Определение и разновидности[править | править вики-текст]

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

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

Разновидности дедуктивных теорий[править | править вики-текст]

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

Задание аксиом и правил вывода[править | править вики-текст]

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

Задание только аксиом[править | править вики-текст]

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

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

Примеры[править | править вики-текст]

Геометрия

Задание только правил вывода[править | править вики-текст]

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

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

Свойства дедуктивных теорий[править | править вики-текст]

Непротиворечивость[править | править вики-текст]

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

Полнота[править | править вики-текст]

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

Независимость аксиом[править | править вики-текст]

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

Разрешимость[править | править вики-текст]

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

Важнейшие выводы[править | править вики-текст]

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

Примечания[править | править вики-текст]

  1. Клини С. К. Введение в метаматематику. — М.: ИЛ, 1957. — С. 59-60.
  2. Мендельсон Э. Введение в математическую логику. — М.: «Наука», 1971. — С. 36.

Литература[править | править вики-текст]

См. также[править | править вики-текст]

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