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

Отдел формальной логики

Исчисление высказываний — это раздел логики . Ее также называют логикой высказываний , логикой утверждений , исчислением предложений , логикой предложений или иногда логикой нулевого порядка . Он имеет дело с предложениями (которые могут быть истинными или ложными) и отношениями между предложениями, включая построение основанных на них аргументов. Сложные предложения образуются путем соединения предложений логическими связками . Предложения, не содержащие логических связок, называются атомарными предложениями.

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

Объяснение

Логические связки встречаются в естественных языках. В английском языке некоторыми примерами являются «and» ( союз ), «or» ( дизъюнкция ), «not» ( отрицание ) и «if» (но только когда они используются для обозначения материального условного предложения ).

Ниже приводится пример очень простого вывода в рамках логики высказываний:

Посылка 1: Если идет дождь, значит, облачно.

Предпосылка 2: Идет дождь.

Вывод: облачно.

И посылки, и заключение являются предложениями. Посылки принимаются как нечто само собой разумеющееся, и с применением modus ponens ( правила вывода ) из этого следует вывод.

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

Предпосылка 1: ${\displaystyle P\to Q}$

Предпосылка 2: ${\displaystyle P}$

Заключение: ${\displaystyle Q}$

То же самое можно кратко сформулировать следующим образом:

${\displaystyle {\frac {P\to Q,P}{Q}}}$

Когда P интерпретируется как «Идет дождь», а Q как «облачно», можно увидеть, что приведенные выше символические выражения точно соответствуют исходному выражению на естественном языке. Мало того, они также будут соответствовать любому другому выводу этой формы , который будет действительным на том же основании, что и этот вывод.

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

Когда формальная система используется для представления формальной логики, непосредственно представляются только буквы утверждений (обычно заглавные латинские буквы, такие как , и ). Предложения естественного языка, возникающие при их интерпретации, находятся за пределами системы, и отношения между формальной системой и ее интерпретацией также находятся за пределами самой формальной системы. ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle R}$

В классической истинностно-функциональной логике высказываний формулы интерпретируются как имеющие ровно одно из двух возможных значений истинности : истинностное значение « истина» или истинностное значение « ложь» . ^[1] Поддерживаются принцип бивалентности и закон исключенного третьего . Истинно-функциональная пропозициональная логика, определенная как таковая, и изоморфные ей системы считаются логикой нулевого порядка . Однако возможны и альтернативные пропозициональные логики. Дополнительную информацию см. в разделе «Другие логические исчисления» ниже.

История

Хотя на логику высказываний (которая взаимозаменяема с исчислением высказываний) намекали более ранние философы, она была развита в формальную логику ( логику стоиков ) Хрисиппом в III веке до нашей эры ^[2] и расширена его преемниками стоиками . Логика была сосредоточена на предложениях . Это продвижение отличалось от традиционной силлогистической логики , которая была сосредоточена на терминах . Однако большая часть оригинальных сочинений была утеряна ^[3] , а логика высказываний, разработанная стоиками, уже не была понята позднее, в античности. ^{[ нужна цитация ]} Следовательно, система была по существу заново изобретена Питером Абеляром в 12 веке. ^[4]

Пропозициональная логика в конечном итоге была усовершенствована с использованием символической логики . Математику 17-го и 18-го веков Готфриду Лейбницу приписывают звание основателя символической логики за его работу с рассудочным расчетом . Хотя его работа была первой в своем роде, она была неизвестна широкому логическому сообществу. Следовательно, многие достижения Лейбница были воссозданы такими логиками, как Джордж Буль и Огастес Де Морган , — совершенно независимыми от Лейбница. ^[5]

Точно так же, как логику высказываний можно считать развитием более ранней силлогистической логики, логику предикатов Готтлоба Фреге также можно считать развитием более ранней логики высказываний. Один автор описывает логику предикатов как сочетание «отличительных черт логики силлогистики и логики высказываний». ^[6] Следовательно, логика предикатов открыла новую эру в истории логики; однако прогресс в логике высказываний все еще был достигнут после Фреге, включая естественную дедукцию , деревья истинности и таблицы истинности . Естественная дедукция была изобретена Герхардом Генценом и Станиславом Ясковским . Деревья истины были изобретены Эвертом Виллемом Бет . ^[7] Однако авторство изобретения таблиц истинности неясно.

В работах Фреге ^[8] и Бертрана Рассела ^[9] содержатся идеи , оказавшие влияние на изобретение таблиц истинности. Фактическая табличная структура (отформатированная в виде таблицы) обычно приписывается либо Людвигу Витгенштейну , либо Эмилю Посту (или обоим, независимо). ^[8] Помимо Фреге и Рассела, другие авторы идей, предшествовавших таблицам истинности, включают Филона, Буля, Чарльза Сандерса Пирса , ^[10] и Эрнста Шредера . Табличную структуру приписывают Яну Лукасевичу , Альфреду Норту Уайтхеду , Уильяму Стэнли Джевонсу , Джону Венну и Кларенсу Ирвингу Льюису . ^[9] В конце концов, некоторые, как Джон Шоски, пришли к выводу, что «далеко не очевидно, что какому-то одному человеку следует давать титул «изобретателя» таблиц истинности». ^[9]

Терминология

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

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

Набор аксиом может быть пустым, непустым конечным множеством или счетным бесконечным множеством (см. схему аксиом ). Формальная грамматика рекурсивно определяет выражения и правильно построенные формулы языка . Кроме того, может быть задана семантика , определяющая истину и оценки (или интерпретации ).

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

1. набор примитивных символов, называемых по-разному атомарными формулами , заполнителями , буквами предложений или переменными , и
2. набор операторных символов, по-разному интерпретируемых как логические операторы или логические связки .

Правильно составленная формула — это любая атомарная формула или любая формула, которая может быть составлена ​​из атомарных формул с помощью операторных символов в соответствии с правилами грамматики.

Математики иногда различают пропозициональные константы, пропозициональные переменные и схемы. Пропозициональные константы представляют собой какое-то конкретное предложение, тогда как пропозициональные переменные охватывают множество всех атомарных предложений. Однако схемы охватывают все предложения. Пропозициональные константы принято обозначать буквами A , B и C , пропозициональные переменные — буквами P , Q и R , а схематические буквы часто представляют собой греческие буквы, чаще всего φ , ψ и χ .

Базовые концепты

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

1. их язык (т. е. конкретный набор примитивных символов и операторных символов),
2. набор аксиом или отличительных формул, и
3. набор правил вывода.

Любое данное предложение может быть представлено буквой, называемой «пропозициональной константой», аналогично представлению числа буквой в математике (например, a = 5 ). Все предложения требуют ровно одного из двух истинностных значений: истинного или ложного. Например, пусть P — предложение о том, что на улице идет дождь. Это будет истинно ( P ), если на улице идет дождь, и ложным в противном случае ( ¬ P ).

• Затем мы определяем операторы функциональной истинности , начиная с отрицания. ¬P представляет собой отрицание P , которое можно рассматривать как отрицание P. В приведенном выше примере ¬ P выражает то, что на улице не идет дождь, или более стандартным прочтением: «Это не тот случай, когда на улице идет дождь». Когда P истинно, ¬ P ложно; и когда P ложно, ¬ P истинно. В результате ¬ ¬ P всегда имеет то же истинностное значение, что и P .
• Союз — это функционально-истинная связка , которая образует предложение из двух более простых предложений, например P и Q. Соединение P и Q записывается P ∧ Q и означает, что каждое из них истинно. Мы читаем P ∧ Q как « P и Q ». Для любых двух предложений существует четыре возможных присвоения значений истинности:
  1. P верно, а Q верно
  2. P истинно, а Q ложно
  3. P ложно, а Q истинно
  4. P ложно и Q ложно

Соединение P и Q истинно в случае 1 и ложно в противном случае. Где P — это утверждение, что на улице идет дождь, а Q — это утверждение, что над Канзасом находится холодный фронт, P ∧ Q истинно, когда снаружи идет дождь и над Канзасом существует холодный фронт. Если на улице нет дождя, то P ∧ Q ложно; и если над Канзасом нет холодного фронта, то P ∧ Q также ложно.

