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

Синтаксически правильная логическая формула

В математической логике , пропозициональной логике и логике предикатов правильно сформированная формула , сокращенно WFF или wff , часто просто формула , представляет собой конечную последовательность символов из заданного алфавита , которая является частью формального языка . ^[1]

Аббревиатура wff произносится как «вуф» или иногда «вифф», «вефф» или «уифф». ^[12]

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

Введение

Формулы используются в основном в пропозициональной логике и логике предикатов, например, в логике первого порядка . В этих контекстах формула — это строка символов φ, для которой имеет смысл спросить «истинно ли φ?», как только будут инстанциированы все свободные переменные в φ. В формальной логике доказательства могут быть представлены последовательностями формул с определенными свойствами, а последняя формула в последовательности — это то, что доказывается.

Хотя термин «формула» может использоваться для письменных знаков (например, на листе бумаги или доске), точнее его понимать как последовательность символов, которые выражаются, причем знаки являются условным экземпляром формулы. Это различие между неопределенным понятием «свойства» и индуктивно определенным понятием правильно сформированной формулы имеет корни в статье Вейля 1910 года «Uber die Definitionen der mathematischen Grundbegriffe». ^[13] Таким образом, одна и та же формула может быть записана более одного раза, и формула в принципе может быть настолько длинной, что ее вообще невозможно записать в пределах физической вселенной.

Формулы сами по себе являются синтаксическими объектами. Им придаются значения посредством интерпретаций. Например, в пропозициональной формуле каждая пропозициональная переменная может интерпретироваться как конкретное предложение, так что общая формула выражает связь между этими предложениями. Однако формула не обязательно должна интерпретироваться, чтобы рассматриваться исключительно как формула.

Пропозициональное исчисление

Формулы исчисления высказываний , также называемые пропозициональными формулами , ^[14] являются выражениями, такими как . Их определение начинается с произвольного выбора множества V пропозициональных переменных . Алфавит состоит из букв в V вместе с символами для пропозициональных связок и скобок "(" и ")", все из которых, как предполагается, отсутствуют в V . Формулы будут определенными выражениями (то есть строками символов) над этим алфавитом. ${\displaystyle (A\land (B\lor C))}$

Формулы индуктивно определяются следующим образом:

• Каждая пропозициональная переменная сама по себе является формулой.
• Если φ — формула, то ¬φ — формула.
• Если φ и ψ — формулы, а • — любая бинарная связка, то ( φ • ψ) — формула. Здесь • может быть (но не ограничивается) обычными операторами ∨, ∧, → или ↔.

Это определение можно также записать в виде формальной грамматики в форме Бэкуса–Наура , при условии, что набор переменных конечен:

< альфа-множество >  ::= p | q | r | s | t | u | ... (произвольное конечное множество пропозициональных переменных) < форма >  ::=  < альфа-множество > | ¬ < форма > | ( < форма > ∧ < форма > ) | ( < форма > ∨ < форма > ) | ( < форма > → < форма > ) | ( < форма > ↔ < форма > )

Используя эту грамматику, последовательность символов

((( п → д ) ∧ ( г → с )) ∨ (¬ д ∧ ¬ с ))

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

(( п → д )→( д q )) п ))

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

Сложная формула может быть трудной для чтения, например, из-за обилия скобок. Чтобы облегчить это последнее явление, правила приоритета (сродни стандартному математическому порядку операций ) предполагаются среди операторов, делая некоторые операторы более обязательными, чем другие. Например, предполагая приоритет (от наиболее обязательных к наименее обязательным) 1. ¬ 2. → 3. ∧ 4. ∨. Тогда формула

((( п → д ) ∧ ( г → с )) ∨ (¬ д ∧ ¬ с ))

может быть сокращено как

р → q ∧ р → с ∨ ¬ q ∧ ¬ с

Однако это всего лишь соглашение, используемое для упрощения письменного представления формулы. Если бы приоритет предполагался, например, как лево-право ассоциативный, в следующем порядке: 1. ¬ 2. ∧ 3. ∨ 4. →, то та же самая формула выше (без скобок) была бы переписана как

( р → ( q ∧ r )) → ( s ∨ (¬ q ∧ ¬ s ))

Логика предикатов

Определение формулы в логике первого порядка относительно сигнатуры рассматриваемой теории. Эта сигнатура определяет константные символы, предикатные символы и функциональные символы рассматриваемой теории, а также арности функциональных и предикатных символов. ${\displaystyle {\mathcal {QS}}}$

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

1. Любая переменная является термином.
2. Любой постоянный символ из сигнатуры является термином
3. выражение вида f ( t ₁ ,..., t _n ), где f — символ n -арной функции, а t ₁ ,..., t _n — термы, снова является термом.

Следующим шагом является определение атомных формул .

1. Если t ₁ и t ₂ являются членами, то t ₁ = t ₂ является атомарной формулой.
2. Если R — n -арный предикатный символ, а t ₁ ,..., t _n — термы, то R ( t ₁ ,..., t _n ) — атомарная формула

