Введение
Синтаксически правильная логическая формула
В математической логике, в логике высказываний и логике предикатов, правильно построенная формула, сокращенно WFF или wff, часто просто формула, представляет собой конечную последовательность символов из заданного алфавита, являющуюся частью формального языка. Формальный язык может быть отождествлен с множеством формул этого языка. Формула — это синтаксический объект, которому можно придать семантическое значение посредством интерпретации. Два основных применения формул встречаются в логике высказываний и логике предикатов.
Введение
Ключевое применение формул – в логике высказываний и логике предикатов, такой как логика первого порядка. В этих контекстах формула представляет собой последовательность символов φ, для которой осмыслен вопрос: "истинна ли φ?", после того как все свободные переменные в φ будут заменены конкретными значениями. В формальной логике доказательства могут быть представлены последовательностями формул, обладающих определенными свойствами, и последняя формула в последовательности является тем, что и доказывается. Хотя термин "формула" может использоваться для обозначения письменных символов (например, на листе бумаги или доске), более точно понимать его как саму последовательность символов, а символы – как конкретное представление формулы. Различие между нечетким понятием "свойство" и индуктивно определенным понятием "корректная формула" восходит к работе Вейля 1910 года "Uber die Definitionen der mathematischen Grundbegriffe". Таким образом, одна и та же формула может быть записана несколько раз, и формула теоретически может быть настолько длинной, что её невозможно записать в пределах физической вселенной. Сами формулы являются синтаксическими объектами. Им придается смысл посредством интерпретаций. Например, в формуле высказываний каждая переменная может быть интерпретирована как конкретное высказывание, так что вся формула выражает отношение между этими высказываниями. Однако для того, чтобы рассматриваться как формула, формулу необязательно интерпретировать.
Атомные и открытые формулы
Атомная формула — это формула, не содержащая логических связок и кванторов, или, что эквивалентно, формула, не имеющая строгих подформул. Точная форма атомных формул зависит от рассматриваемой формальной системы; например, в пропозициональной логике атомными формулами являются пропозициональные переменные. В логике предикатов атомами являются предикатные символы вместе с их аргументами, каждый из которых является термом. В соответствии с некоторыми определениями, открытая формула образуется путем объединения атомных формул только логическими связками, без использования кванторов. Это не следует путать с незамкнутой формулой.
Закрытые формулы
Закрытая формула, также называемая основной формулой или предложением, — это формула, в которой отсутствуют свободные вхождения каких-либо переменных. Если A — формула языка первого порядка, в которой переменные v1, …, vn имеют свободные вхождения, то A, предваряемое ∀v1…∀vn, является замыканием A.
Свойства, применимые к формулам
Формула А в языке является валидной (действительной), если она истинна для каждой интерпретации. Формула А в языке является выполнимой (удовлетворимой), если она истинна для некоторой интерпретации. Формула А языка арифметики является разрешимой (решаемой), если она представляет собой разрешимое множество, то есть если существует эффективный метод, который, получив подстановку свободных переменных А, определяет, что либо полученный экземпляр А доказуем, либо его отрицание доказуемо.
Использование терминологии
В более ранних работах по математической логике (например, у Черча) под формулами понимали любые последовательности символов, а среди них хорошо сформированные формулы были теми последовательностями, которые соответствовали правилам построения (корректных) формул. Некоторые авторы просто используют термин "формула". Современная практика (особенно в контексте компьютерных наук с использованием математического программного обеспечения, такого как верификаторы моделей, автоматические и интерактивные системы доказательства теорем) склонна сохранять в понятии формулы лишь алгебраический аспект, а вопрос о хорошо сформированности, то есть о конкретном строковом представлении формул (с использованием тех или иных символов для логических связок и кванторов, той или иной конвенции расстановки скобок, польской или инфиксной нотации и т. п.), оставлять как вопрос исключительно обозначений. Хотя выражение "хорошо сформированная формула" всё ещё употребляется, эти авторы не всегда используют его в противопоставлении старому значению формулы, которое больше не является распространённым в математической логике. Выражение "хорошо сформированные формулы" (WFF) также проникло в массовую культуру. WFF является частью эзотерического каламбура, использованного в названии образовательной игры "WFF 'N PROOF: Игра современной логики", разработанной Лейманом Алленом во время учёбы в Йельской юридической школе (впоследствии он был профессором Мичиганского университета). Набор игр предназначен для обучения детей основам символической логики (в польской нотации). Его название – отсылка к слову whiffenpoof, бессмысленному слову, используемому в качестве приветствия в Йельском университете и получившему известность благодаря песне The Whiffenpoof Song и группе The Whiffenpoofs.