Натуральне числення логіки висловлювань
Натуральним численням логіки висловлювань називається такий вид числення, в якому висновок будується із гіпотез (припущень) у відповідності з певними правилами.
Позначають цей вид числень символом S3.
До S3 повністю входять засоби S1. Мається на увазі алфавіт, правила утворення, правила інтерпретації нелогічних і логічних термінів. Окрім цього в S3 входять 14 правил висновку.
Якщо в аксіоматичному численні логіки висловлювань ми маємо набір аксіом і декілька правил висновку, то тут дедуктику (а це правила перетворення) складають правила введення і усунення пропозиційних зв’язок.
Структуру S3 можна зобразити такою схемою:
Логічне числення у вигляді натурального висновку має такі особливості:
а) назва цього числення «натуральне» характеризується тим, що в ньому процес виведення висновку більш наближений до звичайних міркувань людини.
Тобто «натуральне» вживається не в смислі «неформальне», «не регламентоване суворими правилами», а в смислі отримання наслідку із довільних припущень (гіпотез), а не із аксіом;
б) перевагою S3 над S2 вважається те, що тут процес виведення наслідку коротший.
Відомо, що в S2 одна й та ж сама формула в структурі доведення може зустрічатися декілька разів, що дуже рідко трапляється в S3;
в) в S3 відбувається певна систематизація правил висновку. З кожною пропозиційною зв’язкою співставля- ється одне правило введення і усунення конкретної зв’язки як головного знака формули (наявність двох правил УК (усунення кон’юнкції), ВД (введення диз’юнкції), УЕ (усунення еквіваленції) не є суттєвим).
Треба мати на увазі, що група правил введення про- позиційних зв’язок є фактично їх визначенням, а група правил усунення пропозиційних зв’язок є наслідком цих визначень.
При усуненні конкретного знака формула, якої це стосується, і знак, про який йдеться, можуть використовуватися лише в тому значенні, яке вони отримують при введенні даного знака.
Наприклад, формула А ⊃ В може бути введена, якщо наявний висновок В із припущення А, тобто, якщо вірно А |- В.
Застосовуючи до формули А ⊃ В правило УІ (усунення імплікації), діємо так, якщо б В було вивідним із доведеного А, а це можливо в силу того, що формула А ⊃ В у засновку застосування правила УІ реєструє існування висновку В із А.
Систематизація правил введення і усунення пропози- ційних зв’язок належить відомому німецькому математикові і логіку Герхарду Генцену (1909—1946 рр.). Іноді натуральні числення називають «генценівські числення».
Запишемо правила висновку для S3:
Над рискою в кожному правилі записані засновки, а під рискою — резюме застосування правил. Кожне правило містить один висновок, в той час як засновків може бути декілька (однозасновкові, двозасновкові тощо).
Всі «правила введення» уводять відповідну зв’язку у висновок застосування правила, а конже «правило усунення» усуває відповідну зв’язку із засновків. Виняток складає лише правило УД: диз’юнкція А V В скоріше тут «вводиться» ніж усувається. Але це правило можна записати у непарадоксальному вигляді:
Із записів ряду правил введення і усунення пропозиційних зв’язок очевидно, що в них використовується знак ви- відності |—, який вважається вихідним знаком. Слідуючи Генцену, цього можна уникнути:
Квадратні дужки вказують на те, що у них знаходяться припущення (або гіпотези).
В нашій системі S3 будемо вважати знак |- вихідним.
При використанні цього знака в наступних доведеннях і дедукціях мають на увазі такі його властивості:
Тепер розглянемо дефініцію доведення в S3.
На відміну від правил висновку у S2, які застосовуються тільки для виведення доказаних виразів із доказаних, у
натуральному численні правила висновку можуть бути застосовані до будь-якого виразу.
Вираз, який випливає за якимось правилом із доведеного виразу, тим, самим є доведенням. Але вираз, який випливає із недоведеного виразу, ще не доведений. У цьому випадку необхідно звільнитися якимось чином від використовуваних припущень. У наведених правилах висновку для S3 тільки двом правилам притаманна властивість звільнення від припущень: (ВІ) і (ВЗ), адже тільки вони усувають формулу А із припущень.
Оскільки в S3 немає аксіом, то доведення тут базується або на правилі введення імплікації, або на правилі введення заперечення.
Якщо останнім застосовується правило (ВІ), то висновок буде прямим, а якщо — (ВЗ), то висновок буде непрямим.
Доведення в S3 починають із припущень, а потім за правилами висновку отримують із них відповідні наслідки, після чого за допомогою правил (ВІ) та (ВЗ) елімінують (усувають) припущення. Тому в S3 вихідним є поняття доведення із припущень (гіпотез), а поняття безумовного доведення — похідним.
Дефініція поняття вивідності із припущень: «Формула В вивідна із припущень Г, А, символічно: Г,
якщо і тільки якщо:
1) існує правило висновку, в якому Г і А є засновками, а В висновком цього правила; або
2) існує деяка кінцева послідовність застосування правил висновку A1,..., An в якій засновками застосування кожного правила є або формули із Г, А, або наслідки попередніх (в даній послідовності) застосувань правил, і наслідком останнього застосування правила є формула В. При цьому дозволяється використовувати властивості знака
Гіпотезу називають усуненою в ході дедукції, якщо в процесі дедукції до цієї гіпотези (або наслідку із неї) застосовується правило (ВІ) або (ВЗ).
Доведенням формули А називається дедукція із деякої кінцевої множини гіпотез, в ході якої кожна із гіпотез усувається.
Здійснимо доведення деяких теорем пропозиційного числення за допомогою натурального висновку.
Щоб побудувати доведення теореми в S3, необхідно виконати такі дії:
1) виписати всі можливі припущення, виходячи із структури даної формули;
2) застосувати до виписаних припущень відповідні правила висновку із 14 правил, що входять у дедуктику S3;
3) застосувати одне із правил (ВІ) або (ВЗ) для елімінації припущень.
Користуючись цими настановами, перейдемо до доведення конкретних теорем. 
Таким способом будується доведення будь-якої теореми в S3.
Отже, в численнях логіки висловлювань виділяють дві формально логічні теорії: S2 і S3, основна різниця яких полягає в їх дедуктивній логіці або у дедуктиці.
