Елементи логіки

(AB)(BC)A  (AB)(BC)A  A(AB)(BC) 

 (AA)(AB)(BC)  (AB)(BC) 

 (ABB)(ABC)  ABC.

Отже, маємо, що істинною є формула ABC. Але вона істинна лише тоді, коли кожний співмножник істинний. Звідси висловлення C є істинним.

Таким чином, з істинності формул (AB), (BC) і A випливає істинність C. У такому випадку C називається логічним висновком цих формул.

Означення. Формула Y називається логічним висновком формул X1, X2, …, Xn, якщо з істинності X1X2…Xn випливає істинність формули Y. Формули X1, X2, …, Xn називаються засновками Y.

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

Теорема 1. Формула Y є логічним висновком формул X1, X2, …, Xn тоді й тільки тоді, коли формула (X1X2…Xn)Y є тавтологією.

Доведення. 1 (Необхідність). Припустимо, що формула Y є логічним висновком формул X1, X2, …, Xn. Якщо за деяких значень літер у формулах X1, X2, …, Xn хоча б одна з них хибна, то за означенням імплікації (X1X2…Xn)Y істинна. Якщо ж за деяких значень літер у формулах X1, X2, …, Xn всі вони істинні, X1X2…Xn також істинна. Але формула Y є логічним висновком формул X1, X2, …, Xn, тому вона також істинна. Тоді істинна і формула (X1X2…Xn)Y. Отже, за будь-яких значень літер (X1X2…Xn)Y істинна, тобто є тавтологією.

2 (Достатність). Припустимо, що (X1X2…Xn)Y є тавтологією. Тоді якщо за якихось значень літер у формулах X1, X2, …, Xn всі вони істинні, то Y також істинна, тобто є їх логічним висновком.

Теорема 2. Формула Y є логічним висновком формул X1, X2, …, Xn тоді й тільки тоді, коли формула (X1X2…XnY) є суперечністю.Доведення. За теоремою 1, формула Y є логічним висновком формул X1, X2, …, Xn тоді й тільки тоді, коли формула (X1X2…Xn)Y є тавтологією. Звідси Y є логічним висновком формул X1, X2, …, Xn тоді й тільки тоді, коли заперечення ((X1X2…Xn)Y)є суперечністю. Але

((X1X2…Xn)Y)  ((X1X2…Xn)Y) 

 ((X1X2…Xn))Y  X1X2…XnY.

Таким чином, твердження теореми істинне.

Розглянемо приклад застосування наведених теорем. Доведемо, що формула B є логічним висновком формул AB і A. Перетворимо формулу (AB)AB:

(AB)AB  (AB)AB  (AAB)(BAB)  00  0.

Отже, формула (AB)AB суперечлива, і за теоремою 2 формула B є логічним висновком формул AB і A.

Той факт, що формула B є логічним висновком формул AB і A, відіграє в математиці дуже важливу роль. Він дозволяє з уже відомих істинних тверджень AB і A одержати нове істинне твердження B. Зауважимо, що такий спосіб одержання, або виведення нових тверджень у математичній логіці є одним із основних. Таке виведення задається спеціальним правилом виведення, яке має вигляд і назву modus ponens (правило відокремлення). Воно дозволяє одержати висновок B твердження AB як окреме висловлення, тобто відокремити його вид засновку A. У математичній логіці існують і інші правила виведення, але тут ми їх не розглядаємо.