Наконец, набор формул определяется как наименьший набор, содержащий набор атомарных формул, такой, что выполняется следующее:

1. ${\displaystyle \neg \phi }$это формула когда это формула ${\displaystyle \phi }$
2. ${\displaystyle (\phi \land \psi )}$и являются формулами, когда и являются формулами; ${\displaystyle (\phi \lor \psi )}$ ${\displaystyle \phi }$ ${\displaystyle \psi }$
3. ${\displaystyle \exists x\,\phi }$является формулой, когда является переменной и является формулой; ${\displaystyle x}$ ${\displaystyle \phi }$
4. ${\displaystyle \forall x\,\phi }$является формулой, когда является переменной, а является формулой (иначе ее можно определить как сокращение от ). ${\displaystyle x}$ ${\displaystyle \phi }$ ${\displaystyle \forall x\,\phi }$ ${\displaystyle \neg \exists x\,\neg \phi }$

Если формула не содержит вхождений или для любой переменной , то она называется ${\displaystyle \exists x}$ ${\displaystyle \forall x}$ ${\displaystyle x}$без квантификаторов . Экзистенциальная формула — это формула, начинающаяся с последовательности экзистенциальных квантификаций, за которой следует бескванторная формула.

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

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

Согласно некоторой терминологии, открытая формула образуется путем объединения атомарных формул с использованием только логических связок, за исключением квантификаторов. ^[15] Это не следует путать с формулой, которая не является закрытой.

Закрытые формулы

Замкнутая формула , также основная формула или предложение , это формула , в которой нет свободных вхождений какой-либо переменной . Если A является формулой языка первого порядка , в которой переменные v ₁ , …, v _n имеют свободные вхождения, то A , которому предшествует ∀ v ₁ ⋯ ∀ v _{n ,} является универсальным замыканием A .

Свойства, применимые к формулам

• Формула A в языке действительна, если она истинна для каждой интерпретации . ${\displaystyle {\mathcal {Q}}}$ ${\displaystyle {\mathcal {Q}}}$
• Формула A в языке выполнима , если она истинна для некоторой интерпретации . ${\displaystyle {\mathcal {Q}}}$ ${\displaystyle {\mathcal {Q}}}$
• Формула A языка арифметики разрешима , если она представляет разрешимое множество , т. е. если существует эффективный метод , который при подстановке свободных переменных A утверждает, что либо полученный экземпляр A доказуем, либо его отрицание доказуемо.

Использование терминологии

В более ранних работах по математической логике (например, Чёрча ^[16] ) формулы относились к любым цепочкам символов, и среди этих цепочек правильно сформированными формулами были те цепочки, которые следовали правилам формирования (правильных) формул.

Некоторые авторы просто говорят «формула». ^{[17] [18] [19] [20]} Современные способы использования (особенно в контексте компьютерной науки с математическим программным обеспечением, таким как программы проверки моделей , автоматизированные программы доказательства теорем , интерактивные программы доказательства теорем ) имеют тенденцию сохранять понятие формулы только в алгебраическом смысле и оставлять вопрос о корректности , т. е. о конкретном строковом представлении формул (использование того или иного символа для связок и квантификаторов, использование того или иного соглашения о скобках , использование польской или инфиксной записи и т. д.) как простую проблему обозначений.

Выражение «хорошо сформированные формулы» (WFF) также проникло в массовую культуру. WFF является частью эзотерического каламбура, использованного в названии академической игры « WFF 'N PROOF : The Game of Modern Logic» Леймана Аллена ^[21], разработанной во время его учебы в Йельской школе права (позже он был профессором Мичиганского университета ). Набор игр предназначен для обучения детей принципам символической логики (в польской нотации ). ^[22] Его название является отголоском whiffenpoof , бессмысленного слова, используемого в качестве подбадривания в Йельском университете и ставшего популярным в песнях «Песня о Whiffenpoof» и «Семейка Whiffenpoofs» . ^[23]

Смотрите также

• Философский портал

• Выражение земли
• Четко определенное выражение
• Формальный язык
• Глоссарий логики
• WFF 'N Доказательство

Примечания

