4.1.6. Метаматематичні дослідження логіки
Огляд розвитку логічних досліджень в школі (класичного пропозиціонального числення; некласичним логікам буде присвячений окремий параграф) закінчимо коротким абрисом, в центрі якого знаходиться робота Лукасевича і Тарського [1930] "Дослідження числення речень", названа авторами в тексті також і "повідомленням". Мета цього повідомлення полягала в підсумовуванні фактів, що "стосуються [...] "метаматематики", або - краще - "металогіки"".
Перші результати з області металогіки відносяться до 1924 р. У повідомленні Лукасевича [1925] (ще без доказу) стверджується, що аксіоми числення висловів в Principia Mathematica Рассела і Уайтхеда, а також аксіоми, наведені Гільбертом, як і аксіоми самого Лукасевича, викладені вище, не є незалежними. Зокрема, Лукасевич показав, що аксіому CApAqrAqApr можна вивести з аксіом CAppp, CqApq, CApqAqp і CCqrCApqApr (Principia), а аксіому CCpCpqCpq - з аксіом CpCqp, CCpCqrCqCpr, CCqrCCpqCpr, CpCNpq, CCpqCCNpqq (Гільберт).[1] Пізніше Лукасевич [1929], [1934] показав, що і аксіоми Фреге також не є незалежними. Систематичний виклад результатів подано в курсі лекцій Лукасевича [1929]. Роком пізніше в повідомленні Лукасевича і Тарського "Дослідження числення висловів" [1930] підведені підсумки роботи семінару, в якому, починаючи з 1926 р. отримали результати автори статті, а також Вайсберг, Собоцинський і Лінденбаум.
Для доказу незалежності аксіом числення висловів Лукасевич застосував багатозначну матрицю, ідея якої належить Тарському. Цей метод очевидним чином співвідноситься з дослідженнями багатозначних логік, які розвернулися у Варшаві і які привели до створення логічних матриць, відмінних від двозначних.[2] Лукасевич [1929] і Вайсберг [1937] розробили також оригінальні методи доказу повноти числення висловів в значенні Поста.
Зупинимося докладніше на неодноразово згадуваному "повідомленні" Лукасевича і Тарського, центральним поняттям якого є множина S всіх речень даного числення висловів і поняття логічної матриці. Множина S визначається як перетин всіх множин, що містять пропозиціональні змінні і замкнена щодо операцій утворення складних речень. У випадку імплікативно-негативного числення - це операції імплікації і заперечення. Якщо X міститься в S, то Cn(X) - це множина наслідків множини X, яка є перетином всіх множин, що містять X і замкнених щодо правил, які визначають операції в Cn; у разі числення висловів це правила операцій підстановки і відділення. В цій конструкції вперше для визначення металогічних понять (множини речень, наслідку) використана конструкція щонайменшої множини, замкненої щодо визначених в ній операцій.
Іншим важливим поняттям повідомлення є поняття логічної матриці, яка визначається як впорядкована четвірка M = <A, B, f, g>, де А і B – диз'юнктні множини довільних елементів, f -двох-, а g - одноаргументні функції, визначені для всіх елементів множини A+B і приймаючі значення з неї. M є нормальною матрицею, якщо з того, що xÎB і уÎА випливає, що f(x,y) Î А. Функція h називається функцією оцінки матриці M, якщо виконуються наступні умови:
1) функція h визначена для кожного xÎS;
2) якщо x є пропозиціональною змінною, то h(x) Î A+B;
3) якщо x,y Î S, то h(с(x,y)) = f(h(x), h(y));
4) якщо xÎS, то h(n(x)) = g(h(x)). Речення x задовольняє матрицю M, якщо для кожного значення функції h цієї матриці має місце h(x)ÎB, а елементи множини B називаються виділеними.
Розглянемо матрицю M = <{0}, {1}, f, g>, де функції f і g визначені наступним чином: f(x,y) = 1, коли x = 0, y = 1, або x = 1, y = 1, або x = 0, y = 0 і f(x,y) = 0, коли x = 1, y = 0, а g(x) = 1, коли x = 0, g(x) = 0, коли x = 1. Множини {0} і {1} диз'юнктні, а 1 є виділеним значенням. Функції f і g визначені на істиннісних значеннях. Легко бачити, що існує функція оцінки h, узгоджена з таблицями істинності для імплікації і заперечення; символи с і n при визначенні функції h є метамовними іменами С і N. Матриця M, очевидно, є нормальною матрицею. Таким чином, встановлена відповідність між алгеброю істиннісних оцінок і алгеброю речень. Більш того, оскільки елементи множини А і B можуть бути довільної природи, то Лінденбаум запропонував такими вважати речення і матриця в цьому випадку стає алгеброю Лінденбаума. Очевидно, що довільне речення числення висловів задовольняє матрицю, тобто таке речення оцінюється як істинне. Тим самим можна ототожнити множину істиннісних речень з реченнями, що виконуються на матриці. Позначимо цю множину E(M).
Далі, в повідомленні подається два важливі твердження, які встановлюють залежність між реченнями числення і змістом матриці. Твердження 1. Якщо M є нормальною матрицею, то E(M) - дедуктивна система, тобто система, що містить свої наслідки. Твердження 2. Якщо X - дедуктивна система, то існує нормальна матриця M, для якої множина A+B скінчена, перераховується і виконується співвідношення E(M) = X. Ці твердження, особливо друге, виявилися дуже важливими, бо матриця попросту визначає негативно-імплікативне числення висловів, а з цієї дефініції легко можна показати, що числення висловів несуперечливе і повне.
Подальше обговорення повідомлення Лукасевича і Тарського буде продовжено в наступному параграфі, оскільки торкається логік некласичних. Тут же, на завершення, згадаємо цікаві металогічні результати, які насправді демонструють реалізацію гасла "логіка для логіки". Так Собоцинський показав, що числення висловів, яке містить формули CpCqp і CpCqCCpCqrr, для кожного натурального n має аксіоматичний базис, що налічує в точності n елементів, а Тарський узагальнив це твердження для довільного пропозиціонального числення. Вайсбергом доведено наступне твердження: в численні висловів (функціонально повному або частковому), що містить формулу CpCqCrp, аксіоми містять як мінімум три різні пропозиціональні змінні. Дещо відступаючою від гасла школи є наступна знахідка Тарського, яка дозволяє визначити функтор заперечення за допомогою універсального квантора (Np = CpПp). Цей результат послужив підставою для конструкції розширеного числення висловів (Лукасевич, Тарський [1930]).
[1] Воленський [1985] стверджує, що в 1925 р. Тарський довів повноту імплікативного числення висловів, але доведення не було опубліковано.
[2] Ідею доказу незалежності аксіом ми не подаємо: її можна знайти в кожному підручнику математичної логіки, лише зауважимо, що поняття спадкової властивості, яке лежить в основі методу, використовувалося Лукасевичем також у доказі несуперечності числення висловів.