• Дизъюнкция напоминает конъюнкцию тем, что образует предложение из двух более простых предложений. Пишем P ∨ Q , а читается « P или Q ». Оно выражает, что истинно либо P , либо Q. Таким образом, в перечисленных выше случаях дизъюнкция P с Q верна во всех случаях, кроме случая 4. Используя приведенный выше пример, дизъюнкция выражает то, что либо на улице идет дождь, либо над Канзасом существует холодный фронт. (Обратите внимание, что такое использование дизъюнкции должно напоминать использование английского слова «или». Однако оно больше всего похоже на английское включающее «или», которое может использоваться для выражения истинности по крайней мере одного из двух предложений. Другими словами, исключающее «или» ложно, когда и P , и Q истинны (случай 1), и аналогичным образом ложно, когда оба P и Q являются ложными (случай 4). Примером исключающего или является: Вы можете оставить торт (на потом) или можете съесть его все сейчас, но вы не можете одновременно съесть все это сейчас и оставить на потом. Часто в естественном языке, учитывая соответствующий контекст, дополнение «но не то и другое» опускается, но подразумевается. ".)
• Материальный кондиционал также объединяет два более простых предложения, и мы пишем P → Q , что читается «если P, то Q ». Предложение слева от стрелки называется антецедентом, а предложение справа — консеквентом. (Не существует такого обозначения для конъюнкции или дизъюнкции, поскольку они являются коммутативными операциями.) Он выражает, что Q истинно всякий раз, когда P истинно. Таким образом, P → Q истинно во всех случаях, описанных выше, кроме случая 2, поскольку это единственный случай, когда P истинно, а Q — нет. Используя пример, если P, то Q выражает, что если на улице идет дождь, то над Канзасом находится холодный фронт. Материальное условное часто путают с физической причинностью. Материальный кондиционал, однако, связывает два предложения только посредством их истинностных значений, что не является отношением причины и следствия. В литературе спорно, представляет ли материальный смысл логическую причинно-следственную связь.
• Бикондиционал объединяет два более простых предложения, и мы пишем P ↔ Q , что читается « P тогда и только тогда, когда Q ». Оно выражает то, что P и Q имеют одинаковое истинностное значение, как и в случаях 1 и 4. « P истинно тогда и только тогда, когда Q истинно, и ложно в противном случае.

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

Закрытие в процессе эксплуатации

Пропозициональная логика замкнута относительно функционально-истинных связок. Другими словами, для любого предложения φ ¬ φ также является предложением. Аналогично для любых предложений φ и ψ φ ∧ ψ является предложением, и аналогично для дизъюнкции, условного и двуусловного . Это означает, что, например, φ ∧ ψ является предложением, и поэтому его можно соединить с другим предложением. Чтобы это представить, нам нужно использовать круглые скобки, чтобы указать, какое предложение с каким соединяется. Например, P ∧ Q ∧ R не является корректной формулой, поскольку мы не знаем, соединяем ли мы P ∧ Q с R или соединяем P с Q ∧ R . Таким образом, мы должны написать либо ( P ∧ Q ) ∧ R для обозначения первого, либо P ∧ ( Q ∧ R ) для обозначения второго. Оценивая условия истинности, мы видим, что оба выражения имеют одинаковые условия истинности (будут истинны в одних и тех же случаях), и более того, что любое суждение, образованное произвольными союзами, будет иметь одинаковые условия истинности, независимо от расположения скобок. Это означает, что союз ассоциативен , однако не следует считать, что круглые скобки никогда не служат какой-либо цели. Например, предложение P ∧ ( Q ∨ R ) не имеет тех же условий истинности, что и ( P ∧ Q ) ∨ R , поэтому это разные предложения, отличающиеся только круглыми скобками. Это можно проверить с помощью метода таблицы истинности, упомянутого выше.

Примечание. Для любого произвольного числа пропозициональных констант мы можем сформировать конечное число случаев, в которых перечислены их возможные истинностные значения. Простой способ создать это — использовать таблицы истинности, в которых пишут P , Q , ..., Z для любого списка из k пропозициональных констант, то есть любого списка пропозициональных констант с k элементами. Ниже этого списка записывается 2 ^k строк, а ниже P заполняется первая половина строк значением true (или T), а вторая половина — значением false (или F). Ниже Q одна четверть строк заполняется буквой T, затем одна четверть буквой F, затем одна четверть буквой T и последняя четверть буквой F. В следующем столбце чередуются значения «истина» и «ложь» для каждой восьмой строки, затем шестнадцатые и так далее, пока последняя пропозициональная константа не будет меняться между T и F для каждой строки. Это даст полный список случаев или присвоений истинностного значения, возможных для этих пропозициональных констант.

Аргумент

Затем исчисление высказываний определяет аргумент как список предложений. Действительный аргумент — это список предложений, последнее из которых следует из остальных или подразумевается из них. Все остальные аргументы недействительны. Самый простой действительный аргумент — modus ponens , одним из примеров которого является следующий список предложений:

${\displaystyle {\begin{array}{rl}1.&P\to Q\\2.&P\\\hline \therefore &Q\end{array}}}$

Это список из трёх предложений, каждая строка — предложение, а последнее вытекает из остальных. Первые две строки называются посылками, а последняя – заключением. Мы говорим, что любое предложение C следует из любого набора предложений , если C должно быть истинным всякий раз, когда каждый член набора истинен. В приведенном выше рассуждении для любых P и Q всякий раз, когда P → Q и P истинны, обязательно Q истинно. Обратите внимание: когда P истинно, мы не можем рассматривать случаи 3 и 4 (из таблицы истинности). Когда P → Q истинно, мы не можем рассматривать случай 2. Остается только случай 1, в котором Q также истинно. Таким образом, Q подразумевается из посылок. ${\displaystyle (P_{1},...,P_{n})}$ ${\displaystyle (P_{1},...,P_{n})}$

Это схематично обобщает. Таким образом, где φ и ψ могут быть вообще любыми предложениями,

${\displaystyle {\begin{array}{rl}1.&\varphi \to \psi \\2.&\varphi \\\hline \therefore &\psi \end{array}}}$

Другие формы аргументов удобны, но не обязательны. Учитывая полный набор аксиом (один из таких наборов см. ниже), modus ponens достаточен для доказательства всех других форм аргументов в логике высказываний, поэтому их можно рассматривать как производные. Обратите внимание: это не относится к расширению логики высказываний на другие логики, такие как логика первого порядка . Логика первого порядка требует по крайней мере одного дополнительного правила вывода для достижения полноты .

Значение аргумента в формальной логике состоит в том, что из установленных истин можно получить новые истины. В первом примере выше, учитывая две посылки, истинность Q еще не известна и не заявлена. После того, как аргумент приведен, выводится Q. Таким образом, мы определяем систему вывода как набор всех предложений, которые могут быть выведены из другого набора предложений. Например, учитывая набор предложений , мы можем определить систему вывода Γ , которая представляет собой набор всех предложений, которые следуют из A. Повторение всегда предполагается, поэтому . Кроме того, из первого элемента A , последнего элемента, а также modus ponens, R является следствием и так далее . Однако, поскольку мы не включили достаточно полные аксиомы, ничего другого вывести невозможно. Таким образом, хотя большинство систем дедукции, изучаемых в логике высказываний, способны выводить , эта система слишком слаба, чтобы доказать такое утверждение. ${\displaystyle A=\{P\lor Q,\neg Q\land R,(P\lor Q)\to R\}}$ ${\displaystyle P\lor Q,\neg Q\land R,(P\lor Q)\to R\in \Gamma }$ ${\displaystyle R\in \Gamma }$ ${\displaystyle (P\lor Q)\leftrightarrow (\neg P\to Q)}$

Общее описание исчисления высказываний

Исчисление высказываний — это ^{формальная} система , ^{где :} ${\displaystyle {\mathcal {L}}={\mathcal {L}}\left(\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I} \right)}$

• Альфа -множество представляет собой счетный бесконечный набор элементов, называемых символами высказываний или пропозициональными переменными . Синтаксически говоря, это самые основные элементы формального языка , иначе называемые атомарными формулами или терминальными элементами . В последующих примерах элементами обычно являются буквы p , q , r и т. д. ${\displaystyle \mathrm {A} }$ ${\displaystyle {\mathcal {L}}}$ ${\displaystyle \mathrm {A} }$
• Омега -множество Ω — это конечное множество элементов, называемых операторными символами или логическими связками . Множество Ω разбивается на непересекающиеся подмножества следующим образом :

  ${\displaystyle \Omega =\Omega _{0}\cup \Omega _{1}\cup \cdots \cup \Omega _{j}\cup \cdots \cup \Omega _{m}.}$

  В этом разбиении находится набор операторных символов арности j . ${\displaystyle \Omega _{j}}$

  В более знакомых исчислениях высказываний Ω обычно разбивается следующим образом:

  ${\displaystyle \Omega _{1}=\{\lnot \},}$

  ${\displaystyle \Omega _{2}\subseteq \{\land ,\lor ,\to ,\leftrightarrow \}.}$

  Часто принимаемое соглашение рассматривает постоянные логические значения как операторы нулевой арности, таким образом:

  ${\displaystyle \Omega _{0}=\{\bot ,\top \}.}$

  Некоторые авторы используют тильду (~) или N вместо ¬ ; а некоторые используют v вместо амперсанда ( &), префикса K или вместо . Обозначения различаются еще больше для набора логических значений: такие символы, как {false, true}, {F, T} или {0, 1}, все встречаются в различных контекстах вместо . ${\displaystyle \vee }$ ${\displaystyle \cdot }$ ${\displaystyle \wedge }$ ${\displaystyle \{\bot ,\top \}}$
