Принципи побудови формальних теорій

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

Головним предметом у дослідженнях, присвячених «ліквідуванню» кризи і «рятуванню» математики, стали принципи або правила побудови математичних тверджень і математичних теорій, зокрема, пошук відповіді на питання типу: «як повинна бути побудована теорія, щоб у ній не виникало суперечностей або антиномій?», «які властивості повинні мати методи доведення, щоб їх можна було вважати строгими?» тощо.

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

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

У кінці ХIХ століття в зв’язку з виникненням кризи в канторівській теорії множин виникла потреба перегляду загальних принципів організації математичних теорій. Це привело до створення нової галузі математики - засад математики.

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

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

У найзагальнішому вигляді формальну теорію T (інший термін - числення) будують таким чином.

1. Означають набір основних символів - алфавіт теорії.

2. Конструктивно (як правило, індуктивно) означають множину формул, або правильно побудованих виразів, яка утворює мову теорії.

3. Виокремлюють підмножину формул, які називають аксіомами теорії.

4. Задають правила виводу (виведення) теорії.

Правило виводу R(F1,F2,...,Fm,G) - це відношення (або операція) на множині формул.

Якщо формули F1,F2,...,Fm,G знаходяться у відношенні R, то формула G називається безпосередньо вивідною з формул F1,F2,...,Fm за правилом R.

Часто правило виводу R(F1,F2,...,Fm,G) записують у вигляді

F1,F2,...,Fm .

G

Формули F1,F2,...,Fm називають припущеннями, посилками або гіпотезами правила R, а формулу G - висновком, наслідком або вислідом.