Математична логіка Дедуктивна теорія
У математичній теорії велике значення має дедуктивна теорія. Термін дедукція походить від лат. deductio - виведення. Таким чином, дедукція - це один з основних способів міркування та методів дослідження.
Дедуктивну теорію прийнято вважати заданою у разі, якщо:
- Заданий алфавіт, тобто безліч, і правила утворення виразів у цьому алфавіті.
- Задано правила утворення формул.
- Виділено підмножину теорем, які доводять формулу.
Існує кілька способів побудови безлічі теорем:
1.Завдання аксіом та правил виведення
У багатьох формул виділяється підмножина аксіом, після чого задається кінцеве число правил виведення. Правило виведення - це правила, за допомогою яких з аксіом і раніше виведених теорем можна отримати нові теореми. До теорем входять всі аксіоми. Однак відомі випадки (наприклад, в аксіоматиці Пеано), коли теорія містить безліч аксіом, заданих за допомогою однієї або декількох схем аксіом. Подібні аксіоми прийнято називати «прихованими визначеннями».
Цей спосіб дозволяє задавати формальні аксіоматичні теорії.
2.Завдання лише аксіом
У цьому випадку правила виведення вважаються загальновідомими, тому задаються лише аксіоми. Тому за такої побудови теорем, кажуть, що напівформальна аксіоматична теорія .
3.Завдання лише правил виведення
Даний спосіб побудови теорем ґрунтується на завданні лише правил виведення, оскільки безліч аксіом порожня. Виходячи з цього, теорія, задана таким чином, є окремим випадком формальної теорії. Пізніше цей різновид став називатися теорією природного висновку.
Суперечливоюназивається теорія, в якій безліч теорем покриває безліч формул. В іншому випадку, теорія є несуперечливою. Головним і складним завданням формальної логіки є виявлення суперечливості теорії. Суперечливі теорії, як правило, не мають подальшого практичного та теоретичного застосування.
2. Повнота
Повною називається теорія, в якій для будь-якої формули F виводиться або сама F, або її заперечення -F. У тому випадку, якщо теорія містить твердження, що недоказуються, тобто твердження, які не можна ні довести, ні спростувати засобами самої теорії, вона називається неповною.
3. Незалежність аксіом
Коли окрему аксіому теорії не можна вивести з інших аксіом, її називають незалежною . Залежна аксіома є надмірною, тому її вилучення з системи аксіом не відбивається на теорії. Система аксіом називається незалежною лише тому випадку, якщо кожна аксіома у ній незалежна.
4. Дозвіл
Коли теорії існує ефективний алгоритм, що дозволяє визначити кількість кроків, що доводять теорему, теорія називається розв'язною .
Наприклад, логіка висловлювань, логіка першого порядку (обчислення предикатів), формальна арифметика (теорія S).