• Дзета -множество — это конечный набор правил преобразования , которые называются правилами вывода , когда они приобретают логические применения. ${\displaystyle \mathrm {Z} }$
• Множество йоты — это счетное множество начальных точек , которые называются аксиомами , когда получают логические интерпретации. ${\displaystyle \mathrm {I} }$

Язык , также известный как набор формул , правильно построенных формул , индуктивно определяется следующими правилами: ${\displaystyle {\mathcal {L}}}$

1. База: любой элемент альфа-набора представляет собой формулу . ${\displaystyle \mathrm {A} }$ ${\displaystyle {\mathcal {L}}}$
2. Если есть формулы и находится в , то это формула. ${\displaystyle p_{1},p_{2},\ldots ,p_{j}}$ ${\displaystyle f}$ ${\displaystyle \Omega _{j}}$ ${\displaystyle fp_{1}p_{2}\ldots p_{j}}$
3. Закрыто: Ничто иное не является формулой . ${\displaystyle {\mathcal {L}}}$

Повторное применение этих правил позволяет строить сложные формулы. Например:

• По правилу 1 p — формула.
• По правилу 2 это формула. ${\displaystyle \neg p}$
• По правилу 1 q является формулой.
• По правилу 2 это формула. ^{[примечание 1]} ${\displaystyle \neg p\lor q}$

Пример 1. Простая система аксиом.

Пусть , где , , , определены следующим образом: ${\displaystyle {\mathcal {L}}_{1}={\mathcal {L}}(\mathrm {A} ,\Omega ,\mathrm {Z} ,\mathrm {I} )}$ ${\displaystyle \mathrm {A} }$ ${\displaystyle \Omega }$ ${\displaystyle \mathrm {Z} }$ ${\displaystyle \mathrm {I} }$

• Множество , счетное бесконечное множество символов, которые служат для представления логических предложений: ${\displaystyle \mathrm {A} }$

  ${\displaystyle \mathrm {A} =\{p,q,r,s,t,u,p_{2},\ldots \}.}$

• Функционально полный набор логических операторов (логических связок и отрицаний) выглядит следующим образом. Из трех связок конъюнкции, дизъюнкции и импликации ( и → ) одну можно считать примитивной, а две другие можно определить через нее и отрицание ( ¬ ). ^[11] Альтернативно, все логические операторы могут быть определены в терминах единственного достаточного оператора , такого как штрих Шеффера (nand). Бикондиционал ( ), конечно, может быть определен в терминах конъюнкции и импликации как . ${\displaystyle \Omega }$ ${\displaystyle \wedge ,\lor }$ ${\displaystyle a\leftrightarrow b}$ ${\displaystyle (a\to b)\land (b\to a)}$
  Принятие отрицания и импликации в качестве двух примитивных операций исчисления высказываний равносильно разделению множества омега следующим образом: ${\displaystyle \Omega =\Omega _{1}\cup \Omega _{2}}$

  ${\displaystyle \Omega _{1}=\{\lnot \},}$

  ${\displaystyle \Omega _{2}=\{\to \}.}$

Тогда определяется как и определяется как . ${\displaystyle a\lor b}$ ${\displaystyle \neg a\to b}$ ${\displaystyle a\land b}$ ${\displaystyle \neg (a\to \neg b)}$

• Набор (множество начальных точек логического вывода, т. е. логических аксиом) представляет собой систему аксиом, предложенную Яном Лукасевичем и используемую как часть исчисления высказываний системы Гильберта . Все аксиомы являются примерами замены : ${\displaystyle \mathrm {I} }$
  • ${\displaystyle p\to (q\to p)}$
  • ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$
  • ${\displaystyle (\neg p\to \neg q)\to (q\to p)}$
• Набор правил преобразования (правил вывода) является единственным правилом modus ponens (т.е. из любых формул вида и , infer ). ${\displaystyle \mathrm {Z} }$ ${\displaystyle \varphi }$ ${\displaystyle (\varphi \to \psi )}$ ${\displaystyle \psi }$

Эта система используется в базе данных формальных доказательств Metamath set.mm.

Пример 2. Система естественного вычета

Пусть , где , , , определены следующим образом: ${\displaystyle {\mathcal {L}}_{2}={\mathcal {L}}(\mathrm {A} ,\Omega ,\mathrm {Z} ,\mathrm {I} )}$ ${\displaystyle \mathrm {A} }$ ${\displaystyle \Omega }$ ${\displaystyle \mathrm {Z} }$ ${\displaystyle \mathrm {I} }$

• Альфа-множество — это счетный бесконечный набор символов, например: ${\displaystyle \mathrm {A} }$

  ${\displaystyle \mathrm {A} =\{p,q,r,s,t,u,p_{2},\ldots \}.}$

• Омега установила разделы следующим образом: ${\displaystyle \Omega =\Omega _{1}\cup \Omega _{2}}$

  ${\displaystyle \Omega _{1}=\{\lnot \},}$

  ${\displaystyle \Omega _{2}=\{\land ,\lor ,\to ,\leftrightarrow \}.}$

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

• Множество начальных точек пусто, т.е. ${\displaystyle \mathrm {I} =\varnothing }$
• Набор правил преобразования описывается следующим образом: ${\displaystyle \mathrm {Z} }$

Наше исчисление высказываний имеет одиннадцать правил вывода. Эти правила позволяют нам выводить другие истинные формулы на основе набора формул, которые считаются истинными. Первые десять просто утверждают, что мы можем вывести определенные правильные формулы из других правильных формул. Последнее правило, однако, использует гипотетические рассуждения в том смысле, что в предпосылках правила мы временно предполагаем, что (недоказанная) гипотеза является частью набора выведенных формул, чтобы посмотреть, сможем ли мы вывести некоторую другую формулу. Поскольку первые десять правил этого не делают, их обычно описывают как негипотетические правила, а последнее — как гипотетическое правило.

При описании правил преобразования можно ввести метаязыковый символ . По сути, это удобное сокращение для выражения «сделай вывод». Формат: , в котором Γ — (возможно, пустой) набор формул, называемых посылками, а ψ — формула, называемая заключением. Правило преобразования означает, что если каждое предложение в Γ является теоремой (или имеет то же истинностное значение, что и аксиомы), то ψ также является теоремой. Принимая во внимание следующее правило «Введение в конъюнкцию» , мы будем знать, что всякий раз, когда Γ имеет более одной формулы, мы всегда можем безопасно свести ее к одной формуле, используя конъюнкцию. Короче говоря, с этого момента мы можем представлять Γ как одну формулу, а не как набор. Еще одно упущение для удобства — когда Γ — пустое множество, и в этом случае Γ может не появиться. ${\displaystyle \vdash }$ ${\displaystyle \Gamma \vdash \psi }$ ${\displaystyle \Gamma \vdash \psi }$

Введение отрицания

Из и сделайте вывод . ${\displaystyle (p\to q)}$ ${\displaystyle (p\to \neg q)}$ ${\displaystyle \neg p}$

То есть, . ${\displaystyle \{(p\to q),(p\to \neg q)\}\vdash \neg p}$

Устранение отрицания

Из , сделайте вывод . ${\displaystyle \neg p}$ ${\displaystyle (p\to r)}$

То есть, . ${\displaystyle \{\neg p\}\vdash (p\to r)}$

Устранение двойного отрицания

Из , сделайте вывод р . ${\displaystyle \neg \neg p}$

То есть, . ${\displaystyle \neg \neg p\vdash p}$

Знакомство с союзом

Из p и q сделайте вывод . ${\displaystyle (p\land q)}$

То есть, . ${\displaystyle \{p,q\}\vdash (p\land q)}$

Устранение союза

Из , сделайте вывод р . ${\displaystyle (p\land q)}$

Из , сделайте вывод q . ${\displaystyle (p\land q)}$

То есть и . ${\displaystyle (p\land q)\vdash p}$ ${\displaystyle (p\land q)\vdash q}$

Введение в дизъюнкцию

Из р сделайте вывод . ${\displaystyle (p\lor q)}$

Из q сделайте вывод . ${\displaystyle (p\lor q)}$

То есть и . ${\displaystyle p\vdash (p\lor q)}$ ${\displaystyle q\vdash (p\lor q)}$

