Выдержка из текста работы
Аксиоматическое построение логики высказываний состоит в том, чтобы попытаться вычленить из бесконечного числа истинных клауз независимую систему аксиом, с помощью которой можно было бы установить справедливость любых других клауз.
Клауза — это элементарное предложение, в котором использовано отношение порядка, оформленное через символ импликации « => ». (Если А, то В (Если у человека температура 40 градусов, то он болен ))
Отношение порядка удовлетворяет трем законам:
рефлексивности: А=>А (Если у человека температура 40 градусов, значит у него температура 40 градусов.)
антисимметричности: Если А=>В, то неверно, что В=>А (Если у человека температура 40 градусов, то он болен. И неверно, что если человек болен, то у него температура 40 градусов. (Может, у него 37.))
транзитивности: если А=>В и В=>С, то А=>С. (Если у человека температура 40 градусов, то он болен. Если человек болен, то ему нужно лечение. Выходит: если у человека температура 40 градусов, то ему нужно лечение.)
Берутся некоторые клаузы и рассматриваются как высказывания, истинность которых дана заранее. При этом не обязательно, что эти высказывания будут очевидны сами по себе. Важно, чтобы они были удобны для получения вывода. Могут быть выбраны в качестве аксиоматических различные высказывания. Число их так же может быть разным. Большее число аксиом иногда облегчает процесс получения вывода.
За аксиомы примем:
- А=>(В=>А)
- (А=>(В=>С)) =>((А=>В)=>(А=>С))
- (А&В) =>А
- (А&В) =>В
- A =>(B=>(А&B))
- А=>(АилиB)
- B=>(АилиB)
- (A=>C) =>(B=>C) =>((AилиB)=>C)
- (неА=>неВ) =>((неА=>В) =>А)
Обозначим А и В не отдельные высказывания, которые обозначались а и b, а целые формулы логики высказываний. Например, те, которые выше были приведены в качестве аксиомы. С помощью этих символов можно сформулировать правила вывода:
- а) Правило подстановки. Вместо А (переменного высказывания) везде, где эта буква встречается, можно подставить одну и ту же формулу исчисления высказываний. (Дана формула A =>(B=>(А&B)). Присваиваем А значение (Р&Н), получаем: (Р&Н)=>(B=>((Р&Н)&B))
b) Схема заключения. Из двух формул А и А=>В получаем новую формулу В. (А — камень бросили в воду, В — камень утонул. Выходит: Если камень бросить в воду, то он утонет. Камень бросили. Получаем: камень утонул.)
Формула считается доказуемой, если она или аксиома, или получена из аксиомы с помощью указанных правил или же из таких формул, которые уже доказаны.
Аксиоматическое построение именно логики высказываний обладает рядом серьезных преимуществ в сравнении с аксиоматическим построением других разделов логики. Легко доказать, что система аксиом логики высказываний является непротиворечивой, т. е. что с помощью этих аксиом нельзя доказать одновременно А и неА. Приведенные аксиомы логики высказываний являются также независимыми друг от друга, т. е. нельзя вывести хотя бы одну из них из других аксиом.
Для нас наиболее существенно то, что в рамках логики высказываний можно доказать в качестве теорем любую из клауз.
Пример доказательства:
Выдали высказывание: А=>(В=>С) =>(В=>(А=>С)
Чтобы его доказать, нужно набрать энное число клауз (здесь это могут быть как буквы, так и формулы), как говорилось выше, столько, сколько потребуется, и берём такие, что бы с ними было можно что-то сделать. То есть бесполезно брать просто А, В и С — если посмотреть в аксиомы и правила вывода, то мы убедимся, из них ничего нельзя вывести. Нужно самим абсолютно произвольно набрать такое число клауз, чтобы с ними было удобно работать. Рандомно берём простые формулы А, В и С — по ходу доказательства разберёмся, что с ними делать. Теперь нужно взять такую формулу, чтобы на неё кто-то из них среагировал. Берём А и смотрим на всю формулу, видим, что из А следует (В=>С). Смотрим, что у нас есть А (мы её взяли как клаузу), а раз она уже есть, то мы получаем (В=>С) (Это как в примере с камнем: мы его уже бросили, значит, он уже утонул). Раз А реагирует на эту формулу, то мы тоже берём её как клаузу. Запишем все клаузы, которые взяли и присвоили им истину:
- А — посылка
- В — посылка
- С — посылка
- А=>(В=>С) — посылка
И запишем вывод, который мы сделали: Раз есть А(истина) и формула А=>(В=>С) (истина), то мы получаем (В=>С). А раз обе клаузы истинны, то и это истина. Запишем, как
- (В=>С) из посылок 1 и 4.
Смотрим дальше, видим, что во второй части формулы из В следует (А=>С). Мы взяли как клаузу В, так что берём как клаузу и эту формулу, производим те же операции и записываем:
- В=>(А=>С) — посылка
- (А=>С) из посылок 2 и 6.
Теперь у нас доказаны все элементы формулы. Как видим, С как посылка не пригодилась, сделаем вид, что мы её и не брали в этом качестве. Всё равно, если мы посмотрим на сделанные нами выводы и посылки, то мы увидим, что С следует из 2 и 5. Когда будем переписывать в чистовом варианте, запишем это так.
Теперь смотрим: раз у нас есть А=>(В=>С), В, А, и только что мы из этого всего вывели С, значит что-то из этого является причиной С, то есть имплицирует ей. (свойство выводимости) (записывается это как А=>(В=>С), В, А «штопор» С) Подбираем причину так, чтобы нам было удобнее — смотрим в формулу и видим, что нам нужно, чтобы А имплицировало С, так и записываем: имеем А=>(В=>С), В штопор А=>С. Так же перегоняем В: А=>(В=>С), штопор В=>(А=>С). Видим — штопор нам указывает на причинно-следственную связь между А=>(В=>С), и В=>(А=>С). Значит, меняем его на знак импликации и имеем доказанную формулу!
В чистовом варианте это записывается так (клаузы-посылки выделены курсивом):
- А
- В
- А=>(В=>С)
- В=>(А=>С)
- (В=>С) из посылок 1 и 3.
- (А=>С) из посылок 2 и 4.
- С из посылок 2 и 5.
- А=>(В=>С), В, А штопор С
- А=>(В=>С), В штопор А=>С
- А=>(В=>С), штопор В=>(А=>С)
- А=>(В=>С), штопор В=>(А=>С)
- А=>(В=>С) =>(В=>(А=>С)
