Правильная формула - Well-formed formula

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

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

Вступление

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

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

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

Исчисление высказываний

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1. Если т₁ и т₂ условия тогда т₁=т₂ атомарная формула
2. Если р является п-арный предикатный символ, и т₁,...,т_п условия, тогда р(т₁,...,т_п) является атомарной формулой

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

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}$, то он называется бескванторный. An экзистенциальная формула формула, начинающаяся с последовательности экзистенциальная количественная оценка а затем формула без кванторов.

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

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

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

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

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

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

А закрытая формула, также земля формула или предложение, это формула, в которой нет бесплатные вхождения любой переменная. Если А - формула языка первого порядка, в которой переменные v₁, ..., v_п иметь свободные вхождения, то А предшествует ${\displaystyle \forall }$v₁ ... ${\displaystyle \forall }$v_п это закрытие А.

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

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

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

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

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

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

Выражение «правильно сформированные формулы» (WFF) также вошло в массовую культуру. ВФФ является частью эзотерического каламбура, используемого в названии академической игры "WFF 'N ДОКАЗАТЕЛЬСТВО: Игра современной логики », автор - обыватель Аллен,^[12] разработан, когда он был в Йельская школа права (позже он был профессором университет Мичигана ). Набор игр предназначен для обучения детей принципам символической логики (в Польская нотация ).^[13] Его название - отголосок Whiffenpoof, а бессмысленное слово используется как радость в Йельский университет сделал популярным в Песня Whiffenpoof и Уиффенпуф.^[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. Р. Л. Симпсон (1999), Основы символической логики, стр. 12
11. Мендельсон, Эллиотт [2010] (1964), Введение в математическую логику (5-е изд.), Лондон: Chapman & Hall
12. Эренбург 2002
13. Технически, логика высказываний с использованием Расчет в стиле Fitch.
14. Аллен (1965) признает каламбур.

Рекомендации

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

внешняя ссылка

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