Логика высказываний как исчисление

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

Для ЛВ были построены исчисления разного типа - аксиоматичес­кие, натуральные, генценовские. Ниже конструируется исчисление ново­го вида, основанное на методе деревьев, техника которого объяснялась в предшествующих подразделах.

Алфавит ЛВ и правила построения формул ЛВ были указаны ранее. Сформулируем правила прямого и косвенного вывода.

Правила прямого и косвенного вывода

1. Если каждая ветвь дерева формулы φ является конъюнктом ка­кой-либо ветви дерева формул ф₁, ф₂,..., ф_п (включая случай полно­го совпадения ветвей), тогда формула φ прямо выводима из после­довательности формул ф₁, ф₂,..., ф_п.

2. Если каждая ветвь дерева формулы (ф₁, ф₂,..., ф_п&φ) замкну­та, тогда формула φ косвенно выводима из последовательности ^форму^{л ф}1, ^ф₂^,_, ^ф_п.

Вывод произвольной формулы φ из последовательности формул ф₁, ф₂,..., ф_п принято обозначать посредством специальной символизации

которая читается так: «Из допущений ф₁, ф₂,..., ф_п выводима формула ф». Если формула φ представляет собой логическую истину, то это символи­зируется посредством

и читается: «ф - теорема (доказуемая формула)».

Пусть α и β, как и прежде, обозначают посылки и заключение дока­зательства.

• Доказательством заключения β в исчислении ЛВ называется вывод β из множества посылок α.

• Доказательство заключения β считается прямым, если построен прямой вывод β из множества посы­лок α; и косвенным (от противного), если построен косвенный вывод β из множества посылок α

Ветвь BDдерева заключения полностью совпадает с четвертой слева ветвью дерева посылок, а ветви с формуламидерева заключе­

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

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

третьяветви дерева заключения и тем самым заключение в целом. Допустим, истинна вторая ветвь дерева посылок. Тогда истин­

ным является конъюнкти тем самым заключение в целом. Допус­тим, истинна третья ветвь дерева посылокТогда конъюнкт -

С и тем самым заключение в целом также являются истинными. Теперь

предположим, что истинна четвертая ветвь (В &D).Тогда антецедент за­ключения ложен, а доказательство тем не менее истинно.

Косвенное доказательство

Проверим, совместимы ли посылки рассматриваемого доказательс­тва с отрицанием заключения. С этой целью необходимо построить де-

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

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

Косвенное доказательство

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

Дерево заключения:

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

Косвенное доказательство

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

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

Справедливость данного утверждения доказывают следующие две теоремы.

Теорема 4.Если с помощью правил конструирования деревьев П1 - П14 можно построить замкнутое дерево формулы (α &-β), тогда вы­вод заключения β из посылок α является общезначимым.

Доказательство. Допустим, вывод заключения β из посылок α не общезначим и тем самым дерево формулы (α &-β) не замкнуто. Тогда существует по крайней мере одна ветвь, атомарные подформулы и/или их отрицания которой не противоречат друг другу и одновременно истинны. Так как ветвь не замкнута, а ее замыкание необходимо для доказательс­тва выводимости, она может быть далее продолжена с помощью правил конструирования деревьев П1 - П15. Но каждое из них основано на оп­ределенном законе логики - принципе сохранения истины и по опреде­лению не может привести к замыканию ветви. Например, если выполня­ется конъюнкция (A &B),то она продолжается формулами А и В, каждая из которых также выполняется. Если выполняется дизъюнкция (Aѵ B), то она продолжается формулами А или В, из которых по крайней мере одна истинна. Все остальные формулы сводимы по своим структурным свойствам к конъюнкции и дизъюнкции. Следовательно, если ветвь не замкнута, то ни одно из указанных правил никогда не сделает ее замкну­той. Значит, если все ветви дерева формулы (α &-β) замкнуты, тогда не существует ни одной ветви, в которой посылки α были бы истинны, а заключение β ложно. Следовательно, вывод любой тавтологии ЛВ с по­мощью правил П1 - П15 всегда общезначим. QED.

Теорема 5.Если с помощью правил П1 - П14 можно построить неза­мкнутое дерево формулы (α &-β), тогда вывод заключения β из посылок α не общезначим.

Доказательство. Если вывод заключения β из посылок α общезна­чим, тогда, согласно теореме 4, дерево формулы (α &-β), построенное в соответствии с правилами П1 - П15, замкнуто. Не существует ни одной ветви дерева, в которой были бы одновременно истинны множества фор­мул α и -β. Следовательно, если дерево формулы (α &-β) не замкну­то, тогда вывод заключения β из посылок α не является общезначимым. QED.

Теоремы 4 и 5 вместе говорят о необходимости и достаточности пра­вил П1 - П15 для вывода тавтологий ЛВ. Значит, множество этих правил является полным и с их помощью доказуема любая тавтология ЛВ.

6.10.