Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

В математической логике , логики высказываний и логики предикатов , А хорошо сформированные формула , сокращенно ВФФ или Пп , часто просто формула , конечная последовательность из символов из заданного алфавита , которая является частью формального языка . [1] Формальный язык можно отождествить с набором формул в языке.

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

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

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

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

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

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

Основная статья: Исчисление высказываний

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

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

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

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

< альфа-набор >  :: = p | q | г | с | т | u | ... (произвольный конечный набор пропозициональных переменных) < form >  :: =  < alpha set > | ¬ < форма > | ( < форма > ∧ < форма > ) | ( < форма > ∨ < форма > ) | ( < форма > → < форма > ) | ( < форма > ↔ < форма > )

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

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

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

(( p → q ) → ( qq )) p ))

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

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

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

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

p → q ∧ r → s ∨ ¬ q ∧ ¬ s

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

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

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

Определение формулы в логике первого порядка зависит от сигнатуры рассматриваемой теории. Эта сигнатура определяет постоянные символы, предикатные символы и функциональные символы рассматриваемой теории, а также арности функциональных и предикатных символов.

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

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

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

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

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

  1. это формула, когда это формула
  2. и являются формулами, когда и являются формулами;
  3. - формула, когда - переменная, и - формула;
  4. - это формула, когда - переменная, и - формула (в качестве альтернативы может быть определено как сокращение для ).

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

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

Основная статья: Атомная формула

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

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

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

Основная статья: Предложение (логика)

Замкнутая формула , также измельчает формула или фраза , формула , в которой есть нет свободных вхождения любого переменного . Если формула языка первого порядка , в которых переменные v 1 , ..., V п есть свободные вхождения, то предшествует v 1 ⋯ V п является замыкание A .

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

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

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

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

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

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

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

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

  • Основное выражение

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

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

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

  • Аллен, Лейман Э. (1965), "К автотелическому изучению математической логики с помощью игр WFF 'N PROOF", Математическое обучение: отчет конференции, спонсируемой Комитетом по исследованию интеллектуальных процессов Совета по исследованиям в области социальных наук , Монографии Общество исследований в области детского развития, 30 (1): 29–41
  • Булос, Джордж ; Берджесс, Джон; Джеффри, Ричард (2002), вычислимость и логика (4-е изд.), Cambridge University Press , ISBN 978-0-521-00758-0
  • Эренберг, Рэйчел (весна 2002 г.). «Он позитивно логичен» . Мичиган сегодня . Университет Мичигана. Архивировано из оригинала на 2009-02-08 . Проверено 19 августа 2007 .
  • Эндертон, Герберт (2001), Математическое введение в логику (2-е изд.), Бостон, Массачусетс: Academic Press , ISBN 978-0-12-238452-3
  • Gamut, LTF (1990), логика, язык и значение, том 1: Введение в логику , University Of Chicago Press, 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, MR  1950307
  • Раутенберг, Вольфганг (2010), Краткое введение в математическую логику (3-е изд.), Нью-Йорк : Springer Science + Business Media , DOI : 10.1007 / 978-1-4419-1221-3 , ISBN 978-1-4419-1220-6

Внешние ссылки [ править ]

  • Хорошо сформированная формула для логики предикатов первого порядка - включает небольшую викторину по Java .
  • Хорошо сформированная формула в ProvenMath