6.5. Система формального виведення

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

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

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

Визначення 6.6. Певну виділену множину формул-тавтологій називають аксіомами числення висловлювань.

Наприклад, аксіомами можна вважати всі закони еквівалентності 1-11 (усі вони є тавтологіями), або якусь частину цих законів, або інші формули-тавтології — у різних численнях висловлювань вони різні. Розглянута вище система еквівалентних перетворень формул має аксіомами всі закони еквівалентності 1-11. Зауважимо, що в різновидах числення висловлювань константи І і Х (які є в законах 6, 7 і 10), як правило, не використовуються, але, відповідно до законів 6 і 7, ці константи можна замінити на формули і .

У чи́сленні висловлювань аксіоми є початковими законами, які приймають без доведень (по суті вони є тотожно істинними формулами алгебри логіки). Кожна аксіома числення висловлювань відображає в символічній формі схему доведення. У кожну з аксіом числення висловлювань можна підставляти замість пропозиційних змінних інші аксіоми і ми будемо одержувати формули-тавтології. Крім того, тотожна істинність аксіом передбачає можливість підстановки замість пропозиційних змінних будь-яких (не обов’язково істинних) формул числення висловлювань. Отже, будь-яка підстановка в усій аксіомі замість певної змінної іншої змінної чи формули не порушить тотожної істинності аксіоми. Таким чином, маючи базовий набір аксіом числення висловлювань і застосовуючи правило підстановки, можна побудувати нескіченну кількість аксіом.

Базові аксіоми можна розглядати як схеми аксіом, у які можна підставляти замість пропозиційних змінних інші змінні чи формули і без доведення одержувати нові формули-аксіоми.

Формули, одержані шляхом застосування правила транзитивності до вже одержаних формул-тавтологій, теж дають формули-тавтології.

У зв’язку із сказаним вище правила підстановки і транзитивності є правилами виведення⁴. Правила виведення формально записують у вигляді:

(замість дробового запису також використовують запис із символом виведення у вигляді: ; символ читається як “дає”), де , , …, , , , …, є формулами (складними чи атомарними). Формули , , …, називаються засновками (умовами, гіпотезами), а формули , , …, — висновками (наслідками).

Правила виведення мають такий зміст: якщо засновки , , …, є істинними (вважаємо, що їхню істинність вже було встановлено раніше — вони можуть бути тавтологіями або істинними лише на певних інтерпретаціях, тобто умовно істинними формулами), то істинними є і формули , , …, . Зокрема, якщо засновки є тавтологіями, то тавтологіями будуть і висновки. Усі формули-тавтології (і лише такі формули) числення висловлювань можна одержати із аксіом шляхом багаторазового застосування правил виведення.

Запишемо у формальному вигляді правила підстановки й транзитивності:

(правило підстановки);

(правило транзитивності).

Важливим правилом виведення в тих різновидах числення висловлювань, в яких використовують операцію імплікації, є правило висновку (modus popens):

;

логічний зміст правила такий: якщо засновок Р правильний, то правильний і висновок Q з нього. Очевидність цього правила можна перевірити за таблицею істинності для операції імплікації: якщо імплікація і засновок Р істинні, то висновок Q в імплікації може бути тільки істинним.

Правило висновку можна узагальнити: якщо засновки , , …, і імплікація правильні, то правильний і висновок Q. Це правило називають правилом складного висновку. Схематично його можна подати так:

.

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

.

Відповідними тавтологіями для правил підстановки, транзитивності й висновку є:

;

;

.

У різновидах числення висловлювань використовують свої системи правил виведення.

Визначення 6.7. Формулу А, яку одержують з деяких формул, застосовуючи один раз якесь із правил виведення, називають безпосередньо вивідною з цих формул.

Визначення 6.8. Скінченну послідовність, яка містить одну чи більше формул числення висловлювань, називають доведенням (виведенням) формули А, якщо кожна формула в цій послідовності є або аксіомою, або безпосередньо вивідна з попередніх формул послідовності.

Визначення 6.9. Скінченну послідовність, яка містить одну чи більше формул числення висловлювань, називають доведенням (виведенням) формули А із множини формул-гіпотез (умовно істинних формул) , , …, , якщо кожна формула в цій послідовності є або аксіомою, або формулою-гіпотезою, або безпосередньо вивідна з попередніх формул послідовності.

Визначення 6.10. Формулу А числення висловлювань, для якої існує доведення, називають довідною (вивідною).

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

Визначення 6.11. Формулу А називають теоремою числення висловлювань, якщо вона довідна з аксіом.

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

Крім того, якщо формулу А можна довести із множини формул-гіпотез , , …, , то вираз “Із , , …, одержати А” теж є теоремою числення висловлювань; формально таку теорему можна записати у вигляді:

(або ); при цьому аксіоми, які використовують у доведенні, як засновки не вказують.

Будуючи доведення в чи́сленні висловлювань, формули виводять лише за допомогою правил виведення, не беручи до уваги змісту. Зміст може тільки допомогти визначити, до яких засновків застосовувати правила виведення.

Визначення 6.12. Систему аксіом числення висловлювань називають несуперечною, якщо з неї не можна вивести формулу А водночас з її запереченням .

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

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

Визначення 6.13. Систему аксіом називають повною в широкому розумінні, якщо в ній є достатня кількість аксіом, щоб вивести будь-яку тотожно істинну формулу числення висловлювань.

Теорема 6.1 (про повноту). Формула є аксіомою чи вивідною формулою (теоремою) в чи́сленні висловлювань тоді і тільки тоді, коли вона є тотожно істинною формулою (тавтологією) алгебри висловлювань.

Класичне числення висловлювань є повним у широкому розумінні. Воно також є повним у строгому (вузькому) розумінні: приєднання до його аксіом будь-якої недовідної в ньому формули робить одержане числення суперечливим.

Визначення 6.14. Систему аксіом називають незалежною, якщо жодну з аксіом системи не можна вивести з решти, застосовуючи правила виведення даної системи числення.

Незалежність системи аксіом потрібна для того, щоб у системі не було надлишкових аксіом.

Додатковим правилом виведення, яке часто суттєво скорочує доведення теорем у теорії числення висловлювань, є теорема дедукції. Ця теорема в певному розумінні є оберненням правила висновку. Наведемо цю теорему без доведення (у її доведенні використовують деякі аксіоми і правила виведення певного різновиду числення висловлювань, до операцій якого входить операція імплікації).

Теорема 6.2 (теорема дедукції). Якщо формула В вивідна із сукупності формул , , …, , С, то в чи́сленні висловлювань із , , …, виводиться формула .

Зміст теореми дедукції можна подати схематично:

якщо , то .

Наслідок 1 (узагальнена теорема дедукції). Якщо формула В вивідна із сукупності формул , , …, , то в чи́сленні висловлювань виводиться формула .

Схематично: якщо , то .

При доведенні цього наслідку треба послідовно n разів застосувати теорему дедукції:

перший крок — якщо , то ;

другий крок — якщо , то ;

…

n-й крок — якщо , то .

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

Наслідок 2. Якщо із формули А виводиться формула В, то в чи́сленні висловлювань виводиться формула .

Схематично: якщо , то .

Наслідок 3 (правило силогізму). Із засновків і виводиться формула .

Схематично: .

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

При доведенні теорем в чи́сленні висловлювань використовують дві загальні схеми доведень.

Схема 1. Якщо і , то .

Схема 2. Зведення до абсурду (суперечності): якщо і , то .

Розглянемо кілька різновидів класичного числення висловлювань.