• Напечатать
• Спросить
• Отправить другу
• Поделиться
  • Facebook
  • Twitter
• Подписаться на новости

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

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

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

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

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

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

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

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

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

Правило виводу 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 - висновком, наслідком або вислідом.

Виведенням (виводом, вивідністю) формули B з формул A1, A2,..., An називають послідовність формул F1, F2,..., Fm таку, що Fm=B, а будь-яка формула Fi, i=1,2,..., m є:

• або аксіомою;
• або однією з початкових формул A1, A2,..., An;
• або безпосередньо вивідною з формул F1, F2,..., Fi-1 (або будь-якої їх підмножини) за одним з правил виведення.

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

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

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

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

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

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

Наприклад, якщо побудовано виведення формули B з A1, A2,..., An, то твердження "A1, A2,..., An |-B" є метатеоремою; це твердження можна розглядати, як додаткове правило виводу, яке можна додати до початкових правил і використовувати у подальших конструюваннях доведень.

23.10.2011