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

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

Формалізація має на увазі, що формалізуються знання має являти собою якимось чином фіксовану сукупність тверджень і взаємозв'язків між положеннями теорії, що здійснюється [найчастіше] за допомогою аксіоматичного методу. Вона передбачає, що виявлені і чітко сформульовані всі ті логічні засоби, які використовуються при виведенні з вихідних положень теорії інших її тверджень. Якщо ж, поряд з аксіоматизації і точним встановленням логічних засобів, поняття та вираження наукової теорії замінюються деякими символічними позначеннями, вона перетворюється на формальну систему.

Формалізована теорія може розглядатися як система об'єктів певного роду (символів), з якими можна звертатися, як з конкретними фізичними об'єктами, а розгортання теорії звести до маніпулювання цими об'єктами відповідно до деякою сукупністю правил, які приймають до уваги тільки вид і порядок символів. Це дозволяє абстрагуватися від того пізнавального змісту, яке виражається науковою теорією, що зазнала формалізації. Розрізняють два типи формалізованих теорій: повністю формалізовані. в повному обсязі реалізують перераховані вимоги, і частково формалізовані. коли логічні засоби, що використовуються при розгортанні даної теорії, явно не фіксуються.

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

Найбільш важливим засобом, який відкриває принципову можливість формалізації змістовної теорії Т. служать виразні можливості символічного мови, за допомогою якого передбачається відобразити Т. Слід зазначити, що мова числення предикатів дозволяє записати в символічній формі будь звичайне або наукове пропозицію. Для цього достатньо доповнити цю мову символами (константами) використовуваних в реченні предикатів і, може бути, ще так званими функціональними константами, про що для простоти можна не говорити. Однак мати можливість здійснити символічну запис будь-якої пропозиції теорії Т аж ніяк не означає її формалізувати. Для визнання того, що ФТ формалізує Т. необхідними є, принаймні, такі три умови:

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

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

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

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