Проілюструємо, що аксіома (A B) A є незалежною.
1.Припустимо, що A B A не вивідна із аксіом S2. Якщо вона не вивідна, то |=, тобто приймає значення, відмінне від значень решти аксіом.
2.Надамо цій аксіомі інтерпретацію, відмінну від ін-
терпретації решти аксіом. Для цього обумовимо кон’юнкцію такою констатацією: A B = B, тобто яке зна- чення приймає В, таке значення приймає A B.
3.Відповідно до цього аксіома набуде вигляду: В А.
4.В А не є |= (згідно з таблицею істинності для імплі-
кації).
За такої інтерпретації « » можна гарантувати, що аксі- оми, в структурі яких відсутня кон’юнкція, залишаються
тавтологіями.
Нас цікавить, як поводять себе аксіоми, в структурі
|
|
|
|
|
|
|
|
яких є « «: |
B) |
|
|
|
а) |
1. |
(A |
B |
– Ax. – 4 |
|
2. |
|= (B |
B) |
(A B)) |
– A |
B/B; |
б) |
1. |
A |
(B |
– Ax. – 5 |
|
2. |
|= A |
(B B) |
– A |
B/B. |
Отже, всі аксіоми окрім (A B) A залишаються тав- тологіями, незважаючи на ті дефініції, які над ними здій- снювалися. А це означає, що вона є незалежною.
Аналізом металогічних принципів завершується зна- йомство з аксіоматичним численням логіки висловлювань.
3. Натуральне числення логіки висловлювань
Натуральним численням логіки висловлювань нази- вається такий вид числення, в якому висновок будуєть- ся із гіпотез (припущень) у відповідності з певними правилами.
Позначають цей вид числень символом S3.
До S3 повністю входять засоби S1. Мається на увазі ал-
фавіт, правила утворення, правила інтерпретації не- логічних і логічних термінів. Окрім цього в S3 входять 14 правил висновку.
Якщо в аксіоматичному численні логіки висловлювань ми маємо набір аксіом і декілька правил висновку, то тут дедуктику (а це правила перетворення) складають правила введення і усунення пропозиційних зв’язок.
Книга друга. СУЧАСНА ЛОГІКА |
359 |
Структуру S3 можна зобразити такою схемою:
S3
Sin ML
OL
ML
1)ПУ
2)ПП
правила введення і усунення пропо- зиційних зв’язок
ПІ
Sem ML
Логічне числення у вигляді натурального висновку має такі особливості:
а) назва цього числення «натуральне» характеризу- ється тим, що в ньому процес виведення висновку більш наближений до звичайних міркувань людини.
Тобто «натуральне» вживається не в смислі «неформа- льне», «не регламентоване суворими правилами», а в сми- слі отримання наслідку із довільних припущень (гіпотез), а не із аксіом;
б) перевагою S3 над S2 вважається те, що тут процес виведення наслідку коротший.
Відомо, що в S2 одна й та ж сама формула в структурі доведення може зустрічатися декілька разів, що дуже рід- ко трапляється в S3;
в) в S3 відбувається певна систематизація правил висновку. З кожною пропозиційною зв’язкою співставля- ється одне правило введення і усунення конкретної зв’язки як головного знака формули (наявність двох пра-
вил УК (усунення кон’юнкції), ВД (введення диз’юнкції), УЕ (усунення еквіваленції) не є суттєвим).
Треба мати на увазі, що група правил введення про- позиційних зв’язок є фактично їх визначенням, а група правил усунення пропозиційних зв’язок є наслідком цих визначень.
360 |
А. Є. Конверський. ЛОГІКА |
При усуненні конкретного знака формула, якої це сто- сується, і знак, про який йдеться, можуть використовувати- ся лише в тому значенні, яке вони отримують при введенні даного знака.
Наприклад, формула А В може бути введена, якщо
наявний висновок В із припущення А, тобто, якщо вірно
А |− В.
Застосовуючи до формули А В правило УІ (усунення імплікації), діємо так, якщо б В було вивідним із дове- деного А, а це можливо в силу того, що формула А В у засновку застосування правила УІ реєструє існування ви- сновку В із А.
Систематизація правил введення і усунення пропози- ційних зв’язок належить відомому німецькому математи- кові і логіку Герхарду Генцену (1909–1946 рр.). Іноді на- туральні числення називають «генценівські числення».
Запишемо правила висновку для S3:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1. |
Г, Ф| — (ВІ) |
2. |
A, A |
B (УІ) |
Г| —А В |
|
|
B |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
3. |
А, В (ВК) |
4. |
A В |
, |
А В |
(УК) |
А |
В |
|
|
|
|
|
|
|
|
|
А |
|
|
В |
5. |
А |
|
, |
|
В (ВД) |
6. |
Г, А| —С ГВ| —С |
|
|
|
|
|
|
|
|
|
|
|
|
А |
|
|
В |
Г, А В| —C |
|
В А |
|
7.Г, А| —В _ГА| — | В (ВЗ)
Г| − | А
8. |
| |
| А (УПЗ) А, |
|
| А |
(Сл. УЗ) — слабке усунення |
А |
|
|
В |
|
|
|
заперечення |
|
|
|
|
А |
В, В А (ВЕ) |
|
А ~ B |
|
А ~ В (УЕ) |
9. |
|
|
|
|
|
|
|
|
, |
|
|
. |
|
А ~ В |
|
А В |
А |
|
|
|
|
|
А |
Над рискою в кожному правилі записані засновки, а під рискою – резюме застосування правил. Кожне правило містить один висновок, в той час як засновків може бути декілька (однозасновкові, двозасновкові тощо).
Всі «правила введення» уводять відповідну зв’язку у висновок застосування правила, а конже «правило усунен- ня» усуває відповідну зв’язку із засновків. Виняток скла- дає лише правило УД: диз’юнкція А В скоріше тут «вво-
Книга друга. СУЧАСНА ЛОГІКА |
361 |
диться» ніж усувається. Але це правило можна записати у непарадоксальному вигляді:
А В Γ , А |− С Γ , В |− С .
Γ |− С
Із записів ряду правил введення і усунення пропозицій- них зв’язок очевидно, що в них використовується знак ви- відності |−, який вважається вихідним знаком. Слідуючи Генцену, цього можна уникнути:
[АА |
|
[А] [В] |
В |
|
(ВІ) , |
|
А В < С < С (УД) |
|
|
|
|
|
А |
|
|
С |
В |
|
|
|
|
[А] [А] |
|
|
|
|
_ |
|
(ВЗ). |
|
|
|
В_ | В |
|
|
|
|
| А |
|
|
|
Квадратні дужки вказують на те, що у них знаходяться припущення (або гіпотези).
В нашій системі S3 будемо вважати знак |− вихідним.
При використанні цього знака в наступних доведен- нях і дедукціях мають на увазі такі його властивості:
а) А |− А – рефлексивність вивідності; б) якщо Γ ∆ і Γ |− А, то ∆ |− А – (де Γ і ∆ – довільні
послідовності формул, А – формула).
Ця властивість фіксує той факт, що якщо А вивідна із множини засновків, то вона залишається вивідною, якщо до Γ додати додаткові засновки. Іншими словами: якщо А |− В, то С, А |− В;
в) Γ |− А тоді і тільки тоді, коли в Γ існує кінцева підмножина формул ∆ , для якої ∆ |− А;
г) якщо ∆ |− А і Γ |− В для будь-якої формули В із ∆ , то із Γ |− А. Іншими словами: якщо А |− В і В |− С, то А |− С (транзитивність |−).
Власне, ці властивості знака відповідності |− справедливі і для S2.
Тепер розглянемо дефініцію доведення в S3.
На відміну від правил висновку у S2, які застосовуються тільки для виведення доказаних виразів із доказаних, у
362 |
А. Є. Конверський. ЛОГІКА |
натуральному численні правила висновку можуть бути за- стосовані до будь-якого виразу.
Вираз, який випливає за якимось правилом із доведе- ного виразу, тим, самим є доведенням. Але вираз, який випливає із недоведеного виразу, ще не доведений. У цьо-
му випадку необхідно звільнитися якимось чином від ви- користовуваних припущень. У наведених правилах висно-
вку для S3 тільки двом правилам притаманна власти- вість звільнення від припущень: (ВІ) і (ВЗ), адже тільки вони усувають формулу А із припущень.
Оскільки в S3 немає аксіом, то доведення тут базується або на правилі введення імплікації, або на правилі введен- ня заперечення.
Якщо останнім застосовується правило (ВІ), то ви- сновок буде прямим, а якщо – (ВЗ), то висновок буде непрямим.
Доведення в S3 починають із припущень, а потім за правилами висновку отримують із них відповідні нас- лідки, після чого за допомогою правил (ВІ) та (ВЗ) елі- мінують (усувають) припущення. Тому в S3 вихідним є поняття доведення із припущень (гіпотез), а поняття безу- мовного доведення – похідним.
Дефініція поняття вивідності із припущень: «Фор- мула В вивідна із припущень Γ , А, символічно: Γ , А |− В,
якщо і тільки якщо:
1) існує правило висновку, в якому Γ і А є засновками,
а В висновком цього правила; або 2) існує деяка кінцева послідовність застосування
правил висновку А1, ..., Аn в якій засновками застосу- вання кожного правила є або формули із Γ , А, або нас-
лідки попередніх (в даній послідовності) застосувань правил, і наслідком останнього застосування правила є формула В. При цьому дозволяється використовувати властивості знака |−».
Гіпотезу називають усуненою в ході дедукції, якщо в
процесі дедукції до цієї гіпотези (або наслідку із неї) за- стосовується правило (ВІ) або (ВЗ).
Доведенням формули А називається дедукція із де- якої кінцевої множини гіпотез, в ході якої кожна із гі- потез усувається.
Книга друга. СУЧАСНА ЛОГІКА |
363 |
Здійснимо доведення деяких теорем пропозиційного чи- слення за допомогою натурального висновку.
Щоб побудувати доведення теореми в S3, необхідно виконати такі дії:
1) виписати всі можливі припущення, виходячи із структури даної формули;
2) застосувати до виписаних припущень відповідні
правила висновку із 14 правил, що входять у дедуктику
S3;
3) застосувати одне із правил (ВІ) або (ВЗ) для елімі- нації припущень.
Користуючись цими настановами, перейдемо до дове- дення конкретних теорем.
Теорема 1. (А |
В) |
((В |
С) |
(А С)). |
Доведення. |
|
|
|
|
|
1. |
А |
В |
|
|
|
|
– припущення 1 |
2. |
В |
С |
|
|
|
|
– припущення 2 |
3. |
А |
|
|
|
|
|
|
|
– припущення 3 |
4. |
В |
|
|
|
|
|
|
|
– УІ до 1,3 |
5. |
С |
|
|
|
|
|
|
|
– УІ до 2, 4 |
6. |
А |
С |
(В |
|
|
|
– ВІ до 3,5 |
7. (А |
В) |
С) |
|
|
– ВІ до 1, 2 |
8. |
|− (А В) ((В |
С) (А С)) – ВІ до 6,7. |
Теорема 2. (А |
В) |
((С |
А) |
(С В)). |
Доведення. |
|
|
|
|
|
1. |
(А |
В) |
|
|
|
|
– припущення 1 |
2. |
(С |
А) |
|
|
|
|
– припущення 2 |
3. |
С |
|
|
|
|
|
|
|
– припущення 3 |
4. |
А |
|
|
|
|
|
|
|
– УІ до 2, 3 |
5. |
В |
|
|
|
|
|
|
|
– УІ до 1, 4 |
6. |
(С |
В) |
(С |
|
|
|
– ВІ до 3,5 |
7. |
(А |
В) |
А) |
|
|
– ВІ до 1,2 |
8. |− (А В) ((С А) (С В)). |
Теорема 3. (А |
В) |
((С |
А) |
(С В)). |
Доведення. |
|
|
|
|
|
1. |
(А |
В) |
|
|
|
|
– припущення 1 |
2. (С |
А) |
|
|
|
|
– припущення 2 |
364 |
А. Є. Конверський. ЛОГІКА |
3. |
С |
|
|
|
|
|
|
|
– УК до 2 |
4. |
А |
|
|
|
|
|
|
|
– УК до 2 |
5. |
В |
|
|
|
|
|
|
|
– УІ до 1,4 |
6. |
С |
В |
(С |
|
|
|
|
– ВК до 3,5 |
7. |
(А |
В) |
А) |
А) |
(С |
|
– ВІ до 1,2 |
8. |
|− (А В) ((С |
В)) |
– ВІ до 6,7. |
Теорема 4. (А |
В) |
((А С) (В С)). |
Доведення. |
|
|
|
|
|
|
1. |
(А |
В) |
|
|
|
|
|
– припущення 1 |
2. (А |
С) |
|
|
|
|
|
– припущення 2 |
3. |
А |
|
|
|
|
|
|
|
– УК до 2 |
4. |
С |
|
|
|
|
|
|
|
– УК до 2 |
5. |
В |
|
|
|
|
|
|
|
– УІ до 1,3 |
6. |
В |
С |
(А |
|
|
|
|
– ВК до 4,5 |
7. |
(А |
В) |
С) |
С) |
(В |
|
– ВІ до 1,2 |
8. |
|− (А В) ((А |
С)) |
– ВІ до 6,7. |
Теорема 5. (А |
В) |
((С А) (С В)). |
Доведення. |
|
|
|
|
|
|
1. |
А |
В |
|
|
|
|
|
– припущення 1 |
2. |
А |
|
|
|
|
|
|
|
– припущення 2 |
3. |
В |
|
|
|
|
|
|
|
– УІ до 1,2 |
4. |
С |
В |
|
|
|
|
|
– ВД до 3 |
5. |
С |
В, С |
А |− С В |
|
|
– припущення 3 |
6. |
А |
|
|
– УД1 до (1,2,4) і (1,5,4) |
7. |
(А |
В) |
(С |
А) |
А) |
(С |
|
– ВІ до 1,6 |
8. |
|− (А В) ((С |
В)) – ВІ до 7,4. |
Таким способом будується доведення будь-якої теоре- ми в S3.
Отже, в численнях логіки висловлювань виділяють дві формально логічні теорії: S2 і S3, основна різниця яких полягає в їх дедуктивній логіці або у дедуктиці.
1Маються на увазі послідовності 1) А В, А |− С В
2)А В, С |− С В.
Книга друга. СУЧАСНА ЛОГІКА |
365 |