Устранение дизъюнкции

Из и и выведите r . ${\displaystyle (p\lor q)}$ ${\displaystyle (p\to r)}$ ${\displaystyle (q\to r)}$

То есть, . ${\displaystyle \{p\lor q,p\to r,q\to r\}\vdash r}$

Двуусловное введение

Из и сделайте вывод . ${\displaystyle (p\to q)}$ ${\displaystyle (q\to p)}$ ${\displaystyle (p\leftrightarrow q)}$

То есть, . ${\displaystyle \{p\to q,q\to p\}\vdash (p\leftrightarrow q)}$

Двуусловное исключение

Из , сделайте вывод . ${\displaystyle (p\leftrightarrow q)}$ ${\displaystyle (p\to q)}$

Из , сделайте вывод . ${\displaystyle (p\leftrightarrow q)}$ ${\displaystyle (q\to p)}$

То есть и . ${\displaystyle (p\leftrightarrow q)\vdash (p\to q)}$ ${\displaystyle (p\leftrightarrow q)\vdash (q\to p)}$

Modus ponens (условное исключение)

Из p и сделайте вывод q . ${\displaystyle (p\to q)}$

То есть, . ${\displaystyle \{p,p\to q\}\vdash q}$

Условное доказательство (условное введение)

Из [принятие p позволяет доказать q ], сделайте вывод . ${\displaystyle (p\to q)}$

То есть, . ${\displaystyle (p\vdash q)\vdash (p\to q)}$

Основные и производные формы аргументов

Доказательства в исчислении высказываний

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

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

Пример доказательства в системе естественной дедукции

• Нужно показать, что A → A .
• Одно из возможных доказательств этого (которое, хотя и верное, но содержит больше шагов, чем необходимо) можно представить следующим образом:

Интерпретируйте как «Предполагая А , сделайте вывод А ». Читается как «Не предполагая ничего, сделайте вывод, что А подразумевает А », или «Это тавтология, что А подразумевает А », или «Всегда верно, что А подразумевает А ». ${\displaystyle A\vdash A}$ ${\displaystyle \vdash A\to A}$

Пример доказательства в классической системе исчисления высказываний

Теперь мы докажем ту же теорему в аксиоматической системе Яна Лукасевича , описанной выше, которая является примером дедуктивной системы в стиле Гильберта для классического исчисления высказываний. ${\displaystyle A\to A}$

Аксиомы:

(А1) ${\displaystyle (p\to (q\to p))}$

(А2) ${\displaystyle ((p\to (q\to r))\to ((p\to q)\to (p\to r)))}$

(А3) ${\displaystyle ((\neg p\to \neg q)\to (q\to p))}$

И доказательство следующее:

1. ${\displaystyle A\to ((B\to A)\to A)}$       (пример (A1))
2. ${\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}$       (пример (A2))
3. ${\displaystyle (A\to (B\to A))\to (A\to A)}$       (из (1) и (2) по modus ponens )
4. ${\displaystyle A\to (B\to A)}$       (пример (A1))
5. ${\displaystyle A\to A}$       (из (4) и (3) по modus ponens)

Обоснованность и полнота правил

Важнейшими свойствами этого набора правил является то, что они надежны и полны . Неформально это означает, что правила верны и никаких других правил не требуется. Эти утверждения можно сделать более формальными следующим образом. Доказательства правильности и полноты логики высказываний сами по себе не являются доказательствами в логике высказываний; это теоремы в ZFC , используемые в качестве метатеории для доказательства свойств логики высказываний.

Мы определяем истинностное присвоение как функцию , которая отображает пропозициональные переменные в истинное или ложное . Неформально такое присвоение истинности можно понимать как описание возможного положения дел (или возможного мира ), в котором одни утверждения истинны, а другие — нет. Семантику формул затем можно формализовать, определив, для какого «положения дел» они считаются истинными, что и делается с помощью следующего определения.

Мы определяем, когда такое истинностное присвоение A удовлетворяет некоторой корректной формуле со следующими правилами:

• A удовлетворяет пропозициональной переменной P тогда и только тогда, когда A ( P ) = true
• A удовлетворяет ¬ φ тогда и только тогда, когда A не удовлетворяет φ
• A удовлетворяет ( φ ∧ ψ ) тогда и только тогда, когда A удовлетворяет как φ , так и ψ .
• A удовлетворяет ( φ ∨ ψ ) тогда и только тогда, когда A удовлетворяет хотя бы одному из φ или ψ
• A удовлетворяет ( φ → ψ ) тогда и только тогда, когда это не тот случай, когда A удовлетворяет φ , но не удовлетворяет ψ
• A удовлетворяет ( φ ↔ ψ ) тогда и только тогда, когда A удовлетворяет обоим φ и ψ или не удовлетворяет ни одному из них.

С помощью этого определения мы теперь можем формализовать, что означает, что формула φ следует из определенного набора S формул. Неформально это верно, если во всех возможных мирах с учетом набора формул S также выполняется формула φ . Это приводит к следующему формальному определению: мы говорим, что набор S корректных формул семантически влечет за собой (или подразумевает ) некоторую корректную формулу φ , если все назначения истинности, которые удовлетворяют всем формулам в S , также удовлетворяют φ .

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

Правильность: если набор правильно составленных формул S синтаксически влечет за собой правильно составленную формулу φ , то S семантически влечет за собой φ .

Полнота: если набор правильно сформированных формул S семантически влечет за собой правильно сформированную формулу φ , то S синтаксически влечет за собой φ .

Для приведенного выше набора правил это действительно так.

Эскиз доказательства надежности

(Для большинства логических систем это сравнительно «простое» направление доказательства)

Соглашения об обозначениях: пусть G — переменная, охватывающая наборы предложений. Пусть A, B и C варьируются по предложениям. Поскольку « G синтаксически влечет за собой А », мы пишем « G доказывает А ». Поскольку « G семантически влечет за собой А », мы пишем « G подразумевает А ».

Мы хотим показать: ( A )( G ) (если G доказывает A , то G подразумевает A ).

Заметим, что « G доказывает А » имеет индуктивное определение, и это дает нам непосредственные ресурсы для демонстрации утверждений вида «Если G доказывает А , то...». Итак, наше доказательство проводится по индукции.

1. Основа. Докажите: Если A является членом G , то G подразумевает A.
2. Основа. Докажите: Если А — аксиома, то из G следует А.
3. Индуктивный шаг (индукция по n , длине доказательства):
   1. Предположим для произвольных G и A , что если G доказывает A за n или меньше шагов, то G подразумевает A.
   2. Для каждого возможного применения правила вывода на шаге n +1 , приводящего к новой теореме B , покажите, что из G следует B.

Обратите внимание, что базовый шаг II можно опустить для систем естественной дедукции , поскольку они не имеют аксиом. При использовании Шага II необходимо показать, что каждая из аксиом является (семантической) логической истиной .

Шаги «Базис » демонстрируют, что простейшие доказуемые предложения из G также подразумеваются из G для любого G. (Доказательство простое, поскольку семантический факт, что множество подразумевает любой из своих членов, также тривиален.) На индуктивном этапе будут систематически охватываться все дальнейшие предложения, которые могут быть доказуемы, — путем рассмотрения каждого случая, в котором мы можем прийти к логическому выводу. используя правило вывода, и показывает, что если новое предложение доказуемо, оно также логически подразумевается. (Например, у нас может быть правило, говорящее нам, что из « А » мы можем вывести « А» или «В ». В III.a мы предполагаем, что если А доказуемо, то оно подразумевается. Мы также знаем, что если А доказуемо, то « A или B » доказуемы. Мы должны показать, что тогда также подразумеваются « A или B ». Мы делаем это, апеллируя к семантическому определению и предположению, которое мы только что сделали. Мы предполагаем, что A доказуемо из G. Итак, это так. также подразумевается G. Таким образом, любая семантическая оценка, делающая все G истинным, делает A истинным. Но любая оценка, делающая A истинным, делает « A или B » истинным в соответствии с определенной семантикой для «или». Таким образом, любая оценка, которая делает все G истинным делает « A или B » истинным. Таким образом, подразумевается « A или B ».) Обычно индуктивный этап состоит из длительного, но простого анализа каждого конкретного случая всех правил вывода, показывающего, что каждое из них «сохраняет» семантическое значение. импликация.

По определению доказуемости, не существует никаких предложений, которые можно было бы доказать, кроме как будучи членом G , аксиомой или следуя правилу; поэтому, если все это семантически подразумевается, дедуктивный расчет верен.

Эскиз доказательства полноты

(Обычно это гораздо более сложное направление доказательства.)

Мы принимаем те же обозначения, что и выше.

