6.6. Система природного виведення

У різновиді класичного числення висловлювань, який називають системою природного виведення, повторюють форми міркувань, використовувані в звичайній розмовній мові⁵. У цій формальній системі є п’ять операцій — кон’юнкція ( ), диз’юнкція ( ), імплікація ( ), еквівалентність ( ) і заперечення ( ), але немає аксіом, не використовуються константи І і Х, кількість правил виведення мінімальна.

Розглянемо задачу доведення того, що висновок випливає з деякого засновку (засновків у задачах може бути й кілька).

Приклад 6.14. Доведемо, що істинність формули випливає з істинності формули , тобто істинна на будь-якій інтерпретації, на якій істинна. У цій задачі засновком є формула , а висновком — . Використовуючи звичайну мову, ми можемо розв’язати сформульовану задачу, міркуючи так. Оскільки формула істинна, то істинними є обидві змінні (атомарні формули) А і В. Відповідно до однієї з властивостей операції диз’юнкції, для будь-якої змінної С формула істинна, якщо істинна змінна В. Вище ми з’ясували, що змінна В істинна, тому формула теж істинна. Нарешті, оскільки А і істинні, то за властивістю кон’юнкції маємо, що формула теж істинна.

При формальному доведенні теорем для розкриття суті самого доведення використовують схему, в якій записують:

— умову теореми;

— послідовність формул, які є засновками і стосовно яких з самого початку допускається, що вони істинні;

— послідовність формул, які є істинними відповідно до попередніх формул і різноманітних правил виведення.

Приклад 6.15. Для поданої вище задачі (приклад 6.14) схема доведення має такий вигляд:

У формальній системі природного виведення теорема, яку доводять, має вигляд: “Із , , …, одержати В”.

Цю теорему інтерпретують так: якщо формули , , …, (засновки) істинні на деякій інтерпретації, то формула В (висновок) теж істинна на цій інтерпретації.

Якщо , що означає відсутність засновків, то теорему можна інтерпретувати так: формула В істинна на всіх інтерпретаціях, тобто В — тавтологія. У цьому разі пишуть: “Одержати В”.

Формула, яка стоїть у якомусь рядку доведення, означає, що вона істинна на будь-якій інтерпретації, при якій істинні формули попередніх рядків.

Система природного виведення має 10 правил виведення — по два правила для кожної з п’яти операцій , , , і . При цьому одне правило дає можливість вводити операцію в нову формулу, інше — її вилучати. Правила введення і вилучення операції відповідно позначимо і ; аналогічно позначатимемо й інші правила.

Спочатку розглянемо правила виведення для введення кон’юнкції , вилучення кон’юнкції і введення диз’юнкції :

: ;

: , ;

: , .

Пояснимо суть цих правил для випадку двох формул і . Правило введення кон’юнкції означає, що якщо формули і містилися в попередніх рядках доведення (тобто вважається, що вони істинні, чи це доведено), то їхню кон’юнкцію можна записати в поточному рядку. Правило вилучення кон’юнкції показує, як можна вилучити кон’юнкцію, щоб одержати один із кон’юнктивних членів: якщо формула містилася в якомусь із попередніх рядків доведення (тобто вважається, що вона істинна, чи це доведено), то або формулу , або формулу можна записати в наступному рядку. Правило введення диз’юнкції означає, що якщо формула була записана на попередньому рядку, то в даному рядку можна записати диз’юнкцію .

Вказані правила по суті є схемами правил і вони виконуються для всіх формул і . Конкретні правила можна одержати, замінюючи і конкретними формулами.

Правило вилучення використовують для того, щоб розбити формулу на складові частини, а правила введення і — щоб побудувати нові формули.

Приклад 6.16. а) Проілюструємо правило введення кон’юнкції : якщо ми стверджуємо “іде дощ” і стверджуємо “світить сонце”, то можемо зробити висновок, що: “іде дощ, і світить сонце”. Формально це запишемо:

.

б) Проілюструємо правило вилучення кон’юнкції : якщо ми стверджуємо “іде дощ, і світить сонце”, то можемо зробити висновок, що “іде дощ”, і можемо зробити висновок, що “світить сонце”. Формально це запишемо:

