В математической логике, логике высказываний и логика предикатов, правильно сформированная формула, сокращенно WFF или wff, часто просто формула, является конечной последовательностью из символов из заданного алфавита, который является частью формального языка. Формальный язык можно отождествить с набором формул в языке.
Формула - это синтаксический объект, которому можно дать семантическое значение посредством интерпретации. Два ключевых использования формул - в логике высказываний и логике предикатов.
Ключевое использование формул находится в логике высказываний и логика предиката, например логика первого порядка. В этих контекстах формула представляет собой строку символов φ, для которой имеет смысл спросить «истинно ли φ?» После того, как были созданы любые свободные переменные в φ. В формальной логике доказательства могут быть представлены последовательностями формул с определенными свойствами, и последняя формула в последовательности - это то, что доказано.
Хотя термин «формула» может использоваться для письменных отметок (например, на листе бумаги или классной доске), более точно он понимается как последовательность выражаемых символов, при этом отметки представляют собой токен экземпляр формулы. Таким образом, одна и та же формула может быть записана более одного раза, и в принципе формула может быть настолько длинной, что ее вообще нельзя записать в пределах физической вселенной.
Сами формулы являются синтаксическими объектами. Им придают значения интерпретации. Например, в формуле высказываний каждая пропозициональная переменная может интерпретироваться как конкретное высказывание, так что общая формула выражает взаимосвязь между этими высказываниями. Однако формулу не нужно интерпретировать, чтобы рассматривать ее исключительно как формулу.
Формулы исчисления высказываний, также называемые формулами высказываний, представляют собой такие выражения, как . Их определение начинается с произвольного выбора набора V пропозициональных переменных. Алфавит состоит из букв в V, а также символов для пропозициональных связок и круглых скобок «(» и «)», которые, как предполагается, не входят в V. Формулы будут определенными выражениями ( то есть строки символов) над этим алфавитом.
Формулы индуктивно определяются следующим образом:
Это определение также может быть записано в виде формальной грамматики в форме Бэкуса – Наура при условии, что набор переменных конечен:
:: = p | q | г | с | т | u |... (произвольный конечный набор пропозициональных переменных)
Используя эту грамматику, последовательность символов
является формулой, поскольку она грамматически правильна Последовательность символов
не является формулой, потому что она не соответствует грамматике.
Сложные формулы могут быть трудночитаемыми из-за, например, большого количества скобок. Чтобы смягчить это последнее явление, для операторов применяются правила приоритета (аналогичные стандартному математическому порядку операций ), что делает некоторые операторы более обязательными, чем другие. Например, если принять приоритет (от наиболее обязательного до наименее связующего) 1. ¬ 2. → 3. ∧ 4. ∨. Тогда формулу
можно сократить как
Однако это всего лишь соглашение, используемое для упрощения письменного представления формулы. Если бы приоритет предполагался, например, ассоциативным слева и справа, в следующем порядке: 1. ¬ 2. ∧ 3. ∨ 4. →, то та же самая формула выше (без скобок) была бы переписана как
Определение формулы в логике первого порядка относится к сигнатуре рассматриваемой теории. Эта сигнатура определяет постоянные символы, символы предикатов и функциональные символы рассматриваемой теории, а также арности функциональных и предикатных символов.
Определение формулы состоит из нескольких частей. Во-первых, набор термов определяется рекурсивно. Неформально термины - это выражения, которые представляют объекты из области дискурса .
Следующим шагом является определение атомарных формул.
Наконец, набор формул определяется как наименьший набор содержащий набор атомарных формул, таких что выполняется следующее:
Если в формуле нет вхождений или для любой переменной , тогда это называется бескванторным. Формула существования - это формула, начинающаяся с последовательности количественной оценки существования, за которой следует бескванторная формула.
Атомарная формула - это формула, не содержащая логических связок и квантификаторов, или, что эквивалентно, формула, не имеющая строгих подформулы. Точная форма атомарных формул зависит от рассматриваемой формальной системы; для логики высказываний, например, атомарные формулы являются пропозициональными переменными. Для логики предикатов атомы представляют собой символы предиката вместе со своими аргументами, каждый аргумент представляет собой термин .
Согласно некоторой терминологии, открытая формула формируется путем объединения атомарных формул с использованием только логических связок, за исключением кванторов. Это не следует путать с формулой, которая не закрыта.
Замкнутые формулы, также основная формула или предложение, - это формула, в которой нет свободных вхождений любого переменная. Если A - это формула языка первого порядка, в которой переменные v 1,..., v n встречаются бесплатно, то A, которому предшествует v1... vn, является закрытием A.
В более ранних работах по математической логике (например, автор Черч ), формулы относятся к любым строкам символов, и среди этих строк хорошо сформированные формулы - это строки, которые соответствуют правилам формирования (правильных) формул.
Некоторые авторы просто говорят формулу. Современное использование (особенно в контексте информатики с математическим программным обеспечением, таким как средства проверки моделей, автоматические средства доказательства теорем, интерактивные средства доказательства теорем ), как правило, сохраняют это понятие формул - только алгебраическое понятие и оставить вопрос о корректности, т.е. о конкретном строковом представлении формул (с использованием того или иного символа для связок и кванторов, с использованием того или иного соглашения о скобках с использованием польской или инфиксной нотации и т. Д.) Как простую проблему с нотацией.
Хотя выражение «правильно сформированная формула» все еще используется, эти авторы не обязательно используют его в отличие от старого смысла формулы, который больше не используется в математической логике.
Выражение «правильно сформированные формулы» (WFF) также вошло в массовую культуру. WFF является частью эзотерического каламбура, использованного в названии академической игры «WFF 'N PROOF : Игра современной логики», разработанной обывателем Алленом, когда он учился в Йельской школе права (позже он был профессором Мичиганского университета ). Набор игр предназначен для обучения детей принципам символической логики (в польской нотации ). Его название является отголоском whiffenpoof, бессмысленного слова, использованного в качестве приветствия в Йельском университете, ставшего популярным в The Whiffenpoof Song и The Whiffenpoofs.