Мы хотим показать: если G подразумевает A , то G доказывает A. Мы действуем путем противопоставления : вместо этого мы показываем, что если G не доказывает A , то из G не следует A. Если мы покажем, что существует модель , в которой A не выполняется, несмотря на истинность G , то, очевидно , из G не следует A. Идея состоит в том, чтобы построить такую ​​модель на основе нашего предположения, что G не доказывает A.

1. G не доказывает A. (Предположение)
2. Если G не доказывает A , то мы можем построить (бесконечное) максимальное множество G ^∗ , которое является надмножеством G и которое также не доказывает A.
   1. Упорядочите (с типом порядка ω) все предложения на языке (например, сначала самые короткие и одинаково длинные в расширенном алфавитном порядке) и пронумеруйте их ( E ₁ , E ₂ , ...)
   2. Определим серию G _n множеств ( G ₀ , G ₁ , ...) индуктивно:
      1. ${\displaystyle G_{0}=G}$
      2. Если доказывает A , то ${\displaystyle G_{k}\cup \{E_{k+1}\}}$ ${\displaystyle G_{k+1}=G_{k}}$
      3. Если не доказано A , то ${\displaystyle G_{k}\cup \{E_{k+1}\}}$ ${\displaystyle G_{k+1}=G_{k}\cup \{E_{k+1}\}}$
   3. Определим G ^∗ как объединение _всех Gn . (То есть G ^∗ — это множество всех предложений, входящих в любой _Gn . )
   4. Можно легко показать, что
      1. G ^∗ содержит (является надмножеством) G (по (bi));
      2. G ^∗ не доказывает A (поскольку доказательство будет содержать только конечное число предложений, и когда последнее из них будет введено в _{некотором Gn ,} Gn докажет A вопреки определению Gn ) ; и
      3. G ^∗ является максимальным множеством относительно A : если бы к G ^∗ были добавлены еще какие-либо предложения, это доказывалобы A. _{(Потому что, если бы} можно было добавить еще предложения, их следовало бы добавлять тогда, когда они встречались при построении Gn , опять же по определению)
3. Если G ^∗ — максимальное множество относительно A , то оно истинноподобно . Это означает, что он содержит C тогда и только тогда, когда он не содержит ¬C ; Если он содержит C и содержит «Если C, то B », то он также содержит B ; и так далее. Чтобы показать это, нужно показать, что аксиоматическая система достаточно сильна для следующего:
   • Для любых формул C и D , если доказываются и C , и ¬C , то доказывается D. Отсюда следует, что максимальное множество относительно A не может доказать одновременно C и ¬C , так как в противном случае оно доказывало бы A.
   • Для любых формул C и D , если доказано C → D и ¬C → D , то доказано D. Это используется вместе с теоремой о дедукции , чтобы показать, что для любой формулы либо она, либо ее отрицание находится в G ^∗ : Пусть B — формула, не принадлежащая G ^∗ ; тогда G ^∗ с добавлением B доказывает A. Таким образом, из теоремы о дедукции следует, что G ^∗ доказывает B → A. Но предположим, что ¬B также не было в G ^∗ , тогда по той же логике G ^∗ также доказывает, что ¬B → A ; но тогда G ^∗ доказывает A , ложность которого мы уже показали.
   • Для любых формул C и D , если доказано C и D , то доказано C → D.
   • Для любых формул C и D , если доказано C и ¬D , то доказывается ¬( C → D ).
   • Для любых формул C и D , если доказывается ¬C , то доказывается C → D.
   Если дополнительные логические операции (такие как конъюнкция и/или дизъюнкция) также являются частью словаря, то к аксиоматической системе предъявляются дополнительные требования (например, если она доказывает C и D , она также доказывает и их конъюнкцию).
4. Если G ^∗ истинноподобен, то существует G ^∗ -каноническая оценка языка: такая, которая делает каждое предложение в G ^∗ истинным, а все, что находится за пределами G ^∗, ложным, при этом подчиняясь законам семантической композиции в языке. Требование истинности необходимо для того, чтобы гарантировать, что это присвоение истинности будет удовлетворять законам семантической композиции в языке.
5. G ∗ -каноническая оценка сделает наше исходное множество G истинным, а ^A — ложным.
6. Если существует оценка, при которой G истинны , а A ложны, то G не (семантически) подразумевает A.

Таким образом, каждая система, которая имеет modus ponens в качестве правила вывода и доказывает следующие теоремы (включая их замены), является полной:

• ${\displaystyle p\to (\neg p\to q)}$
• ${\displaystyle (p\to q)\to ((\neg p\to q)\to q)}$
• ${\displaystyle p\to (q\to (p\to q))}$
• ${\displaystyle p\to (\neg q\to \neg (p\to q))}$
• ${\displaystyle \neg p\to (p\to q)}$
• ${\displaystyle p\to p}$
• ${\displaystyle p\to (q\to p)}$
• ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$

Первые пять используются для удовлетворения пяти условий этапа III выше, а последние три — для доказательства теоремы дедукции.

Пример

В качестве примера можно показать, что, как и любая другая тавтология, три аксиомы классической системы исчисления высказываний, описанной ранее, могут быть доказаны в любой системе, которая удовлетворяет вышесказанному, а именно, которая имеет modus ponens в качестве правила вывода и доказывает вышеизложенное. восемь теорем (включая их замены). Из восьми теорем последние две являются двумя из трех аксиом; третья аксиома также может быть доказана, как мы сейчас покажем. ${\displaystyle (\neg q\to \neg p)\to (p\to q)}$

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

1. ${\displaystyle q\to (p\to q)}$       (пример 7-й теоремы)
2. ${\displaystyle (q\to (p\to q))\to ((\neg q\to \neg p)\to (q\to (p\to q)))}$       (пример 7-й теоремы)
3. ${\displaystyle (\neg q\to \neg p)\to (q\to (p\to q))}$       (из (1) и (2) по modus ponens)
4. ${\displaystyle (\neg p\to (p\to q))\to ((\neg q\to \neg p)\to (\neg q\to (p\to q)))}$       (пример теоремы о гипотетическом силлогизме)
5. ${\displaystyle (\neg p\to (p\to q))}$       (пример 5-й теоремы)
6. ${\displaystyle (\neg q\to \neg p)\to (\neg q\to (p\to q))}$       (из (5) и (4) по modus ponens)
7. ${\displaystyle (q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))}$       (пример 2-й теоремы)
8. ${\displaystyle ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q)))\to ((\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))))}$       (пример 7-й теоремы)
9. ${\displaystyle (\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q)))}$       (из (7) и (8) по modus ponens)
10. ${\displaystyle ((\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))))\to }$

    ${\displaystyle (((\neg q\to \neg p)\to (q\to (p\to q)))\to ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q))))}$       (пример 8-й теоремы)

11. ${\displaystyle ((\neg q\to \neg p)\to (q\to (p\to q)))\to ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q)))}$       (из (9) и (10) по modus ponens)
12. ${\displaystyle (\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q))}$       (из (3) и (11) по modus ponens)
13. ${\displaystyle ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q)))\to (((\neg q\to \neg p)\to (\neg q\to (p\to q)))\to ((\neg q\to \neg p)\to (p\to q)))}$       (пример 8-й теоремы)
14. ${\displaystyle ((\neg q\to \neg p)\to (\neg q\to (p\to q)))\to ((\neg q\to \neg p)\to (p\to q))}$       (из (12) и (13) по modus ponens)
15. ${\displaystyle (\neg q\to \neg p)\to (p\to q)}$       (из (6) и (14) по modus ponens)

Проверка полноты классической системы исчисления высказываний

Теперь мы проверим, что классическая система исчисления высказываний, описанная ранее, действительно может доказать необходимые восемь упомянутых выше теорем. Мы используем несколько доказанных здесь лемм :

(DN1) - Двойное отрицание (одно направление) ${\displaystyle \neg \neg p\to p}$

(DN2) — Двойное отрицание (другое направление) ${\displaystyle p\to \neg \neg p}$

(HS1) - одна из форм Гипотетического силлогизма. ${\displaystyle (q\to r)\to ((p\to q)\to (p\to r))}$

(HS2) - другая форма гипотетического силлогизма. ${\displaystyle (p\to q)\to ((q\to r)\to (p\to r))}$

(TR1) — Транспонирование ${\displaystyle (p\to q)\to (\neg q\to \neg p)}$

(TR2) – другая форма транспозиции. ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$

(Л1) ${\displaystyle p\to ((p\to q)\to q)}$

(Л3) ${\displaystyle (\neg p\to p)\to p}$

Мы также используем метод метатеоремы гипотетического силлогизма как сокращение для нескольких шагов доказательства.