і .

в) Проілюструємо правило введення диз’юнкції : якщо ми стверджуємо, що “іде дощ”, то можемо зробити висновок, що “іде дощ, або світить сонце”. Формально це запишемо:

.

Приклад 6.17. Нехай є дві формули і , тоді правило введення кон’юнкції запишемо:

.

Приклад 6.18. Запишемо схему доведення того, що істинність формули випливає з істинності формули (приклади 6.14 і 6.15), використовуючи правила введення і вилучення:

Приклад 6.19. а) Запишемо схему доведення того, що для операції кон’юнкції виконується імплікація :

Це доведення звичайною мовою можна подати так. Нехай формула істинна (рядок 1). Тоді істинними є кожна зі змінних А і В (рядки 2 і 3). Отже, відповідно до визначення операції кон’юнкції, формула теж істинна (рядок 4).

б) Аналогічно можна одержати імплікацію :

Правило виведення для вилучення диз’юнкції має такий вигляд:

: .

У випадку двох формул і це правило означає, що якщо на попередньому рядку містилася диз’юнкція і якщо на попередніх рядках для кожного диз’юнктивного члена стоять імплікації , то в поточному рядку доведення можна записати В.

Приклад 6.20. Проілюструємо правило вилучення диз’юнкції : якщо ми стверджуємо “завтра буде йти дощ чи сніг” і “якщо йде дощ, то сонце не світить”, а також “якщо йде сніг, то сонце не світить”, то ми можемо зробити висновок, що “завтра не буде світити сонце”. Формально (скорочено) це можна записати:

.

Приклад 6.21. Проілюструємо застосування правил вилучення і введення диз’юнкції:

Аналогічно із заданих засновків (рядки 1, 2, 3) можна одержати твердження і .

Правило виведення для вилучення імплікації (правило висновку, відокремлення — modus popens) має вигляд:

: .

Це правило дає можливість записати в поточному рядку доведення висновок імплікації, якщо її засновок з’явився в попередньому рядку.

Приклад 6.22. Проілюструємо правило вилучення імплікації : нехай ми стверджуємо “якщо йде дощ, то асфальт мокрий” і нехай встановлено, що “йде дощ”, то можна зробити висновок, що “асфальт мокрий”. Формально це можна записати:

.

Приклад 6.23. Проілюструємо застосування правила вилучення імплікації:

Звичайною мовою це доведення можна подати так. Нехай формули і є істинними. Із істинності формули робимо висновок, що змінна А істинна (відповідно до таблиці істинності для операції кон’юнкції тільки дає І). Оскільки формула істинна і змінна А теж істинна, то істинною є змінна С (відповідно до таблиці істинності для операції імплікації дає Х, а дає І). Але, якщо змінна С істинна, то до неї за допомогою операції диз’юнкції можна приєднати будь-яку формулу. Отже, формула теж істинна.

Правила виведення для введення еквівалентності і вилучення еквівалентності мають такий вигляд:

: ;

: .

Сумісно правила введення і вилучення еквівалентності визначають еквівалентність через імплікацію. Засновки одного правила є висновками іншого, і навпаки. Правило введення еквівалентності використовують для введення еквівалентності , спираючись на попереднє доведення і , а правило вилучення еквівалентності використовують для одержання іплікацій і на основі еквівалентності .

Приклад 6.24. Проілюструємо правила введення і вилучення еквівалентності:

а) нехай ми стверджуємо “якщо йде дощ, то на поверхні води розходяться кола” і стверджуємо “якщо на поверхні води розходяться кола, то йде дощ”, то можна зробити висновок, що “йде дощ тоді і тільки тоді, коли на поверхні води розходяться кола”. Формально це можна записати:

;

б) якщо ми стверджуємо “дощ іде тоді і тільки тоді, коли на поверхні води розходяться кола”, то можна стверджувати, що “якщо йде дощ, то на поверхні води розходяться кола” і “якщо на поверхні води розходяться кола, то йде дощ”. Формально це можна записати:

.

Приклад 6.25. Проілюструємо застосування правил введення і вилучення еквівалентності:

Щоб спростити запис доведення, його можна подати в скороченому вигляді — засновки в рядках доведення не записувати, а брати безпосередньо з умови теореми:

Теорема виду “Із , , …, одержати В” має таку інтерпретацію: якщо формули , , …, істинні в певному стані, то в цьому стані істинна й формула В. Якщо формули , , …, з’явилися в рядках доведення, що означає, що вони вважалися істинними чи їхню істинність було доведено, то повинна бути можливість записати в поточному рядку формулу В. Зробити це можна за допомогою правила виведення для введення імплікації , яке має вигляд:

: .

Засновок цього правила не обов’язково має з’являтися в попередніх рядках доведення. Він може з’явитися будь-де як окреме доведення, на яке можна послатися при конкретному використанні правила.

Приклад 6.26. Проілюструємо застосування правила введення імплікації (при цьому в рядках 1 і 2 використовується посилання на результати прикладу 6.19 пп. а і б):

Правило введення імплікації дає можливість зробити висновок, що формула істинна, якщо є доведення істинності В, виходячи з даного засновку А. З іншого боку, якщо формулу взято як засновок, то правило вилучення імплікації (modus popens) дає можливість зробити висновок, що В істинна, якщо А істинна. Звідси видно, що в системі природного виведення теорему дедукції можна сформулювати так.

Теорема 6.3 (теорема дедукції). “Одержати ” (це означає, що  — тавтологія) є теоремою природного виведення тоді і тільки тоді, коли “Із А одержати В” є теоремою.

Визначення 6.15. Доведення, яке міститься всередині іншого доведення, називають підвиведенням.

Використання підвиведення дає можливість записати засновок правила введення імплікації як рядок доведення.

Приклад 6.27. Проілюструємо застосування підвиведення (підвиведеннями є доведення з прикладу 6.19) на основі попереднього прикладу:

Приклад 6.28. Наведемо ще приклад застосування підвиведення:

Підвиведення може містити посилання не тільки на свої попередні рядки, а й на попередні рядки, які містяться в загальному виведенні. Їх називають глобальними посиланнями на рядки. При цьому рекурсія не допускається: наприклад, у рядку з номером не можна вживати посилання на теорему, доведення якої не закінчене до рядка .

Правило області дії. Рядок з номером в доведенні може містити посилання на рядки . Рядок може містити посилання на рядки і рядки .

З наведеного правила випливає, що рядок не може посилатися на рядок ; також рядок не може посилатися на рядок з іншого підвиведення, навіть якщо рядок розміщено в доведенні раніше від рядка .

Приклад 6.29. Проілюструємо використання правила області дії. Тут у рядку 2.2 є посилання на рядок 1, який розміщено поза областю доведення рядка 2:

Приклад 6.30. Розглянемо виведення з двома рівнями підвиведень:

Одним із методів доведення теорем є метод доведення “від протилежного”. При доведенні від протилежного, як правило, роблять припущення і з нього одержують доведення суперечності (наприклад, що якась формула істинна й хибна водночас). Оскільки така суперечність неможлива, а виведення суперечності з припущення правильне, то припущення має бути хибним.

Доведення від протилежного закладено в правилах виведення для введення заперечення і вилучення заперечення , які мають такий вигляд:

: ;

: .

Правило введення заперечення означає, що якщо “Із А одержати ” доведено для деякої формули В, то можна записати в поточному рядку доведення. Аналогічно правило вилучення заперечення дає можливість зробити висновок, що формула А істинна (тобто А можна записати в поточному рядку доведення), якщо для деякої формули В існує доведення “Із одержати ”.

Приклад 6.31. Використовуючи правило введення заперечення , доведемо, що із А випливає :

Приклад 6.32. Використовуючи правило вилучення заперечення , доведемо, що А випливає із :

У системі виведення потрібні обидва правила і : якщо одне з цих правил вилучити, то неможливо буде вивести деякі формули, які є тавтологіями (наприклад, ).

Із формул А і можна довести будь-яку формулу В. Правда, те, що з хибної формули можна вивести хибну, не є парадоксом; парадоксом є те, що з хибної формули можна вивести будь-яку формулу, а, отже, з хибного твердження — будь-яке, навіть логічно з ним не зв’язане (приклад Гільберта⁶: “Якщо , то Місяць зроблено з зеленого сиру”). Це можливо через те, що А і не можуть бути одночасно істинними, і тому засновки приводять до абсурду.

