2. Правило введення диз’юнкції (вд):

_А__ , _ В__ _ з істинного судження логічно слідує диз’юнкція його з будь-яким

А Ú В АÚ В іншим судженням. Якщо істинність деякого твердження є доведе-ною, то можна утворити нове твердження-аргумент – диз’юнкцію даного з будь-яким іншим. Оскільки диз’юнкція буде істинною при істинності принаймні одного з них – А або В.

3. Правило усунення кон’юнкції (ук):

А Ù В , А Ù В _ з істинної кон’юнкції логічно слідує висловлювання, що є одним з її

А В членів. Якщо істинність кон’юнкції є доведеною, то можна відокре-мити один з її членів і використовувати як новий аргумент.

4. Правило усунення диз’юнкції (УД) або правило modus tollendo ponens (mtp):

АÚ В, ~А , А Ú В, ~В , ~А Ú В, А , А Ú ~В, В _

В А В А

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

5. Правило modus ponens (mp):

А ® В, А _ з істинної імплікації та формули, що є її антецедентом, логічно слідує

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

6. Правило modus tollens (mt):

А ® В, ~В _ з істинної імплікації та формули, що є запереченням її консеквента,

~ Ā логічно слідує формула – заперечення її антецедента. Якщо істинність умовного судження та заперечення його наслідку є доведеними, то можна відокремити формулу - заперечення підстави цього судження і використовувати як самостійний аргумент.

Крім цих основних правил виводу у формальному доведенні можна використовувати і інші правильні структури виводу або закони логіки.

3. Пряме доведення

В залежності від способу обґрунтування істинності тези доведення поділяють на пряме та непряме.

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

Розглянемо приклад формального доведення, побудованого за допомогою правила mp. Покажемо, що А ® В, В ® С, А ├ С.

Спочатку випишемо аргументи, тобто всі формули, що стоять зліва від знаку “├”. А потім, кожен новий висновок (аргумент) будемо обгрунтовувати правилом mp, записуючи його справа від висновку.

Отже:

1. А ® В

2. В ® С Аргументи

3. А

4. В – отримано по mp з 1 та 3 ( А ® В, А );

В

С – отримано по mp з 2 та 4 ( В ® С, В ).

С

Таким чином, теза “С” є доведеною. Останній рядок не нумеруємо для того, щоб показати, що доведення закінчено.

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

Візьмемо ще один приклад. Побудуємо пряме доведення для такого розміркування:

(А Ù В) ® ~С, В Ù С ├ ~А.

1. ( А Ù В) ® ~С Аргументи

2. В Ù С

3. С – за правилом УК з 2 ( В Ù С );

С

4. ~ (А Ù В) – mt з 1 і 3 ((А Ù В) ® ~С, С);

~ (А Ù В)

5. ~ (А Ù В) ® (~А Ú ~В) – логічний аргумент закон де Моргана;

6. ~А Ú ~В - mp з 5 та 4;

7. В - УК з 2;

~А - mtp з 6 та 7 (~А Ú ~В, В).

~А

Істинність тези (~А) є доведеною, оскільки кожен висновок (новий аргумент) в ході розмірковування отриманий нами за одним із правил виводу. Часто в міркуваннях висновок (тезу) формулюють як умовне судження (А ® С), тоді антецедент (А) цього твердження використовують як ще один аргумент. Тобто:

((А ® В) Ù (В ® С))→ (А ® С).

В цьому міркуванні фактично слід довести істинність твердження – “С”:

(А ® В) Ù (В ® С), А a├ С.

Доведення буде мати вигляд:

1. (А ® В) Ù (В ® С) – допущення істинності засновку;

2. А - допущення істинності антецедента;

3. А ® В - УК з 1;

4. В – mp з 3 та 2;

5. В ® С - УК з 1;

С - mp з 5 та 4.

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