6.7. Аксіоматичні системи числення висловлювань

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

Аксіоматична система з операціями заперечення ( ) й імплікації ( ). Зауважимо, що, відповідно до теореми Поста, система операцій є повною.

У цій системі, якщо А і В є формулами, то формулами також є і . Формули, які містять логічні операції кон’юнкції , диз’юнкції і еквівалентності , відповідно можна подати за допомогою формул: , , . Тут використовують три схеми аксіом, у яких P, Q, R — довільні формули:

: ;

: ;

: ,

і правило виведення — правило висновку (modus popens):

.

Крім того, оскільки А1-А3 — це схеми аксіом, то до них можна застосовувати правило підстановки:

.

Приклад 6.42. Доведемо, що формула є теоремою в чи́сленні висловлювань . Для цього виконаємо таку послідовність дій:

1) у схему аксіом А2 замість P і R підставимо A, а замість Q підставимо формулу . Одержимо:

;

2) у схему аксіом А1 замість P підставимо A, а замість Q підставимо :

;

3) за правилом modus popens , беручи замість формули результат пункту 1, а замість атомарної формули (засновку) Р результат пункту 2, матимемо:

,

отже, ;

4) у схему аксіом А1 замість P і Q підставимо А:

;

5) за правилом modus popens , беручи замість формули результат пункту 3, а замість атомарної формули Р результат пункту 4, матимемо:

.

Ми довели, що формула є теоремою в чи́сленні висловлювань ; вона виводиться лише з аксіом. Аналогічно можна довести не тільки формулу , а й будь-яку формулу, одержану підстановкою замість А іншої формули, наприклад, .

Із наведеного прикладу випливає найпростіший прийом доведення теорем: у певній схемі аксіом робимо такі підстановки, щоб в кінці одержаної формули розміщувався результат, а на її початку фрагмент, схожий на іншу аксіому; з цієї іншої аксіоми за допомогою підстановок треба спробувати одержати даний фрагмент, а потім застосувати правило modus popens, щоб залишити лише кінцеву частину формули. Проте описаний прийом не є універсальним. У доведеннях часто використовують доведені раніше теореми, правило дедукції й інші правила, які можна вивести як теореми.

Приклад 6.43. Доведемо, що із трьох умовно істинних формул-гіпотез А, В, можна одержати формулу С. Наведемо послідовність міркувань:

1) А — засновок I;

2) В — засновок II;

3) — засновок III;

4) за правилом modus popens , беручи замість формули засновок III, а замість атомарної формули Р засновок I, матимемо:

;

5) за правилом modus popens , беручи замість формули результат пункту 4, а замість атомарної формули Р засновок II, матимемо С. Таким чином, ми показали, що формула С виводиться із формул А, В і ; це можна записати схематично:

.

У цьому доведенні ми явно не застосовували аксіом. Тому дану теорему можна так само довести в будь-якій іншій аксіоматизації (зокрема й у системі природного виведення), де використовують правило виведення modus popens.

Приклад 6.44. Доведемо, що формула є теоремою в чи́сленні висловлювань . Якщо при виведенні цієї формули скористатися лише схемами аксіом, правилом modus popens і правилом підстановки, то викладки будуть дуже громіздкими. Використання теореми дедукції⁷ значно спростить процес доведення. Відповідно до узагальненої теореми дедукції (наслідок 1 з теореми 6.2), якщо із , , …, виводиться В, то в чи́сленні висловлювань виводиться формула . Тому, щоб показати вивідність формули , треба спочатку показати, що із , А виводиться В (правило слабкого вилучення заперечення; ми це доводили в прикладі 6.33, використовуючи правила виведення системи природного виведення, у якій не було жодної аксіоми). Покажемо це в системі :

1) — засновок (формула-гіпотеза) I;

2) А — засновок II;

3) у схему аксіом А1 замість P підставимо A, а замість Q підставимо :

;

4) у схему аксіом А1 замість P підставимо , а замість Q — :

;

5) за правилом modus popens , беручи замість формули результат пункту 3, а замість атомарної формули Р засновок II, матимемо:

;

6) за правилом modus popens , беручи замість формули результат пункту 4, а замість атомарної формули Р засновок I, матимемо:

