<<
>>

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

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

Неформализованными остались только понятия логического следования и логически истинной формулы. В ЛВ как исчислении эти понятия заменяются своими синтаксическими двойниками - понятием вывода и доказуемой формулы (теоремы исчисления) соответственно.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

о том, всякая ли логически истин­ная формула ЛВ является доказуемой в исчислении ЛВ. Иными словами, можно ли множество правил построения деревьев формул П1 - П15 счи­тать полным? Если это множество полно, тогда их применение должно гарантировать, что всякая логически истинная формула ЛВ доказуема и, наоборот, что всякая доказуемая формула ЛВ логически истинна.

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

Теорема 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.

<< | >>
Источник: Логика: учеб. пособие / В.А. Светлов. - М.,2012. - 432 с.. 2012

Еще по теме Логика высказываний как исчисление:

  1. 1.3.Автоматический поиск вывода в натуральном исчислении
  2. Как самостоятельная наука логика сложилась более двух тысяч лет назад, в IV в. до н.э.
  3. Асмус Валентин Фердинандович. Лекции по истории логики: Авиценна, Бэкон, Гоббс, Декарт, Паскаль / Под ред. и со вступ, ст. Б. В. Бирюкова. Изд. стереотип. M.: Издательство ЛКИ,2017. — 238 с. (Из истории логики XX века.), 2017
  4. Деконструкция логики - логика деконструкции?
  5. §3. О трансцендентальной логике
  6. §5. Проблема обоснования логики в философии Канта
  7. 1. ПРЕДМЕТ И ЗНАЧЕНИЕ ЛОГИКИ В СИСТЕМЕ НАУЧНОГО ЗНАНИЯ
  8. Источник генезиса логики
  9. Логика: учеб. пособие / В.А. Светлов. - М.,2012. - 432 с., 2012
  10. 2. ОСНОВНЫЕ ИСТОРИЧЕСКИЕ ЭТАПЫ РАЗВИТИЯ ЛОГИКИ
  11. В.К. Астафьев. ЗАКОНЫ МЫШЛЕНИЯ В ФОРМАЛЬНОЙ И ДИАЛЕНТИЧЕСКОЙ ЛОГИКЕ. ИЗДАТЕЛЬСТВО ЛЬВОВСКОГО УНИВЕРСИТЕТА - 1968, 1968
  12. §2. Об общей (формальной) логике