1. Формулы являются стандартной темой вводной логики и рассматриваются во всех вводных учебниках, включая Enderton (2001), Gamut (1990) и Kleene (1967)
2. Генслер, Гарри (2002-09-11). Введение в логику. Routledge. стр. 35. ISBN 978-1-134-58880-0.
3. Холл, Корделия; О'Доннелл, Джон (2013-04-17). Дискретная математика с использованием компьютера. Springer Science & Business Media. стр. 44. ISBN 978-1-4471-3657-6.
4. Аглер, Дэвид В. (2013). Символическая логика: синтаксис, семантика и доказательство. Rowman & Littlefield. стр. 41. ISBN 978-1-4422-1742-3.
5. Симпсон, Р. Л. (2008-03-17). Основы символической логики - Третье издание. Broadview Press. стр. 14. ISBN 978-1-77048-495-5.
6. Ладероут, Карл (2022-10-24). Карманный справочник по формальной логике . Broadview Press. стр. 59. ISBN 978-1-77048-868-7.
7. Маурер, Стивен Б.; Ралстон, Энтони (2005-01-21). Дискретная алгоритмическая математика, третье издание. CRC Press. стр. 625. ISBN 978-1-56881-166-6.
8. Мартин, Роберт М. (2002-05-06). Словарь философа - Третье издание. Broadview Press. стр. 323. ISBN 978-1-77048-215-9.
9. Дейт, Кристофер (14 октября 2008 г.). Словарь реляционных баз данных, расширенное издание. Apress. стр. 211. ISBN 978-1-4302-1042-9.
10. Дата, CJ (2015-12-21). Новый словарь реляционных баз данных: термины, концепции и примеры. "O'Reilly Media, Inc.". стр. 241. ISBN 978-1-4919-5171-2.
11. Симпсон, Р. Л. (1998-12-10). Основы символической логики. Broadview Press. стр. 12. ISBN 978-1-55111-250-3.
12. • "гав" ^{[2] [3] [4] [5]}
    • "дуновение" ^{[6] [7] [8]}
    • "вефф" ^{[9] [10]}
    • "дуновение" ^[11]
    Все источники поддерживают "woof". Источники, цитируемые для "wiff", "weff" и "whiff", дают эти произношения как альтернативы "woof". Источник Gensler приводит "wood" и "woofer" в качестве примеров того, как произносить гласную в "woof".
13. У. Дин, С. Уолш, Предыстория подсистем арифметики второго порядка (2016), стр. 6
14. Логика первого порядка и автоматическое доказательство теорем, Мелвин Фитинг, Springer, 1996 [1]
15. Справочник по истории логики (Том 5, Логика от Рассела до Черча), Логика Тарского под редакцией Кейта Симмонса, Д. Габбея и Дж. Вудса, стр. 568 [2].
16. Алонзо Чёрч, [1996] (1944), Введение в математическую логику, стр. 49
17. Гильберт, Дэвид ; Аккерман, Вильгельм (1950) [1937], Принципы математической логики, Нью-Йорк: Челси
18. Ходжес, Уилфрид (1997), Более короткая модельная теория, Cambridge University Press, ISBN 978-0-521-58713-6 
19. Барвайз, Джон , ред. (1982), Справочник по математической логике, Исследования по логике и основаниям математики, Амстердам: Северная Голландия, ISBN 978-0-444-86388-1 
20. Кори, Рене; Ласкар, Дэниел (2000), Математическая логика: курс с упражнениями, Oxford University Press, ISBN 978-0-19-850048-3 
21. Эренбург 2002
22. Более технически, пропозициональная логика с использованием исчисления в стиле Фитча .
23. Аллен (1965) признает каламбур.

Ссылки

• Аллен, Лейман Э. (1965), «К аутотелическому обучению математической логике с помощью игр WFF 'N PROOF», Математическое обучение: Отчет о конференции, спонсируемой Комитетом по исследованиям интеллектуальных процессов Совета по исследованиям социальных наук , Монографии Общества исследований в области развития ребенка, 30 (1): 29–41
• Булос, Джордж ; Берджесс, Джон; Джеффри, Ричард (2002), Вычислимость и логика (4-е изд.), Cambridge University Press , ISBN 978-0-521-00758-0
• Эренберг, Рэйчел (весна 2002 г.). «Он позитивно логичен». Michigan Today . Мичиганский университет. Архивировано из оригинала 2009-02-08 . Получено 2007-08-19 .
• Эндертон, Герберт (2001), Математическое введение в логику (2-е изд.), Бостон, Массачусетс: Academic Press , ISBN 978-0-12-238452-3
• Гамут, LTF (1990), Логика, язык и значение, том 1: Введение в логику , Издательство Чикагского университета, ISBN 0-226-28085-3
• Ходжес, Уилфрид (2001), «Классическая логика I: логика первого порядка», в Гобл, Лу (ред.), The Blackwell Guide to Philosophical Logic , Blackwell, ISBN 978-0-631-20692-7
• Хофштадтер, Дуглас (1980), Гёдель, Эшер, Бах: Вечная золотая коса , Penguin Books , ISBN 978-0-14-005579-5
• Клини, Стивен Коул (2002) [1967], Математическая логика , Нью-Йорк: Dover Publications , ISBN 978-0-486-42533-7, МР  1950307
• Раутенберг, Вольфганг (2010), Краткое введение в математическую логику (3-е изд.), Нью-Йорк: Springer Science+Business Media , doi :10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6

Внешние ссылки

• Правильно сформированная формула для логики предикатов первого порядка — включает краткий тест по Java .
• Правильно сформированная формула в ProvenMath