• ${\displaystyle p\to (\neg p\to q)}$- доказательство:
  1. ${\displaystyle p\to (\neg q\to p)}$       (пример (A1))
  2. ${\displaystyle (\neg q\to p)\to (\neg p\to \neg \neg q)}$       (экземпляр (TR1))
  3. ${\displaystyle p\to (\neg p\to \neg \neg q)}$       (из (1) и (2) с использованием метатеоремы гипотетического силлогизма)
  4. ${\displaystyle \neg \neg q\to q}$       (экземпляр (DN1))
  5. ${\displaystyle (\neg \neg q\to q)\to ((\neg p\to \neg \neg q)\to (\neg p\to q))}$       (пример (HS1))
  6. ${\displaystyle (\neg p\to \neg \neg q)\to (\neg p\to q)}$       (из (4) и (5) с использованием modus ponens)
  7. ${\displaystyle p\to (\neg p\to q)}$       (из (3) и (6) с использованием метатеоремы гипотетического силлогизма)
• ${\displaystyle (p\to q)\to ((\neg p\to q)\to q)}$- доказательство:
  1. ${\displaystyle (p\to q)\to ((\neg q\to p)\to (\neg q\to q))}$       (пример (HS1))
  2. ${\displaystyle (\neg q\to q)\to q}$       (пример (L3))
  3. ${\displaystyle ((\neg q\to q)\to q)\to (((\neg q\to p)\to (\neg q\to q))\to ((\neg q\to p)\to q))}$       (пример (HS1))
  4. ${\displaystyle ((\neg q\to p)\to (\neg q\to q))\to ((\neg q\to p)\to q)}$       (из (2) и (3) по modus ponens)
  5. ${\displaystyle (p\to q)\to ((\neg q\to p)\to q)}$       (из (1) и (4) с использованием метатеоремы гипотетического силлогизма)
  6. ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$       (пример (TR2))
  7. ${\displaystyle ((\neg p\to q)\to (\neg q\to p))\to (((\neg q\to p)\to q)\to ((\neg p\to q)\to q))}$       (пример (HS2))
  8. ${\displaystyle ((\neg q\to p)\to q)\to ((\neg p\to q)\to q)}$       (из (6) и (7) с использованием modus ponens)
  9. ${\displaystyle (p\to q)\to ((\neg p\to q)\to q)}$       (из (5) и (8) с использованием метатеоремы гипотетического силлогизма)
• ${\displaystyle p\to (q\to (p\to q))}$- доказательство:
  1. ${\displaystyle q\to (p\to q)}$       (пример (A1))
  2. ${\displaystyle (q\to (p\to q))\to (p\to (q\to (p\to q)))}$       (пример (A1))
  3. ${\displaystyle p\to (q\to (p\to q))}$       (из (1) и (2) с использованием modus ponens)
• ${\displaystyle p\to (\neg q\to \neg (p\to q))}$- доказательство:
  1. ${\displaystyle p\to ((p\to q)\to q)}$       (пример (L1))
  2. ${\displaystyle ((p\to q)\to q)\to (\neg q\to \neg (p\to q))}$       (экземпляр (TR1))
  3. ${\displaystyle p\to (\neg q\to \neg (p\to q))}$       (из (1) и (2) с использованием метатеоремы гипотетического силлогизма)
• ${\displaystyle \neg p\to (p\to q)}$- доказательство:
  1. ${\displaystyle \neg p\to (\neg q\to \neg p)}$       (пример (A1))
  2. ${\displaystyle (\neg q\to \neg p)\to (p\to q)}$       (пример (A3))
  3. ${\displaystyle \neg p\to (p\to q)}$       (из (1) и (2) с использованием метатеоремы гипотетического силлогизма)
• ${\displaystyle p\to p}$- доказательство, приведенное в примере доказательства выше
• ${\displaystyle p\to (q\to p)}$- аксиома (А1)
• ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$- аксиома (А2)

Еще один план доказательства полноты

Если формула является тавтологией , то для нее существует таблица истинности , которая показывает, что каждая оценка дает истинное значение для формулы. Рассмотрим такую ​​оценку. С помощью математической индукции по длине подформул покажите, что истинность или ложность подформулы следует из истинности или ложности (в зависимости от оценки) каждой пропозициональной переменной в подформуле. Затем объедините строки таблицы истинности вместе по две, используя «( P истинно, подразумевает S ) подразумевает (( P ложно, подразумевает S ) подразумевает S )». Продолжайте повторять это до тех пор, пока не будут устранены все зависимости от пропозициональных переменных. В результате мы доказали данную тавтологию. Поскольку любая тавтология доказуема, логика полна.

Интерпретация функционального исчисления высказываний

Интерпретация истинностно-функционального исчисления высказываний представляет собой присвоение каждому пропозициональному символу того или иного (но не обоих) истинностных значений истины ( T ) и ложности ( F ), а также присвоение связующим символам их обычные истинностно-функциональные значения. Интерпретацию функционального исчисления высказываний можно также выразить в терминах таблиц истинности . ^[14] ${\displaystyle {\mathcal {P}}}$ ${\displaystyle {\mathcal {P}}}$ ${\displaystyle {\mathcal {P}}}$

Для различных пропозициональных символов существуют различные возможные интерпретации. Например, для любого конкретного символа возможны интерпретации: ${\displaystyle n}$ ${\displaystyle 2^{n}}$ ${\displaystyle a}$ ${\displaystyle 2^{1}=2}$

1. ${\displaystyle a}$присваивается T , или
2. ${\displaystyle a}$присвоено Ф. _

Для пары возможны интерпретации: ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle 2^{2}=4}$

1. обоим присвоено T ,
2. обоим присвоено F ,
3. ${\displaystyle a}$присвоено T и присвоено F , или ${\displaystyle b}$
4. ${\displaystyle a}$назначается F и назначается T . ^[14] ${\displaystyle b}$

Поскольку имеет , то есть счетное множество пропозициональных символов, существует и, следовательно , бесчисленное множество различных возможных интерпретаций . ^[14] ${\displaystyle {\mathcal {P}}}$ ${\displaystyle \aleph _{0}}$ ${\displaystyle 2^{\aleph _{0}}={\mathfrak {c}}}$ ${\displaystyle {\mathcal {P}}}$

Интерпретация предложения истинно-функциональной пропозициональной логики

Если φ и ψ являются формулами и интерпретацией , то применяются следующие определения: ${\displaystyle {\mathcal {P}}}$ ${\displaystyle {\mathcal {I}}}$ ${\displaystyle {\mathcal {P}}}$

• Предложение пропозициональной логики истинно при интерпретации, если этому предложению присваивается значение истинности T. Если предложение истинно в соответствии с интерпретацией, то эта интерпретация называется моделью этого предложения. ${\displaystyle {\mathcal {I}}}$ ${\displaystyle {\mathcal {I}}}$
• φ ложно при интерпретации, если φ не истинно при . ^[14] ${\displaystyle {\mathcal {I}}}$ ${\displaystyle {\mathcal {I}}}$
• Предложение логики высказываний логически значимо, если оно истинно при любой интерпретации.

  ${\displaystyle \models }$ φ означает, что φ логически допустим.

• Предложение ψ логики высказываний является семантическим следствием предложения φ , если не существует интерпретации, при которой φ истинно, а ψ ложно.
• Предложение логики высказываний является непротиворечивым , если оно истинно хотя бы при одной интерпретации. Оно непоследовательно, если оно непоследовательно.

Некоторые следствия этих определений:

• Для любой данной интерпретации данная формула либо истинна, либо ложна. ^[14]
• Ни одна формула не является одновременно истинной и ложной при одной и той же интерпретации. ^[14]
• φ ложна для данной интерпретации тогда и только тогда, когда истинно для этой интерпретации; и φ истинно в соответствии с интерпретацией тогда и только тогда, когда ложно в соответствии с этой интерпретацией. ^[14] ${\displaystyle \neg \phi }$ ${\displaystyle \neg \phi }$
• Если φ и оба верны при данной интерпретации, то ψ истинно при этой интерпретации. ^[14] ${\displaystyle (\phi \to \psi )}$
• Если и , то . ^[14] ${\displaystyle \models _{\mathrm {P} }\phi }$ ${\displaystyle \models _{\mathrm {P} }(\phi \to \psi )}$ ${\displaystyle \models _{\mathrm {P} }\psi }$
• ${\displaystyle \neg \phi }$верно при условии, что φ неверно при . ${\displaystyle {\mathcal {I}}}$ ${\displaystyle {\mathcal {I}}}$
• ${\displaystyle (\phi \to \psi )}$истинно при условии, если либо φ неверно при , либо ψ истинно при . ^[14] ${\displaystyle {\mathcal {I}}}$ ${\displaystyle {\mathcal {I}}}$ ${\displaystyle {\mathcal {I}}}$
• Предложение ψ логики высказываний является семантическим следствием предложения φ тогда и только тогда , когда оно логически значимо , то есть тогда и только тогда . ^[14] ${\displaystyle (\phi \to \psi )}$ ${\displaystyle \phi \models _{\mathrm {P} }\psi }$ ${\displaystyle \models _{\mathrm {P} }(\phi \to \psi )}$