Приклад 6.33. Із формул А і виведемо формулу В:

Кожну доведену теорему, як і правила виведення, в подальшому можна розглядати як схему, підставляючи замість змінних інші змінні чи формули. Проілюструємо це на прикладі.

Приклад 6.34. З доведення теореми “Із одержати ” (приклад 6.19.а) можна вивести доведення теореми “Із одержати ”, механічно підставляючи замість А, а Е замість В у всьому доведенні:

На основі продемонстрованого на прикладі сформулюємо теорему.

Теорема 6.4 (про пряму підстановку в теорему й доведення). Нехай теорема “Із , , …, одержати ” записана як функція від змінної Р. І нехай — довільна формула. Тоді теорему “Із , , …, одержати ” теж можна довести.

Цю теорему у вигляді правила виведення можна записати так:

.

Приклад 6.35. Використовуючи теорему 6.4 про пряму підстановку, запишемо виведення для доведеної раніше теореми (приклад 6.26):

Введене при розгляді еквівалентних перетворень (п. 6.4) правило підстановки подамо в іншій формі.

Теорема 6.5 (правило підстановки) Для будь-яких формул і і формули , записаної як функція від змінної Р, теорему

можна довести в системі природного виведення.

Цю теорему можна записати у вигляді правила виведення так:

.

Приклад 6.36. Проілюструємо застосування правила підстановки (теорема 6.5). Нехай дано, що формула істинна. Щоб показати істинність формули , ми як візьмемо формулу , а замість візьмемо закон комутативності і застосуємо правило підстановки. Одержимо:

.

У системі природного виведення немає аксіом. Але в ній можна як тереми довести всі еквівалентності 1-11 і використовувати їх у подальших доведеннях.

Раніше в прикладах 6.26 і 6.27 було доведено закон комутативності для операції кон’юнкції . Подамо доведення ще деяких еквівалентностей.

Приклад 6.37. Доведемо закон виключення третього, використовуючи доведення від протилежного для одержання суперечності:

Приклад 6.38. Доведемо твердження, яке встановлює, що якщо хоч би одне з двох висловлювань істинне і якщо при цьому перше з них хибне, то друге висловлювання істинне:

Приклад 6.39. Доведемо перший закон дистрибутивності . Його доведення розіб’ємо на три частини.

Перша частина — доведемо імплікацію :

Друга частина — використовуючи закон виключення третього, доведемо зворотну імплікацію :

Третя частина — доведемо, що :

Приклад 6.40. Доведемо закон де Моргана . Як і при доведенні закону дистрибутивності, це доведення розіб’ємо на три частини.

П ерша частина — доведемо імплікацію :

Друга частина — доведемо зворотну імплікацію :

Третя частина — доведемо еквівалентність :

Приклад 6.41. Доведемо закон заперечення. Це доведення опирається на результати прикладів 6.31 і 6.32:

Або, використовуючи доведення прикладів 6.31 і 6.32 як підвиведення, запишемо повне виведення:

Вище ми розглядали дуже докладні доведення. Щоб спростити процес доведення теорем, можна проводити міркування не настільки докладно, а укрупнювати кроки — основне, щоб при цьому не втрачалася легкість розуміння доведення.

Зв’язок між системою обчислень, еквівалентними перетвореннями і системою природного виведення можна встановити так. Якщо — еквівалентність, і формула А не містить констант І і Х і є тавтологією, то “Одержати А” — теорема системи природного виведення. І навпаки: якщо “Одержати А” — теорема системи природного виведення, то А — тавтологія, а  — еквівалентність. Якщо не використовувати константи І і Х, то в будь-якому висловлюванні І можна замінити тавтологією (наприклад, або ), а Х суперечністю , тобто запереченням тавтології (наприклад, ). Таким чином, будь-яку формулу числення висловлювань можна інтерпретувати як формулу алгебри висловлювань і (якщо не використовувати константи І і Х) навпаки.