Формальна система (формальна теорія. Аксіоматична теорія. Аксіоматика. Дедуктивна система) - результат суворої формалізації теорії. яка передбачає повну абстракцію від сенсу слів використовуваної мови, причому всі умови, які регулюють вживання цих слів в теорії, явно висловлені за допомогою аксіом і правил, що дозволяють вивести одну фразу з інших [1].
Формальна система - це сукупність абстрактних об'єктів, не пов'язаних із зовнішнім світом, в якій представлені правила оперування безліччю символів в строго синтаксичної трактуванні без урахування смислового змісту, тобто семантики. Строго описані формальні системи з'явилися після того, як була поставлена задача Гільберта. Перші ФС з'явилися після виходу книг Рассела і Уайтхеда «Формальні системи» [уточнити]. Цим ФС були пред'явлені певні вимоги.
Основні положення [| ]
Формальна теорія вважається визначеною, якщо [2]:
- Визнач кінцеве або рахункове безліч довільних символів. Кінцеві послідовності символів називаються виразами теорії.
- Є підмножина виразів, які називаються формулами.
- Виділено підмножина формул, які називаються аксіомами.
- Є кінцеве безліч відносин між формулами, які називаються правилами виведення.
Звичайно є ефективна процедура, що дозволяє з даного виразу визначити, чи є воно формулою. Часто безліч формул задається індуктивним визначенням. Як правило, це безліч нескінченно. Безліч символів і безліч формул в сукупності визначають мову або сигнатуру формальної теорії.
Для кожного правила виведення R і для кожної формули A ефективно вирішується питання про те, чи знаходиться обраний набір формул щодо R з формулою A. і якщо так, то A називається безпосереднім наслідком даних формул за правилом R.
Висновком називається всяка послідовність формул така, що будь-яка формула послідовності є або аксіома, або безпосередній наслідок будь-яких попередніх формул по одному з правил виведення.
Формула називається теоремою. якщо існує висновок, в якому ця формула є останньою.
Теорія, для якої існує ефективний алгоритм, що дозволяє дізнаватися по даній формулі, чи існує її висновок, називається вирішуваною; в іншому випадку теорія називається нерозв'язною.
Теорія, в якій не всі формули є теоремами, називається абсолютно несуперечливої.
Визначення та різновиди [| ]
Дедуктивна теорія вважається заданою, якщо:
- Заданий алфавіт (безліч) і правила утворення виразів (слів) в цьому алфавіті.
- Задані правила освіти формул (правильно побудованих, коректних висловлювань).
- З безлічі формул деяким способом виділено підмножина T теорем (доказових формул).
Різновиди дедуктивних теорій [| ]
Залежно від способу побудови безлічі теорем:
Завдання аксіом і правил виведення [| ]
У безлічі формул виділяється підмножина аксіом, і задається кінцеве число правил виведення - таких правил, за допомогою яких (і тільки за допомогою їх) з аксіом і раніше виведених теорем можна утворити нові теореми. Всі аксіоми також входять до числа теорем. Іноді (наприклад в аксіоматиці Пеано) теорія містить нескінченну кількість аксіом, що задаються за допомогою однієї або декількох схем аксіом. Аксіоми іноді називають «прихованими визначеннями». Таким способом задається формальна теорія (формальна аксіоматична теорія. Формальне (логічне) обчислення).
Завдання тільки аксіом [| ]
Задаються тільки аксіоми, правила виведення вважаються загальновідомими.
Приклади [| ]
Завдання тільки правил виводу [| ]
Аксіом немає (безліч аксіом порожньо), задаються тільки правила виведення.
По суті, задана таким чином теорія - окремий випадок формальної, але має власну назву: теорія природного виведення.
Властивості дедуктивних теорій [| ]
Несуперечливість [| ]
Теорія, в якій безліч теорем покриває все безліч формул (всі формули є теоремами, «істинними висловлюваннями»), називається суперечливою. В іншому випадку теорія називається несуперечливої. З'ясування суперечливості теорії - одна з найважливіших і іноді складних завдань формальної логіки. Після з'ясування суперечливості теорія, як правило, не має подальшого ні теоретичного, ні практичного застосування.
Повнота [| ]
Теорія називається повною. якщо в ній для будь-якої пропозиції (замкнутої формули) F виводиться або саме F. або його заперечення # X00AC; F. В іншому випадку, теорія містить недоведені твердження (затвердження, які не можна ні довести, ні спростувати засобами самої теорії), і називається неповною.
Незалежність аксіом [| ]
Окрема аксіома теорії вважається незалежною. якщо цю аксіому можна вивести з інших аксіом. Залежна аксіома по суті надлишкова, і її видалення із системи аксіом ніяк не відіб'ється на теорії. Вся система аксіом теорії називається незалежною. якщо кожна аксіома в ній незалежна.
Можливість розв'язання [| ]
Теорія називається вирішуваною. якщо в ній поняття теореми ефективно. тобто існує ефективний процес (алгоритм), що дозволяє для будь-якої формули за кінцеве число кроків визначити, є вона теоремою чи ні.
Найважливіші результати [| ]
- У 30-і рр. XX століття Курт Гедель показав, що є цілий клас теорій першого порядку, є неповними. Більш того, формула, яка стверджує несуперечність теорії, також невиведені засобами самої теорії (див. Теореми Геделя про неповноту). Цей висновок мав величезне значення для математики, так як формальна арифметика (а також будь-яка теорія, що містить її в якості подтеоріі) є якраз такою теорією першого порядку, а отже, неповна.
- Незважаючи на це, теорія матеріально замкнутих полів [en] зі складанням, множенням і відношенням порядку є повною (теорема Тарського - Зайденберга).
- Чёрчем доведено, що не існує алгоритму, який для будь-якої формули логіки предикатів встановлює, логічно общезначима формула чи ні.
- Обчислення висловлювань є несуперечливої, повної, можливо розв'язати теорією.