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

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

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

Введение [ править ]

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

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

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

Исчисление высказываний [ править ]

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

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

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

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

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

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

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

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

(( п → q )→( qq )) п ))

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

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

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

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

п → q ∧ r → s ∨ ¬ q ∧ ¬ s

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

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

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

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

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

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

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

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

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

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

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

Атомарные и открытые формулы [ править ]

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

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

Закрытые формулы [ править ]

Замкнутая формула , также основная формула или предложение , — это формула, в которой нет свободных вхождений какой-либо переменной . Если A — формула языка первого порядка, в которой переменные $v 1, \dots, v n$ имеют свободное вхождение, то A, которым стоит $\forall v 1 \dots \forall v n,$ является универсальным замыканием A перед .

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

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

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

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

Некоторые авторы просто говорят «формула». ^[6]^[7]^[8]^[9] Современные обычаи (особенно в контексте информатики с математическим программным обеспечением, таким как средства проверки моделей , автоматизированные средства доказательства теорем , интерактивные средства доказательства теорем ) имеют тенденцию сохранять понятие формулы только как алгебраическое понятие и оставлять вопрос о правильности формулировки , т.е. конкретное строковое представление формул (с использованием того или иного символа для связок и кванторов, с использованием того или иного соглашения о заключении скобок , с использованием польской или инфиксной записи и т. д.) как просто проблема нотации.

Хотя выражение «правильно сформированная формула» все еще используется, ^[10]^[11]^[12] эти авторы не обязательно ^{[ ласковые слова ]} используйте его в отличие от старого смысла формулы , который больше не распространен в математической логике. ^{[ нужна цитата ]}

Выражение «правильно сформированные формулы» (WFF) также проникло в массовую культуру. WFF — это часть эзотерического каламбура, используемого в названии академической игры « WFF 'N PROOF : The Game of Modern Logic», автором которой является Лэйман Аллен. ^[13]разработал, когда он учился на юридической школе Йельского университета (позже он был профессором Мичиганского университета ). Комплекс игр предназначен для обучения детей основам символической логики (в польских обозначениях ). ^[14] Его название является отголоском слова «wiffenpoof» , бессмысленного слова , используемого в качестве приветствия в Йельском университете и ставшего популярным в песнях «Whiffenpoof Song» и «The Whiffenpoofs» . ^[15]

См. также [ править ]

Примечания [ править ]

^ Формулы являются стандартной темой вводной логики и рассматриваются во всех вводных учебниках, включая Enderton (2001), Gamut (1990) и Kleene (1967).
^ У. Дин, С. Уолш, Предыстория подсистем арифметики второго порядка (2016), стр.6
^ Логика первого порядка и автоматическое доказательство теорем, Мелвин Фиттинг, Springer, 1996 [1]
^ Справочник по истории логики (Том 5, Логика от Рассела до Черча), логика Тарского Кейта Симмонса, Д. Габбея и Дж. Вудса Eds, стр. 568 [2] .
^ Алонзо Чёрч, [1996] (1944), Введение в математическую логику, стр. 49
^ Гильберт, Дэвид ; Акерманн, Вильгельм (1950) [1937], Принципы математической логики, Нью-Йорк: Челси.
^ Ходжес, Уилфрид (1997), Более короткая теория модели, Cambridge University Press, ISBN 978-0-521-58713-6
^ Барвайз, Джон , изд. (1982), Справочник по математической логике, Исследования по логике и основам математики, Амстердам: Северная Голландия, ISBN 978-0-444-86388-1
^ Кори, Рене; Ласкар, Дэниел (2000), Математическая логика: курс с упражнениями, Oxford University Press, ISBN 978-0-19-850048-3
^ Эндертон, Герберт [2001] (1972), Математическое введение в логику (2-е изд.), Бостон, Массачусетс: Academic Press, ISBN 978-0-12-238452-3
^ Р.Л. Симпсон (1999), Основы символической логики, стр. 12
^ Мендельсон, Эллиотт [2010] (1964), Введение в математическую логику (5-е изд.), Лондон: Chapman & Hall
^ Эренбург 2002
^ Более технически, пропозициональная логика с использованием исчисления в стиле Fitch .
^ Аллен (1965) признает каламбур.

Ссылки [ править ]

Аллен, Лэйман Э. (1965), «К автотелическому обучению математической логики с помощью игр WFF 'N PROOF», Математическое обучение: отчет конференции, спонсируемой комитетом по исследованию интеллектуальных процессов Совета социальных наук , монографии Общество исследований развития детей, 30 (1): 29–41.
Булос, Джордж ; Берджесс, Джон; Джеффри, Ричард (2002), Вычислимость и логика (4-е изд.), Cambridge University Press , ISBN 978-0-521-00758-0
Эренберг, Рэйчел (весна 2002 г.). «Он положительно логичен» . Мичиган сегодня . Университет Мичигана. Архивировано из оригинала 8 февраля 2009 г. Проверено 19 августа 2007 г.
Эндертон, Герберт (2001), Математическое введение в логику (2-е изд.), Бостон, Массачусетс: Academic Press , ISBN 978-0-12-238452-3
Гамут, LTF (1990), Логика, язык и значение, Том 1: Введение в логику , University of Chicago Press, ISBN 0-226-28085-3
Ходжес, Уилфрид (2001), «Классическая логика I: логика первого порядка», в Гобл, Лу (редактор), « Руководство Блэквелла по философской логике» , Блэквелл, 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

[1] Формулы являются стандартной темой вводной логики и рассматриваются во всех вводных учебниках, включая Enderton (2001), Gamut (1990) и Kleene (1967).

[2] У. Дин, С. Уолш, Предыстория подсистем арифметики второго порядка (2016), стр.6

[3] Логика первого порядка и автоматическое доказательство теорем, Мелвин Фиттинг, Springer, 1996 [1]

[4] Справочник по истории логики (Том 5, Логика от Рассела до Черча), логика Тарского Кейта Симмонса, Д. Габбея и Дж. Вудса Eds, стр. 568 [2] .

[5] Алонзо Чёрч, [1996] (1944), Введение в математическую логику, стр. 49

[6] Гильберт, Дэвид ; Акерманн, Вильгельм (1950) [1937], Принципы математической логики, Нью-Йорк: Челси.

[7] Ходжес, Уилфрид (1997), Более короткая теория модели, Cambridge University Press, ISBN 978-0-521-58713-6

[8] Барвайз, Джон , изд. (1982), Справочник по математической логике, Исследования по логике и основам математики, Амстердам: Северная Голландия, ISBN 978-0-444-86388-1

[9] Кори, Рене; Ласкар, Дэниел (2000), Математическая логика: курс с упражнениями, Oxford University Press, ISBN 978-0-19-850048-3

[10] Эндертон, Герберт [2001] (1972), Математическое введение в логику (2-е изд.), Бостон, Массачусетс: Academic Press, ISBN 978-0-12-238452-3

[11] Р.Л. Симпсон (1999), Основы символической логики, стр. 12

[12] Мендельсон, Эллиотт [2010] (1964), Введение в математическую логику (5-е изд.), Лондон: Chapman & Hall

[13] Эренбург 2002

[14] Более технически, пропозициональная логика с использованием исчисления в стиле Fitch .

[15] Аллен (1965) признает каламбур.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]