Реферат на тему:
Принципи побудови формальних теорій
Математична логіка
як самостійний розділ сучасної математики сформувався відносно нещодавно - на рубежі дев’ятнадцятого і двадцятого століть. Виникнення і швидкий розвиток математичної логіки були пов’язані з так званою кризою основ (засад) математики, одним з проявів якої є відомі парадокси або антиномії канторівської теорії множин.
Головним предметом у дослідженнях, присвячених «ліквідуванню» кризи і «рятуванню» математики, стали принципи або правила побудови математичних тверджень і математичних теорій, зокрема, пошук відповіді на питання типу: «як повинна бути побудована теорія, щоб у ній не виникало суперечностей або антиномій?», «які властивості повинні мати методи доведення, щоб їх можна було вважати строгими?» тощо.
У математиці з античних часів існував зразок систематичної і строгої побудови теорії - геометрія Евкліда
, в якій усі вихідні положення формулюються явно, у вигляді аксіом, а всі твердження, істинні в цій теорії, - теореми - виводяться з цих аксіом за допомогою послідовностей логічних міркувань, що називаються доведеннями.
Однак при побудові більшості наступних математичних теорій математики, як правило, не вважали за потрібне явно виділяти всі вихідні принципи і чітко формулювати методи конструювання доведень; критерії строгості доведень та очевидності тверджень у математиці в різні часи були різними. Відтак, це призводило час від часу до виникнення криз і необхідності перегляду основ тієї чи іншої теорії.
У кінці ХIХ століття в зв’язку з виникненням кризи в канторівській теорії множин виникла потреба перегляду загальних принципів організації математичних теорій. Це привело до створення нової галузі математики - засад математики
.
Однією з фундаментальних ідей, на які спираються дослідження із засад математики, є ідея формалізації теорій
, тобто послідовного проведення аксіоматичного методу побудови теорії. При цьому не припускається використовувати будь-які припущення про об’єкти теорії, окрім тих, що виражені явно у вигляді аксіом. Аксіоми розглядають як формальні послідовності символів (вирази, формули або слова), а методи доведення - як методи одержання одних виразів з інших за допомогою операцій над символами.
Такий формальний алгебраїчний підхід гарантує чіткість і однозначність вихідних (початкових) тверджень та коректність і однозначність виводу. Однак може скластися враження, що осмисленність (зміст, інтерпретація або семантика) понять і тверджень у формалізованій теорії не відіграють жодної ролі. Зовні це так і є; однак, насправді, і аксіоми, і правила виводу прагнуть означати так, щоб побудована за їхнью допомогою формальна теорія мала б змістовний сенс.
У найзагальнішому вигляді формальну теорію
T
(інший термін - числення
) будують таким чином.
1. Означають набір основних символів - алфавіт
теорії.
2. Конструктивно (як правило, індуктивно) означають множину формул
, аб
3. Виокремлюють підмножину формул, які називають аксіомами
теорії.
4. Задають правила виводу
(виведення
) теорії.
Правило виводу R
(F
1
,F
2
,...,Fm
,G
) - це відношення (або операція) на множині формул.
Якщо формули F
1
,F
2
,...,Fm
,G
знаходяться у відношенні R
, то формула G
називається безпосередньо вивідною
з формул F
1
,F
2
,...,Fm
за правилом R
.
Часто правило виводу R
(F
1
,F
2
,...,Fm
,G
) записують у вигляді
F
1
,F
2
,...,Fm
.
G
Формули F
1
,F
2
,...,Fm
називають припущеннями
, посилками
або гіпотезами
правила R
, а формулу G
- висновком
, наслідком
або вислідом
.
Виведенням
(виводом
, вивідністю
) формули B
з формул A
1
,A
2
,...,An
називають послідовність формул F
1
,F
2
,...,Fm
таку, що Fm
=B
, а будь-яка формула Fi
, i
=1,2,...,m
є:
1) або аксіомою;
2) або однією з початкових формул A
1
,A
2
,...,An
;
3) або безпосередньо вивідною з формул F
1
,F
2
,...,Fi
-1
(або будь-якої їх підмножини) за одним з правил виведення.
Якщо існує виведення формули B
з формул A
1
,A
2
,...,An
, то кажуть, що B
є вивідною
з A
1
,A
2
,...,An
і позначають цей факт так: A
1
,A
2
,...,An
|-B
. Формули A
1
,A
2
,...,An
називають посилками
або гіпотезами
виведення. Перехід у виведенні від формули Fi
-1
до Fi
називають i
-м кроком виведення.
Доведенням
формули B
у теорії T
називають виведення B
з порожньої множини формул, тобто виведення, в якому як початкові формули використовують тільки аксіоми теорії.
Формула B
, для якої існує доведення, називається формулою довідною
(вивідною
) у теорії T
, або теоремою
теорії T
; факт довідності формули B
позначають |-B
.
При вивченні формальних теорій існує два типи тверджень:
1) твердження самої теорії або її теореми;
2) твердження про теорію (про властивості її теорем, властивості доведень тощо).
Перші є елементами (словами, виразами, формулами) внутрішньої мови теорії, а другі - зовнішніми і формулюються у термінах мови, зовнішньої по відношенню до теорії і званої метамовою
теорії; самі ці твердження називають метатеоремами
.
Наприклад, якщо побудовано виведення формули B
з A
1
,A
2
,...,An
, то твердження «A
1
,A
2
,...,An
|-B
» є метатеоремою; це твердження можна розглядати, як додаткове правило виводу, яке можна додати до початкових правил і використовувати у подальших конструюваннях доведень.