Альтернативное исчисление

Можно определить другую версию исчисления высказываний, которая определяет большую часть синтаксиса логических операторов посредством аксиом и использует только одно правило вывода.

Аксиомы

Пусть φ , χ и ψ обозначают корректные формулы. (Сами правильно составленные формулы не будут содержать греческих букв, а будут содержать только заглавные латинские буквы, соединительные операторы и круглые скобки.) Тогда аксиомы будут следующими:

• Аксиому THEN-2 можно рассматривать как «распределительное свойство импликации относительно импликации».
• Аксиомы И-1 и И-2 соответствуют «устранению соединения». Отношение между AND-1 и AND-2 отражает коммутативность оператора конъюнкции.
• Аксиома AND-3 соответствует «введению союза».
• Аксиомы ОР-1 и ОР-2 соответствуют «введению дизъюнкции». Связь между OR-1 и OR-2 отражает коммутативность оператора дизъюнкции.
• Аксиома НЕ-1 соответствует «доведению до абсурда».
• Аксиома НЕ-2 гласит, что «из противоречия можно вывести все».
• Аксиома НЕ-3 называется « tertium non-datur » ( лат . «третье не дано») и отражает семантическую оценку пропозициональных формул: формула может иметь истинностное значение либо истинное, либо ложное. Третьего истинностного значения не существует, по крайней мере, в классической логике. Логики-интуиционисты не принимают аксиому НЕ-3 .

Правило вывода

Правило вывода — modus ponens :

${\displaystyle {\frac {\phi ,\ \phi \to \chi }{\chi }}}$.

Правило мета-вывода

Пусть демонстрация представлена ​​последовательностью, в которой гипотезы располагаются слева от турникета , а выводы — справа от турникета. Тогда теорему о дедукции можно сформулировать следующим образом:

Если последовательность

${\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi }$

было продемонстрировано, то можно также продемонстрировать последовательность

${\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \to \psi }$.

Эта теорема о дедукции (DT) сама по себе не сформулирована с помощью исчисления высказываний: это не теорема исчисления высказываний, а теорема об исчислении высказываний. В этом смысле это метатеорема , сравнимая с теоремами о правильности или полноте исчисления высказываний.

С другой стороны, DT настолько полезен для упрощения процесса синтаксического доказательства, что его можно рассматривать и использовать как еще одно правило вывода, сопровождающее modus ponens. В этом смысле DT соответствует естественному правилу вывода условного доказательства , которое является частью первой версии исчисления высказываний, представленной в этой статье.

Обратное DT также справедливо:

Если последовательность

${\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \to \psi }$

было продемонстрировано, то можно также продемонстрировать последовательность

${\displaystyle \phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi }$

на самом деле, справедливость обратного DT почти тривиальна по сравнению с DT:

Если

${\displaystyle \phi _{1},\ ...,\ \phi _{n}\vdash \chi \to \psi }$

затем

1: ${\displaystyle \phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi \to \psi }$

2: ${\displaystyle \phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi }$

и из (1) и (2) можно вывести

3: ${\displaystyle \phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \psi }$

посредством modus ponens, QED

Обратное DT имеет важные последствия: его можно использовать для преобразования аксиомы в правило вывода. Например, по аксиоме И-1 имеем:

${\displaystyle \vdash \phi \wedge \chi \to \phi ,}$

которое можно преобразовать с помощью обращения теоремы дедукции в

${\displaystyle \phi \wedge \chi \vdash \phi ,}$

что говорит нам о том, что правило вывода

${\displaystyle {\frac {\phi \wedge \chi }{\phi }}}$

допустимо . _ Это правило вывода — исключение конъюнкции , одно из десяти правил вывода, использованных в первой версии (в этой статье) исчисления высказываний.

Пример доказательства

Ниже приведен пример (синтаксической) демонстрации, включающий только аксиомы THEN-1 и THEN-2 :

Докажите: (Рефлексивность импликации). ${\displaystyle A\to A}$

Доказательство:

1. ${\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}$

   Аксиома ТОГДА-2 с ${\displaystyle \phi =A,\chi =B\to A,\psi =A}$

2. ${\displaystyle A\to ((B\to A)\to A)}$

   Аксиома ТОГДА-1 с ${\displaystyle \phi =A,\chi =B\to A}$

3. ${\displaystyle (A\to (B\to A))\to (A\to A)}$

   Из (1) и (2) по modus ponens.

4. ${\displaystyle A\to (B\to A)}$

   Аксиома ТОГДА-1 с ${\displaystyle \phi =A,\chi =B}$

5. ${\displaystyle A\to A}$

   Из (3) и (4) по modus ponens.

Эквивалентность эквациональной логике

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

Классическое исчисление высказываний, описанное выше, эквивалентно булевой алгебре , тогда как интуиционистское исчисление высказываний эквивалентно алгебре Гейтинга . Эквивалентность доказывается переносом в каждую сторону теорем соответствующих систем. Теоремы классического или интуиционистского исчисления высказываний переводятся как уравнения булевой или гейтинговой алгебры соответственно. И наоборот, теоремы булевой или гейтинговой алгебры переводятся как теоремы классического или интуиционистского исчисления соответственно, что является стандартным сокращением. В случае булевой алгебры также можно перевести как , но этот перевод интуиционистски неверен. ${\displaystyle \phi }$ ${\displaystyle \phi =1}$ ${\displaystyle x=y}$ ${\displaystyle (x\to y)\land (y\to x)}$ ${\displaystyle x\equiv y}$ ${\displaystyle x=y}$ ${\displaystyle (x\land y)\lor (\neg x\land \neg y)}$

И в булевой, и в алгебре Гейтинга вместо равенства может использоваться неравенство. Равенство выражается парой неравенств и . Обратно, неравенство выражается как равенство , или как . Значение неравенства для систем гильбертовского стиля состоит в том, что оно соответствует последнему символу вывода или следования . Следствие ${\displaystyle x\leq y}$ ${\displaystyle x=y}$ ${\displaystyle x\leq y}$ ${\displaystyle y\leq x}$ ${\displaystyle x\leq y}$ ${\displaystyle x\land y=x}$ ${\displaystyle x\lor y=y}$ ${\displaystyle \vdash }$

${\displaystyle \phi _{1},\ \phi _{2},\ \dots ,\ \phi _{n}\vdash \psi }$

в версии алгебраической модели с неравенством переводится как

${\displaystyle \phi _{1}\ \land \ \phi _{2}\ \land \ \dots \ \land \ \phi _{n}\ \ \leq \ \ \psi }$

Обратно, алгебраическое неравенство переводится как следствие ${\displaystyle x\leq y}$

${\displaystyle x\ \vdash \ y}$.

Разница между импликацией и неравенством или следствием заключается в том, что первое является внутренним по отношению к логике, а второе — внешним. Внутренняя импликация между двумя терминами — это еще один термин того же типа. Следствие как внешняя импликация между двумя терминами выражает метаистину вне языка логики и считается частью метаязыка . Даже если изучаемая логика является интуиционистской, следование обычно понимается классически как двузначное: либо левая часть влечет за собой правую сторону, либо меньше или равна ей, либо нет. ${\displaystyle x\to y}$ ${\displaystyle x\leq y}$ ${\displaystyle x\ \vdash \ y}$

Аналогичные, но более сложные переводы в алгебраическую логику и обратно возможны для систем естественной дедукции, описанных выше, и для секвенциального исчисления . Следствия последнего можно интерпретировать как двузначные, но более проницательная интерпретация - это набор, элементы которого можно понимать как абстрактные доказательства, организованные как морфизмы категории . В этой интерпретации правило сечения секвенциального исчисления соответствует композиции в категории. Булевы алгебры и алгебры Гейтинга входят в эту картину как специальные категории, имеющие не более одного морфизма на каждое гомомножество, т. е. одно доказательство на каждое следствие, что соответствует идее о том, что существование доказательств — это все, что имеет значение: подойдет любое доказательство, и нет смысла их различать. .

Графические исчисления

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

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

Другие логические вычисления

