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

Реферат на тему:

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

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

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

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

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

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

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

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

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

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

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

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

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

Правило виводу R(F₁,F₂,...,F_m,G) - це відношення (або операція) на множині формул.

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

Часто правило виводу R(F₁,F₂,...,F_m,G) записують у вигляді

F₁,F₂,...,F_m .

G

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

Виведенням (виводом, вивідністю) формули B з формул A₁,A₂,...,A_n називають послідовність формул F₁,F₂,...,F_m таку, що F_m=B, а будь-яка формула F_i, i=1,2,...,m є:

1) або аксіомою;

2) або однією з початкових формул A₁,A₂,...,A_n;

3) або безпосередньо вивідною з формул F₁,F₂,...,F_i-1 (або будь-якої їх підмножини) за одним з правил виведення.

Якщо існує виведення формули B з формул A₁,A₂,...,A_n, то кажуть, що B є вивідною з A₁,A₂,...,A_n і позначають цей факт так: A₁,A₂,...,A_n |-B. Формули A₁,A₂,...,A_n називають посилками або гіпотезами виведення. Перехід у виведенні від формули F_i-1 до F_i називають i-м кроком виведення.

Доведенням формули B у теорії T називають виведення B з порожньої множини формул, тобто виведення, в якому як початкові формули використовують тільки аксіоми теорії.

Формула B, для якої існує доведення, називається формулою довідною (вивідною) у теорії T, або теоремою теорії T; факт довідності формули B позначають |-B.

При вивченні формальних теорій існує два типи тверджень:

1) твердження самої теорії або її теореми;

2) твердження про теорію (про властивості її теорем, властивості доведень тощо).

Перші є елементами (словами, виразами, формулами) внутрішньої мови теорії, а другі - зовнішніми і формулюються у термінах мови, зовнішньої по відношенню до теорії і званої метамовою теорії; самі ці твердження називають метатеоремами.

Наприклад, якщо побудовано виведення формули B з A₁,A₂,...,A_n, то твердження «A₁,A₂,...,A_n |-B» є метатеоремою; це твердження можна розглядати, як додаткове правило виводу, яке можна додати до початкових правил і використовувати у подальших конструюваннях доведень.