Правильно построенная формула

Правильно построенная формула (англ. well-formed formula, WFF) — в математической логике и формальных грамматиках — последовательность символов формального языка, которая соответствует синтаксическим правилам этого языка и может быть интерпретирована как осмысленное выражение. Правильно построенная формула противопоставляется бессмысленным наборам символов, которые не подчиняются правилам построения (например, «P ∧ ∧ Q» в логике высказываний). Понятие WFF является фундаментальным для формальных систем, аксиоматических теорий и языков программирования.

Определение и общие принципы

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

В отличие от естественных языков, где грамматическая правильность часто допускает неоднозначность, в формальных языках WFF должна быть однозначно интерпретируема. Например, в арифметике выражение «2 + 3 × 4» может быть прочитано по-разному, если не заданы приоритеты операций; в формальной записи с явными скобками — «(2 + 3) × 4» или «2 + (3 × 4)» — каждая из формул является WFF, но они различны.

Правильно построенные формулы в логике высказываний

Алфавит

Алфавит языка логики высказываний обычно включает:

• пропозициональные переменные: \( p, q, r, \dots \) (или с индексами);
• логические связки: \(\neg\) (отрицание), \(\land\) (конъюнкция), \(\lor\) (дизъюнкция), \(\rightarrow\) (импликация), \(\leftrightarrow\) (эквиваленция);
• вспомогательные символы: левая и правая скобки.

Правила образования

Правильно построенные формулы определяются индуктивно:

1. Базис: всякая пропозициональная переменная является WFF.
2. Индуктивный шаг:

• если \(\varphi\) — WFF, то \(\neg \varphi\) — WFF;
• если \(\varphi\) и \(\psi\) — WFF, то \((\varphi \land \psi)\), \((\varphi \lor \psi)\), \((\varphi \rightarrow \psi)\), \((\varphi \leftrightarrow \psi)\) — WFF.

1. Замыкание: других WFF, кроме полученных по пунктам 1 и 2, нет.

Таким образом, последовательность «\(p \land q\)» не является WFF, так как скобки обязательны. Правильной записью будет «\((p \land q)\)». В некоторых изложениях допускается опускание внешних скобок, но внутренняя структура остаётся строгой.

Примеры и контрпримеры

• WFF: \(p\), \(\neg p\), \((p \land q)\), \((\neg p \rightarrow (q \lor r))\).
• Не WFF: \(p \land\), \(\land q\), \((p \rightarrow )\), \(p q\).

Правильно построенные формулы в логике предикатов

Расширение алфавита

В логике предикатов (исчислении предикатов первого порядка) алфавит дополняется:

• предметными переменными: \(x, y, z, \dots\);
• предметными константами: \(a, b, c, \dots\);
• функциональными символами: \(f, g, h, \dots\) (каждый с заданной арностью);
• предикатными символами: \(P, Q, R, \dots\) (с арностью);
• кванторами: \(\forall\) (квантор всеобщности), \(\exists\) (квантор существования).

Термы

Сначала определяются термы — выражения, обозначающие объекты:

1. Базис: переменные и константы — термы.
2. Индуктивный шаг: если \(t_1, \dots, t_n\) — термы, а \(f\) — n-арный функциональный символ, то \(f(t_1, \dots, t_n)\) — терм.

Атомарные формулы

Атомарная формула — это предикатный символ, применённый к термам: \(P(t_1, \dots, t_n)\). Атомарные формулы являются WFF.

Правила образования для формул

1. Базис: атомарные формулы — WFF.
2. Индуктивный шаг:

• если \(\varphi\) — WFF, то \(\neg \varphi\) — WFF;
• если \(\varphi\) и \(\psi\) — WFF, то \((\varphi \land \psi)\), \((\varphi \lor \psi)\), \((\varphi \rightarrow \psi)\), \((\varphi \leftrightarrow \psi)\) — WFF;
• если \(\varphi\) — WFF и \(x\) — переменная, то \(\forall x \varphi\) и \(\exists x \varphi\) — WFF.

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

Примеры

• WFF: \(\forall x P(x)\), \(\exists y (Q(y) \land R(y))\), \(\neg \forall x (P(x) \rightarrow Q(f(x)))\).
• Не WFF: \(\forall P(x)\) (квантор применён не к переменной), \(P(\forall x)\) (предикат применён к квантору), \((x \land y)\) (переменные не соединены логической связкой).

Правильно построенные формулы в формальных грамматиках

В теории формальных языков понятие WFF обобщается до понятия выводимой цепочки в контекстно-свободной грамматике. Например, в арифметических выражениях:

• Терминалы: цифры, знаки операций, скобки.
• Нетерминалы: <выражение>, <терм>, <множитель>.
• Продукции:
• <выражение> → <выражение> + <терм> | <терм>
• <терм> → <терм> * <множитель> | <множитель>
• <множитель> → ( <выражение> ) | число

Цепочка «(2 + 3) 5» является WFF (выводится из <выражение>), а «2 + 3» — нет.

Значение и применение

В математической логике

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

В информатике

• Языки программирования: компиляторы и интерпретаторы проверяют, является ли исходный код синтаксически правильным (то есть WFF для данной грамматики языка). Ошибки синтаксиса — это нарушение правил образования.
• Базы данных: в языках запросов (SQL, SPARQL) правильно построенные запросы — это те, которые соответствуют грамматике языка.
• Искусственный интеллект: в системах логического вывода (например, Prolog) программа состоит из WFF (хорновских дизъюнктов).

В лингвистике

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

Критика и ограничения

Понятие WFF является чисто синтаксическим. Оно не гарантирует ни истинности, ни осмысленности формулы. Например, в логике предикатов формула \(\forall x (P(x) \land \neg P(x))\) является WFF, но она логически противоречива (ложна во всех интерпретациях). В программировании синтаксически правильная программа может содержать логические ошибки (например, бесконечный цикл).

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

См. также

• Формальная грамматика
• Синтаксис (логика)
• Терм
• Атомарная формула
• Теория формальных языков

Источники

• Мендельсон Э. Введение в математическую логику. — М.: Наука, 1976.
• Чёрч А. Введение в математическую логику. — М.: ИЛ, 1960.
• Хопкрофт Дж., Мотвани Р., Ульман Дж. Введение в теорию автоматов, языков и вычислений. — М.: Вильямс, 2002.
• Клини С. К. Математическая логика. — М.: Мир, 1973.