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

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

Определение и основные компоненты

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

• Алфавит — конечное множество символов (например, буквы, цифры, логические операторы).
• Грамматика — набор правил, определяющих, какие последовательности символов являются правильно построенными формулами (ППФ).
• Аксиомы — конечное или рекурсивно перечислимое множество ППФ, принимаемых за истинные без доказательства.
• Правила вывода — конечное множество правил, позволяющих из одних ППФ получать новые (например, modus ponens).

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

История развития

Понятие формальной системы восходит к работам древнегреческих философов, в частности Аристотеля, который впервые систематизировал силлогистику. Однако современное понимание сформировалось в конце XIX — начале XX века.

Предпосылки

В конце XIX века математики столкнулись с кризисом оснований математики, вызванным парадоксами (например, парадокс Рассела в наивной теории множеств). В ответ на это возникла программа гильбертианства (формализма), предложенная Давидом Гильбертом. Она предполагала, что вся математика может быть представлена в виде непротиворечивой формальной системы, в которой все истинные утверждения доказуемы.

Ключевые вехи

• 1879 год — Готлоб Фреге в «Исчислении понятий» впервые построил полноценную формальную систему для логики первого порядка.
• 1931 год — Курт Гёдель опубликовал теоремы о неполноте, показав, что для достаточно выразительных формальных систем (включающих арифметику) невозможно одновременно доказать их непротиворечивость и полноту внутри самой системы.
• 1936 год — Алонзо Чёрч и Алан Тьюринг доказали неразрешимость проблемы выводимости в логике первого порядка, установив фундаментальные ограничения формальных методов.
• 1930-е годы — Развитие теории алгоритмов (машина Тьюринга, рекурсивные функции) позволило формализовать понятие вычислимости, тесно связанное с формальными системами.

Классификация формальных систем

Формальные системы классифицируются по нескольким признакам.

По типу логики

• Логические системы — основаны на классической логике (логика высказываний, логика первого порядка, логика высших порядков). В них аксиомы и правила вывода задают логические истины.
• Теории — формальные системы, расширяющие логику специфическими аксиомами, описывающими конкретную предметную область (например, формальная арифметика Пеано, теория множеств Цермело — Френкеля).

По свойствам

• Непротиворечивость — система непротиворечива, если в ней нельзя вывести одновременно формулу и её отрицание.
• Полнота — система полна, если для любой правильно построенной формулы либо она сама, либо её отрицание является теоремой.
• Разрешимость — существует алгоритм, который для любой формулы определяет, является ли она теоремой.

По способу задания

• Аксиоматические — явно перечислены аксиомы и правила вывода.
• Генеративные — теоремы порождаются грамматикой и правилами, часто без явного выделения аксиом (например, формальные грамматики Хомского).

Устройство и формальное описание

Формальная система обычно задаётся четвёркой: ⟨A, F, Ax, R⟩, где:

• A — алфавит.
• F — множество ППФ (задаётся грамматикой).
• Ax — подмножество F, аксиомы.
• R — конечное множество правил вывода, каждое из которых является отношением на F^n × F.

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

Пример: исчисление высказываний

Простейшая формальная система — исчисление высказываний. Алфавит включает пропозициональные переменные (p, q, r…), логические связки (¬, ∧, ∨, →) и скобки. Аксиомы — три схемы (например, p → (q → p)). Правило вывода — modus ponens: из p и p → q выводится q. Теоремами являются все тавтологии классической логики.

Применение

Формальные системы находят применение в различных областях.

Математика и логика

• Доказательство теорем — формальные системы служат основой для автоматического доказательства теорем (например, в системах Coq, Isabelle, Lean).
• Основания математики — теория множеств ZFC является формальной системой, в которой может быть выражена практически вся современная математика.

Информатика

• Языки программирования — формальные грамматики (контекстно-свободные грамматики) используются для описания синтаксиса языков.
• Верификация программ — формальные системы (например, логика Хоара, темпоральная логика) применяются для доказательства корректности программного обеспечения.
• Искусственный интеллект — системы логического вывода (экспертные системы, дедуктивные базы данных) основаны на формальных правилах.

Лингвистика

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

Философия

• Аналитическая философия — формальные системы применяются для анализа структуры аргументов, разрешения парадоксов и моделирования рассуждений.
• Эпистемология — формальные системы используются для формализации знания и веры (логика знания).

Ограничения и критика

Формальные системы имеют фундаментальные ограничения, установленные метаматематикой.

Теоремы Гёделя о неполноте

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

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

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

Критика формализма

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

Интересные факты

• Понятие формальной системы лежит в основе «тезиса Чёрча — Тьюринга», согласно которому любая вычислимая функция может быть реализована на машине Тьюринга.
• В 1930-е годы в СССР активно развивалась конструктивная математика (А. А. Марков, П. С. Новиков), которая предлагала альтернативный подход к формализации, основанный на алгоритмических конструкциях.
• Известный парадокс «Лжец» («Это утверждение ложно») может быть формализован в некоторых формальных системах, приводя к противоречиям, что ограничивает их выразительность.

Источники

• Гильберт Д., Аккерман В. «Основы теоретической логики». — М.: Иностранная литература, 1947.
• Гёдель К. «О формально неразрешимых предложениях Principia Mathematica и родственных систем» // Сборник «Математическая логика и основания математики». — М.: Наука, 1970.
• Мендельсон Э. «Введение в математическую логику». — М.: Наука, 1976.
• Шенфилд Дж. «Математическая логика». — М.: Мир, 1975.
• Тьюринг А. «О вычислимых числах с приложением к проблеме разрешимости» // Сборник «Математическая логика и теория алгоритмов». — М.: Наука, 1983.