Формальні теорії
3.1. Визначення формальної теорії
Формальна теорія (числення) це спосіб викладу логіки без приписування пропозиційним змінним, предикатам
та формулам значення. За задумом творців формальних теорій таким чином можна уникнути багатьох неприємностей, що виникають при використанні в логіці людської мови, що допускає двозначність, недомовленість, переінакшення вихідно закладеного значення, сенсу і т.д.
Формальна теорія це гра зі знаками, зі словами та реченнями, складеними із знаків. При цьому мається на увазі, що правила складання слів із знаків та правила гри зі словами
та пропозиціями заздалегідь обумовлені, точно та суворо прописані. В основі формальної теорії мова, якою «розмовляє» теорія. На перше місце виходить синтаксис цієї мови, тобто спосіб побудови формул, протиставлення семантиці.
Наявне таке визначення формальної теорії. Формальна теорія T складається з наступних компонентів:
1. Безліч знаків, що утворюють абетку мови теорії.
2. Безліч слів, складених із знаків алфавіту, званих формулами.
3. Підмножини формул усієї множини формул, званих
4. Безліч правил виведення, за допомогою яких формул отримують нові формули.
У мову теорії T входить алфавіт та формули. Кількість аксіом може бути кінцевою або нескінченною. У разі для наочного уявлення вони задаються з допомогою схем 2) .
1) від грец. ‚xÐwma вимога, становище.
2) від грец. sq ma образ, вигляд.
Розділ 3. Формальні теорії
За схемами легко виписуються самі аксіоми. Під логічними аксіомами, як правило, розуміють аксіоми базової логіки, над якою надбудовуються конкретні теорії за рахунок додаваннянових аксіом, що відбивають специфіку конкретної теорії. Такі аксіоми називають нелогічними.
Зазвичай формули складаються із кінцевого числа знаків. Але бувають теорії з нескінченно довгими формулами, тобто з формулами, що містять нескінченну кількість знаків.
Для позначення формул користуватимемося готичними літерами A; B; C і т. д. Ці літери не входять в алфавіт теорії, вони є лише умовними позначеннями формул.
Формальний доказ формули A теорії T це кінцева послідовність формул A 1 ; A 2; : : : ; A n де кожна формула A i або аксіома, або отримана з попередніх за допомогою одного з правил виведення, a A n це формула A. Формула A в цьому випадку називається теоремою 3) , для теорем використовується запис `A.
Формальна теорія називається повною, якщо для будь-якої формули A маємо `A або `A.
За задумом творця числення предикатів Р. Фреге 4) , будь-яка правильно побудована формула, а точніше висловлювання (висловлювання у логіці предикатів це закрита формула, т. е. формула, всі змінні якої пов'язані кванторами), має бути теоремою, т. е. повинна бути доведеним твердженням. Інакше кажучи, обчислення висловлювань та обчислення предикатів мають бути повними теоріями. Очікування Фреге виправдалися. Але, як виявилося, сильніші теорії, що включають арифметику, неповні. Це було доведено К. Ґеделем 5) (див. стор.48).
Формальна теорія називається несуперечливою, якщо в ній не доводиться формула A & A де A довільне висловлювання теорії.
Сенс умови несуперечності у цьому, що може бути доведено засобами й у рамках самої формальної теорії. На жаль, у такий спосіб, як з'ясувалося, неможливо встановити навіть несуперечність (формальної) арифметики.
3) від грец.je¸rhma уявлення, положення.
4) Фрідріх Людвіг Готлоб Фреге (Friedrich Ludwig Gottlob Frege; 1848 1925) німецький логік, математик і філософ.
5) Курт Фрідріх Гедель (Kurt Friedrich G?odel; 1906 1978) австрійський логік, математик та філософ.