;

7) у схему аксіом А3 замість P підставимо В, а замість Q — A:

;

8) за правилом modus popens , беручи замість формули результат пункту 7, а замість атомарної формули Р результат пункту 6, матимемо:

;

9) за правилом modus popens , беручи замість формули результат пункту 8, а замість атомарної формули Р результат пункту 7, матимемо В.

Отже, ми показали, що із , А виводиться В. На снові узагальненої теореми дедукції можна стверджувати, що формула вивідна.

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

1) — засновок I;

2) — засновок II;

3) А — засновок III;

4) за правилом modus popens , беручи замість формули засновок I, а замість атомарної формули Р засновок III, матимемо В;

5) за правилом modus popens, беручи замість формули засновок II, а замість атомарної формули Р результат пункту 4, матимемо С.

Отже, ми показали, що із , і А виводиться С. На снові теореми дедукції можна стверджувати, що .

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

Приклад 6.46. Доведемо, що формула , яку називають правилом контрапозиції, є теоремою в чи́сленні висловлювань . Як і в попередньому прикладі, для доведення цієї теореми скористаємося теоремою дедукції. Крім того, також використаємо доведене в попередньому прикладі правило силогізму:

1) — засновок I;

2) А — засновок II;

3) у схему аксіом А3 замість P підставимо В, а замість Q — А:

;

4) у схему аксіом А1 замість P підставимо А, а замість Q — :

;

5) за правилом modus popens , беручи замість формули результат пункту 3, а замість атомарної формули Р засновок I, матимемо:

;

6) за правилом силогізму, якщо і , то , на основі результатів пунктів 4 і 5, матимемо:

;

7) за правилом modus popens , беручи замість формули результат пункту 6, а замість атомарної формули Р засновок II, матимемо В.

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

Правило контрапозиції також можна подати у вигляді: .

Аналогічно доводиться вивідність формул , , .

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

1) — засновок I;

2) — засновок II;

3) — засновок III;

4) — правило контрапозиції;

5) за правилом modus popens , беручи замість формули формулу пункту 3, а замість атомарної формули Р засновок I, матимемо:

;

6) за правилом modus popens, беручи замість формули результат пункту 5, а замість атомарної формули Р засновок III, матимемо А;

7) за правилом modus popens, беручи замість формули засновок II, а замість атомарної формули Р результат пункту 6, матимемо С.

Отже, ми показали, що із засновків , і виводиться формула С. На снові теореми дедукції можна стверджувати, що із засновків і виводиться формула , тобто довели правило резолюцій.

Приклад 6.48. Доведемо, що із формули виводиться формула , тобто доведемо правило перестановки засновків :

1) — засновок I;

2) В — засновок II;

3) А — засновок III;

4) за правилом modus popens , беручи замість формули засновок I, а замість атомарної формули Р засновок III, матимемо:

;

5) за правилом modus popens, беручи замість формули результат пункту 4, а замість атомарної формули Р засновок II, матимемо С.

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

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

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

Якщо в аксіому А2 замінити аксіомою або аксіому А3 замінити аксіомою , то одержимо інші аксіоматичні системи класичного числення висловлювань. Зауважимо, що вказані тут аксіоми можна довести як теореми в системі .

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

У системі використовують дванадцять схем аксіом (тут P, Q, R — довільні формули):

: ;

: ;

: ;

: ;

: ;

: ;

: ;

: ;

: ;

: ;

: ;

: ,

правило виведення — правило висновку (modus popens), а також правило підстановки.

Зауважимо, що в системах і аксіоми А1 і А2 однакові.

Приклад 6.49. У системі доведемо теорему . Для цього виконаємо таку послідовність дій:

1) у схему аксіом А7 замість P підставимо В, а замість Q підставимо А:

;

2) у схему аксіом А6 замість P підставимо В, замість Q — А:

;

3) у схему аксіом А8 замість P підставимо А, замість Q — В, а замість R — :

;

4) за правилом modus popens , беручи замість формули результат пункту 3, а замість атомарної формули Р результат пункту 1, матимемо:

;