Исчисление высказываний — это простейший вид логического исчисления, используемый в настоящее время. Его можно расширить несколькими способами. ( Аристотелевское «силлогистическое» исчисление , которое в значительной степени вытеснено современной логикой, в некоторых отношениях проще, но в других отношениях более сложно, чем исчисление высказываний.) Самый непосредственный способ разработать более сложное логическое исчисление — это ввести правила, которые чувствительны к более мелким деталям используемых предложений.

Логика первого порядка (также известная как логика предикатов первого порядка) возникает, когда «атомарные предложения» логики высказываний разбиваются на термины , переменные , предикаты и кванторы , причем все они сохраняют правила логики высказываний с добавлением некоторых новых. (Например, из «Все собаки — млекопитающие» мы можем сделать вывод: «Если Ровер — собака, то Ровер — млекопитающее».) С помощью инструментов логики первого порядка можно сформулировать ряд теорий либо с явными аксиомами, либо с явными аксиомами. или правилами вывода, которые сами по себе можно рассматривать как логические исчисления. Арифметика — самая известная из них; другие включают теорию множеств и мереологию . Логика второго порядка и другие логики более высокого порядка являются формальными расширениями логики первого порядка. Таким образом, имеет смысл называть логику высказываний «логикой нулевого порядка» при сравнении ее с этими логиками.

Модальная логика также предлагает множество выводов, которые невозможно уловить с помощью исчисления высказываний. Например, из «Обязательно p » мы можем сделать вывод, что p . Из p мы можем сделать вывод: «Возможно, что p ». Перевод между модальными логиками и алгебраическими логиками касается классической и интуиционистской логики, но с введением унарного оператора на булевых или гейтинговых алгебрах, отличного от булевых операций, интерпретирующего модальность возможности, а в случае алгебры Гейтинга - второго оператора, интерпретирующего необходимость. (для булевой алгебры это избыточно, поскольку необходимость есть двойственная возможность по Де Моргану). Первый оператор сохраняет 0 и дизъюнкцию, а второй сохраняет 1 и конъюнкцию.

Многозначные логики — это те, которые позволяют предложениям иметь значения, отличные от true и false . (Например, ни то , ни другое не является стандартными «дополнительными значениями»; «континуальная логика» позволяет каждому предложению иметь любую из бесконечного числа «степеней истинности» между истиной и ложью .) Эта логика часто требует вычислительных устройств, совершенно отличных от пропозициональных. исчисление. Когда значения образуют булеву алгебру (которая может иметь более двух или даже бесконечное количество значений), многозначная логика сводится к классической логике; Таким образом, многозначные логики представляют независимый интерес только тогда, когда значения образуют алгебру, которая не является булевой.

Решатели

Одно заметное различие между исчислением высказываний и исчислением предикатов состоит в том, что выполнимость формулы высказываний разрешима . ^[15] Определение выполнимости формул пропозициональной логики является NP-полной проблемой. Однако существуют практические методы (например, алгоритм DPLL , 1962; алгоритм Чаффа , 2001), которые очень быстры для многих полезных случаев. Недавняя работа расширила алгоритмы решателя SAT для работы с предложениями, содержащими арифметические выражения ; это решатели SMT .

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

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

Высшие логические уровни

• Логика первого порядка
• Пропозициональная логика второго порядка
• Логика второго порядка
• Логика высшего порядка

похожие темы

• Булева алгебра (логика)
• Булева алгебра (структура)
• Темы булевой алгебры
• Логический домен
• Булева функция
• Логическая функция
• Категорическая логика
• Комбинационная логика
• Комбинаторная логика
• Концептуальный график
• Дизъюнктивный силлогизм
• Существенный граф
• Эквациональная логика
• Экзистенциальный граф
• Исчисление высказываний Фреге
• Импликативное исчисление высказываний
• Интуиционистское исчисление высказываний
• Жан Буридан
• Законы формы
• Список логических символов
• Логический график
• Логическое НО
• Логическое значение
• Математическая логика
• Операция (математика)
• Павел Венецианский
• Закон Пирса
• Петр Испанский (автор)
• Пропозициональная формула
• Симметричная разница
• Тавтология (правило вывода)
• Функция истины
• Таблица истинности
• Уолтер Берли
• Уильям Шервудский

Примечания

1. Формально правило 2 получает формулы в польской записи , то есть в этом примере. Для удобства в этом и всех последующих примерах мы будем использовать общепринятую инфиксную запись . ${\displaystyle \lor \neg pq}$

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

1. "Пропозициональная логика | Блестящая математическая и научная вики" . блестящий.орг . Проверено 20 августа 2020 г.
2. Бобзиен, Сюзанна (1 января 2016 г.). «Древняя логика». В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии. Лаборатория метафизических исследований, Стэнфордский университет – через Стэнфордскую энциклопедию философии.
3. "Пропозициональная логика | Интернет-энциклопедия философии" . Проверено 20 августа 2020 г.
4. Маренбон, Джон (2007). Средневековая философия: историко-философское введение . Рутледж. п. 137.
5. Пекхаус, Волкер (1 января 2014 г.). «Влияние Лейбница на логику XIX века». В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии. Лаборатория метафизических исследований, Стэнфордский университет – через Стэнфордскую энциклопедию философии.
6. Херли, Патрик (2007). Краткое введение в логику, 10-е издание . Издательство Уодсворт. п. 392.
7. Бет, Эверт В.; «Семантическое следствие и формальная выводимость», серия: Mededlingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, Nieuwe Reeks, vol. 18, нет. 13, Северо-Голландский Уитг. Mij., Амстердам, 1955, стр. 309–42. Перепечатано в журнале Яакко Интикка (редактор) «Философия математики» , Oxford University Press, 1969 г.
8. Правда в Фреге
9. «Рассел: журнал исследований Бертрана Рассела».
10. Анеллис, Ирвинг Х. (2012). «Функциональный анализ истины Пирса и происхождение таблицы истинности». История и философия логики . 33 : 87–97. дои : 10.1080/01445340.2011.621702. S2CID  170654885.
11. Верник, Уильям (1942) «Полные наборы логических функций», Труды Американского математического общества 51 , стр. 117–132.
12. Мы используем для обозначения эквивалентности и , то есть как сокращение для и . ${\displaystyle \phi \dashv \vdash \psi }$ ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \phi \vdash \psi }$ ${\displaystyle \psi \vdash \phi }$
13. Тоида, Шуничи (2 августа 2009 г.). «Доказательство последствий». CS381 Материалы веб-курса «Дискретные структуры/Дискретная математика» . Кафедра компьютерных наук Университета Олд Доминион . Проверено 10 марта 2010 г.
14. Хантер, Джеффри (1971). Металогика: введение в метатеорию стандартной логики первого порядка . Издательство Калифорнийского университета. ISBN 0-520-02356-0.
15. WVO Quine, Математическая логика (1980), стр.81. Издательство Гарвардского университета, 0-674-55451-5

дальнейшее чтение

• Браун, Фрэнк Маркхэм (2003), Булево рассуждение: логика булевых уравнений , 1-е издание, Kluwer Academic Publishers, Норвелл, Массачусетс. 2-е издание, Dover Publications, Минеола, Нью-Йорк.
• Чанг, CC и Кейслер, HJ (1973), Теория моделей , Северная Голландия, Амстердам, Нидерланды.
• Кохави, Цви (1978), Теория коммутации и конечных автоматов , 1-е издание, McGraw-Hill, 1970. 2-е издание, McGraw-Hill, 1978.
• Корфхаге, Роберт Р. (1974), Дискретные вычислительные структуры , Academic Press, Нью-Йорк, Нью-Йорк.
• Ламбек Дж. и Скотт П.Дж. (1986), Введение в категориальную логику высшего порядка , издательство Кембриджского университета, Кембридж, Великобритания.
• Мендельсон, Эллиот (1964), Введение в математическую логику , Компания Д. Ван Ностранда.

Сопутствующие работы

• Хофштадтер, Дуглас (1979). Гёдель, Эшер, Бах: Вечная золотая коса . Основные книги . ISBN 978-0-465-02656-2.

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

• Клемент, Кевин К. (2006), «Логика высказываний», Джеймс Физер и Брэдли Дауден (ред.), Интернет-энциклопедия философии , Eprint.
• Формальное исчисление предикатов содержит систематическое формальное развитие в духе альтернативного исчисления.
• forall x: введение в формальную логику П.Д. Магнуса охватывает формальную семантику и теорию доказательств для логики предложений.
• Глава 2 / Пропозициональная логика из «Логики в действии»
• Доказательство секвенциального исчисления высказываний в рамках проекта «Наюки». ( примечание : импликация может быть введена в форму !X|Y, а секвенция может представлять собой одну формулу с префиксом запятых >и без запятых)
• Пропозициональная логика — порождающая грамматика