Формалізація, поняття і категорії

ФОРМАЛІЗАЦІЯ - відображення змістовного знання в формалізованої теорії (обчисленні). Формализуемость знання має являти собою якимось чином фіксовану сукупність тверджень. Для визначеності доречно говорити про формалізацію деякої змістовної теорії Т. Під теорією в даному випадку мається на увазі замкнута щодо всіх своїх логічних наслідків сукупність тверджень, які стосуються відповідної предметної області. Це означає, що всі наслідки, які можна отримати в Т в рамках коректних міркувань, також відносяться до теорії Т. Можливості формалізації теорії Т за рахунок побудови відповідного обчислення (формалізованої теорії) ФТ, а також взаємини між Т і ФТ, якщо таку можливість вдається деяким чином реалізувати, залежать від ряду обставин. Зазвичай принципову можливість формалізації змістовної теорії Т пов'язують з тим, наскільки ця теорія Т підготовлена ​​до даної операції. Йдеться про її розвиненості, достатній мірі вираженість її понятійного апарату. Можливість формалізації істотно зростає при можливості розв'язання теорії, т. Е. При існуванні процедури, що дозволяє відносно будь-якого сформульованого в мові теорії пропозиції вирішувати, належить воно до теорії чи ні. Все це важливо, але головне, що відкриває принципову можливість формалізації змістовної теорії Т, - це виразні можливості символічного мови, за допомогою якого передбачається відобразити Т. Взагалі кажучи, мова числення предикатів дозволяє записати в символічній формі будь звичайне або наукове пропозицію. Для цього достатньо доповнити цю мову символами (константами) використовуваних в реченні предикатів і, може бути, ще так званими функціональними константами, про що для простоти можна не говорити. Однак мати можливість здійснити символічну запис будь-якої пропозиції теорії Г аж ніяк не означає її формалізувати. Для визнання того, що ФТ формалізує Т, необхідними є, принаймні, такі три умови:

(1) Мова L обчислення, використовуваного для формалізації, повинен давати можливість висловити будь-яку пропозицію А теорії Т за допомогою деякої формули ФТ, яка при змістовної її інтерпретації породжує пропозицію, яке прийнятне трактувати як виражає ту ж думку, що і А.

(2) Вихідні постулати (аксіоми) ФТ при отриманні з них теорем повинні розглядатися як ланцюжка беззмістовний-них символів, з яких за фіксованими правилами ви-вода виходять нові ланцюжки символів (теореми). Інакше кажучи, процес отримання теорем не повинен здійснюватися на підставі очевидності, подтверждаемости практикою ит. п.

(3) Між класом теорем ФТ і класом змістовно істинних тверджень теорії Г має бути певна обумовлений відношення, що дозволяє ФТ вважати формалізацією Г (точніше про це нижче).

Пункт (2) істотно відрізняє ФТ від Т. В Т не обов'язково є фіксовані правила виведення, і для отримання нових тверджень можна спиратися на змістовний сенс термінів і наявний контекст. Якщо, наприклад, в Т міститься твердження, що подія а сталося раніше події Р, то ми зобов'язані за змістовним підстав відносити до вірних тверджень теорії Т також і те, що В сталося пізніше а. Разом з тим ми не зобов'язані фіксувати це. Інакше в ФТ. Тут логічні зв'язки між відносинами раніше і пізніше повинні бути явно відображені. І якщо зазначені відносини позначаються як «<» и «>»Відповідно, то ФТ повинна містити правило, що дозволяє переходити від (α<β) к β> α). Очевидно, в ФТ доведеться вказати також на транзитивність зазначених відносин. Коротко кажучи, в ФУ доведеться відобразити логіку даних відносин, необхідну для опису відповідної предметної області. При цьому сама ця логіка може залежати від того, наприклад, чи буде вважатися час безперервним або дискретним, нескінченно або звичайно діленим, навіть якщо в Т ці питання не обговорюються. Таким чином, формалізація полягає не просто в тому, щоб здійснити запис Т в деякому символічній мові, але в тому, щоб виявити і відобразити при цьому логіку, якою будуть задовольняти висловлювання з тими термінами, які фігурують в Т. Рішення такої проблеми є професійним завданням логіки взагалі і може досліджуватися незалежно від тих чи інших конкретно взятих змістовних теорій і завдань, пов'язаних з їх формалізацією. Так, наприклад, в логіці формалізуються теорії алетіческіх, епістеміческіх, деонтическая, тимчасових і інші модальностей, повні щодо деяких змістовних семантик. Питання про можливість формалізації теорії Т є тому не тільки питання про готовність до цієї процедури з боку Т, а й про те, чи в достатній мірі розроблений для цієї мети наявний логічний і математичний апарат.

Проблему формалізації змістовної теорії Т в Ф Т можна вважати вирішеною, якщо в рамках метатеоріі МФТ вдається показати, що кожному істинному в прийнятій інтерпретації пропозицією Т відповідає доказові твердження ФГ (теорема повноти), і навпаки (теорема адекватності). В силу різних причин такого становища не завжди вдається домогтися. Про це говорить, зокрема, відома теорема К. Геделя (1931) про неповноту несуперечливої ​​формалізованої арифметики. Справа в тому, що деяка формалізується теорія Т може містити настільки багатий виразними можливостями мову, що в її рамках можуть будується твердження про формалізує її системі ФТ і, отже, відображатися в останній. Відбувається т. Н. замикання мови і метамови. Будь-яка несуперечлива формалізація теорії Т виявляється принципово неповної, так як будь-яка зміна ФТ породжує клас нових змістовно істинних в МФТ і в самій Т пропозицій. Саме такого роду теорією доводиться змістовна арифметика. В об'єктному мовою формалізує цю арифметику теорії ФТ можна будувати твердження про самої цієї теорії, які при змістовної інтерпретації стають справжніми пропозиціями теорії Т. В ФТ відтворюється, зокрема, деяка форма парадоксу брехуна (див. Парадокс логічний), т. К. Завжди знаходиться формула, яка стверджує свою власну недовідність в ФТ. Така формула змістовно істинна саме тому, що в ФТ недовідна. Її істинність в Г і при цьому недовідність в Ф 7 "говорить про неповноту останньої. Теорема Геделя не виключає можливості повної формалізації вужчих фрагментів математики. Теоремі Геделя про неповноту не слід надавати перебільшеного, у всякому разі універсального філософського значення і поширювати її слідства на теорії , при формалізації яких принципово відсутні і не можуть виникнути розглянуті вище причини, що перешкоджають повній формалізації всіх справжніх пропозицій змістовної математики.

Кліні С. К. Введення в метаматематику. М. 1957.