5) за правилом modus popens , беручи замість формули результат пункту 4, а замість атомарної формули Р результат пункту 2, матимемо:

.

Отже, ми довели, що формула є теоремою в чи́сленні висловлювань .

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

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

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

Якщо замінити в аксіому А12 аксіомою або двома аксіомами — А13 і аксіомою , то одержимо інші класичні числення висловлювань.

Якщо в замінити аксіоми А9-А12 трьома аксіомами , А13 і , то одержимо аксіоматизацію Гільберта класичного числення висловлювань.

Аксіоматична система (аксіоматизація Новикова⁸) з операціями кон’юнкції ( ), диз’юнкції ( ), імплікації ( ) і заперечення ( ), у якій на відміну від системи природного виведення і системи відсутня операція еквівалентності ( ), теж є одним з прикладів класичного числення висловлювань.

У системі використовують одинадцять схем аксіом (тут P, Q, R — довільні формули):

: ;

: ;

: ;

: ;

: ;

: ;

: ;

: ;

: ;

: ;

: ,

правило висновку (modus popens), а також правило підстановки.

Зауважимо, що в системах і аксіоми А1-А4 і А6-А8 однакові.

Приклад 6.50. Покажемо, що формула є вивідною в системі :

1) у схему аксіом А2 замість P і R підставимо А, замість Q — В:

;

2) за правилом modus popens , беручи замість формули результат пункту 1, а замість атомарної формули Р аксіому А1 з заміною P на А, Q на В, матимемо:

,

що свідчить про те, що ця формула вивідна, тобто є теоремою. Цю формулу так само можна вивести в системах і .

Приклад 6.51. Покажемо, що формула є вивідною в системі :

1) у схему аксіом А5 замість P підставимо формулу , замість Q — В і замість R — А:

;

2) за правилом modus popens , беручи замість формули результат пункту 1, а замість атомарної формули Р аксіому А4 з заміною P на А, Q на В, матимемо:

;

3) за правилом modus popens , беручи замість формули результат пункту 2, а замість атомарної формули Р аксіому А3 з заміною P на А, Q на В, одержимо потрібну формулу:

.

Приклад 6.52. У системі одержимо формулу . Для цього в схему аксіом А11 замість P підставимо формулу :

.

Цю формулу також можна вивести іншим шляхом:

1) у схему аксіом А9 замість P підставимо А, а замість Q — формулу :

;

2) засновок одержаної в пункті 1 формули є аксіомою А10 з заміною Р на А. Тому за правилом modus popens одержимо потрібну формулу: .

Якщо замінити в аксіому А5 аксіомою , аксіому А9 аксіомою , а аксіому А10 вилучити, то одержимо аксіоматизацію Кліні⁹. Замінивши в системі Кліні аксіому аксіомою одержимо один із різновидів аксіоматизацій інтуїціоністського (некласичного) числення висловлювань.

Аксіоматизація Россера¹⁰. У цій системі використовують дві зв’язки — кон’юнкцію ( ) і заперечення ( ), а також формулу як скорочення формули . Схемами аксіом є такі формули (тут P, Q, R — довільні формули):

: ;

: ;

: ,

використовують правило висновку (modus popens), а також правило підстановки.

Аксіоматизація Гільберта-Аккермана¹¹. У цій системі використовують дві зв’язки — диз’юнкцію ( ) і заперечення ( ), а також формулу як скорочення формули . Зауважимо, що заперечення явно в аксіомах не використовується, але, якщо А є формулою, то і також є формулою. Схемами аксіом є такі формули (тут P, Q, R — довільні формули):

: ;

: ;

: ;

: ,

використовують правило висновку (modus popens), а також правило підстановки.

Аксіоматизація Мередіта¹². У цій системі, як і в , використовують дві зв’язки — заперечення ( ) й імплікацію ( ), але система має лише одну схему аксіом (тут P, Q, R, S — довільні формули):

: ,

використовують правило висновку (modus popens), а також правило підстановки.

Аксіоматизація Нікода¹³. У цій системі використовується єдина зв’язка — штрих Шеффера ( ) і система має лише одну схему аксіом (тут P, Q, R, S — довільні формули):

: ,

використовується правило виведення , а також правило підстановки.

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