4.1.5. Натуральний умовивід Ст. Яськовського
В 1926 р. Лукасевич поставив проблему, витоки якої можна помітити в розглянутій вище роботі "Про науку". А саме, в математичних доказах не використовуються логічні формули, але в них звертаються до передумов і правил міркувань. Чи можна ці методи доказу відобразити в системі структурних правил і дослідити їх відношення до тверджень аксіоматичного числення висловів? В 1927 р. Яськовський відповів на це питання; результати викладені в роботі "Про правила припущень у формальній логіці" [1934].
Спочатку Яськовський наводить приклади, за допомогою яких з'ясовує інтуїтивне значення методу припущень. Якщо ми хочемо переконатися в істинності формули CpCCpqq, то можна це зробити таким чином:
1. Припустимо p.
2. Припустимо Cpq.
3. З 1 і 2 випливає q.
4. З урахуванням того, що q є наслідком припущення Cpq отримаємо імплікацію Cpqq.
5. З урахуванням припущення p одержуємо вираз CpCpqq.
Наведений неформальний вивід кодується таким чином:
1.Sp
1.1.SCpq
1.1.q
1.CCpqq
CpCCpqq
Символ S є скороченням для звороту "припускається". Кожному припущенню передує цифровий префікс. Префікс, складений з однієї цифри і крапки, означає головне припущення в даному виводі, а префікс, складений з більшого числа цифр і крапок, означає подальші припущення. Якщо подальше припущення позначено префіксом, початковий сегмент якого ідентичний з префіксом деякого вже записаного в даному виводі припущення, то це значить, що ми маємо справу з припущенням, яке охоплюється попереднім припущенням, наприклад, SCpq знаходиться, якщо можна так виразитися, в області припущення Sp. Якщо рядку виводу передує цифровий префікс, після якого знак S не записується, то тоді вираз, що стоїть безпосередньо після префікса, є наслідком припущення, яке має той самий префікс, наприклад, q є наслідком SCpq.
Яськовський представляє систему натуральної дедукції у вигляді послідовності виразів, кожне з яких він вважає таким, що належить численню. Зокрема, передбачається, що істинними формулами системи є припущення та їх наслідки. Таке широке розуміння істинної формули, звичайно, не суперечить її розумінню у вузькому значенні як формули доказової.
Опис системи починається наведеним вище прикладом і Яськовський припускає, що на момент написання першого припущення жодні інші формули не існують. Якщо яка-небудь формула T має номер n, то всі формули, що мають в початковому сегменті номер n, належать (разом з T) до області T; в наведеному прикладі до області формули q належать вирази Sp, SCpq і саме q. Під абсолютною областю Яськовський розуміє множину всіх записаних формул системи, а сама абсолютна область збільшується одночасно з розвитком всієї системи. На момент написання першої формули абсолютна область є порожньою множиною. Ці властивості поповнення формальної системи свідчать про вплив Леснєвського. В 1926 р. на семінарі Лукасевича поняття області Яськовський експлікував таким чином:
p
Cpq
p
q
CCpqq
CpCCpqq
Однак префіксна нотація областей припущень у якості їх імен суперечить поглядам Леснєвського. В зв'язку з цим Яськовський зауважує: "Можна розуміти область як клас виразів у згоді з поглядами Леснєвського на клас як матеріальний об'єкт, але в цьому випадку тлумачення сегментів буде модифіковано і формулювання правил тим самим значно ускладниться". ([1934], S.9)
Правила побудови системи Яськовського наступні:
(R1) До кожної області формул D можна додати вирази, що складаються з (a) префікса, який відрізняється від початкового сегменту префікса довільного елемента D, (b) крапки, (c) символу S, (d) речення.
(RII) Якщо в області D припущення x істинним є речення у, то до області, в якій D є підобластю, можна додати речення Cxy. З двох областей D і D`, де D - область припущення x, а D` - абсолютна область або область припущення x`, префікс якої ідентичний з початковим сегментом префікса припущення x, D є підобластю D` і D є безпосередня підобласть D` тоді і тільки тоді, коли D не є підобластю ніякої підобласті D`.
(RIII) Якщо в даній області D істинні речення Cxy і x, то допустимо до D додати у; це правило, звичайно, є правилом modus роnens для натурального виводу.
(RIV) Якщо в області D припущення Nx істинні речення у і Ny, то до області, відносно якої D є підобластю, можна додати речення x.
Використовуючи наведені правила Яськовський конструює систему, що містить 59 речень "теорії дедукції" (у висновку позначаються td); нижче подаються перші двадцять з них (з правої сторони подані номери речень і правил, які використовуються у виводі даного речення:
td1 1.Sp I
td2 1.1.SCpq I
td3 1.1.q III,2,1
td4 1.CCpqq II,2,3
td5 CpCCpqq II,1,4
td6 2.SCNpNq I
td7 2.1.Sq I
td8 2.1.1.SNp I
td9 2.1.1.Nq III,6,8
td10 2.1.p IV,8,7,9
td11 2.Cqp II,7,10
td12 CCNpNqCqp II,6,11
td13 1.2.Sq I
td14 1.Cqp II,13,1
td15 CpCqp II,1,14
td16 1.3.SNp I
td17 1.3.1.SNq I
td18 1.3.q IV,17,1,16
td19 1.CNpq II,16,18
td20 CpCNpq II,1,19
Таким чином, система виводу Яськовського будується на припущеннях і правилах виводу, але її відмінність від системи Генцена крім кодифікаційних особливостей, визначуваних, ймовірно, бездужковим записом, полягає і на тому, що вона зберігає підобласті абсолютної області (яка позначається по мірі побудови формулами без префіксів) і тим самим містить також правила побудови всієї системи. Отже, твердженням логіки в системі Яськовського не передують цифрові префікси. Він формулює метатеорему, стверджуючу еквівалентність аксіоматичної системи Лукасевича і системи, побудованої на припущеннях. "Доказ" цього твердження є по суті лише абрисом проблеми і покоїться на понятті побудови речення, центральне значення якого передається терміном "еквіморфний" (equiform).
Поза сумнівом, конструкція Яськовського належить до найвидатніших досягнень, отриманих не тільки на семінарі Лукасевича, але і у Львівсько-Варшавській школі. Якщо врахувати, що перші результати датуються 1926 р., то система польського логіка є першою системою натурального виводу в логічній практиці.