Формальна система

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

Формальна система - це сукупність абстрактних об'єктів, не пов'язаних із зовнішнім світом, в якому представлені правила оперування множиною символів в строго синтаксичному трактуванні без врахування смислового змісту, тобто семантики. Строго описані формальні системи з'явилися після того, як була поставлена ​​задача Гільберта. Перші ФС з'явилися після виходу книг Рассела і Уайтхеда «Формальні системи». Цим формальним системам були пред'явлені певні вимоги.

Основні визначення[ред.ред. код]

Формальна теорія вважається визначеною, якщо [2]:

  1. Задано кінцеву або злічену множину довільних символів. Кінцеві послідовності символів називаються виразами теорії.
  2. Є підмножина виразів, званих формулами.
  3. Виділено підмножину формул, званих аксіомами.
  4. Є кінцева множина відношень між формулами, званих правилами виведення.

Звичайно є ефективна процедура, що дозволяє за даним висловом визначити, чи є він формулою. Часто множина формул задається індуктивним визначенням. Як правило, ця множина є нескінченною. Множина символів і множина формул в сукупності визначають мову або сигнатуру формальної теорії.

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

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

Формула називається теоремою, якщо існує виведення, в якому ця формула є останньою.

Теорія, для якої існує ефективний алгоритм, що дозволяє дізнаватися по даній формулі, чи існує її виведення, називається вирішуваною; в іншому випадку теорія називається нерозв'язною.

Теорія, в якій не всі формули є теоремами, називається абсолютно несуперечливою.

Визначення та різновиди[ред.ред. код]

Дедуктивна теорія вважається заданою, якщо:

  1. Задано алфавіт (множина) і правила утворення виразів ( слів) в цьому алфавіті.
  2. Задані правила утворення формул (правильно побудованих, коректних висловів).
  3. З множини формул деяким способом виділено підмножину T теорем (доказових формул).

Різновиди дедуктивних теорій[ред.ред. код]

Залежно від способу побудови множини теорем:

Завдання аксіом і правил висновку[ред.ред. код]

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

Завдання тільки аксіом[ред.ред. код]

Задаються тільки аксіоми, правила виведення вважаються загальновідомими.

При такому завданні теорем кажуть, що задана напівформальна аксіоматична теорія.

Приклади[ред.ред. код]

Геометрія

Завдання тільки правил виводу[ред.ред. код]

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

Властивості дедуктивних теорій[ред.ред. код]

Несуперечність[ред.ред. код]

Теорія, в якій множина теорем покриває всі множини формул (всі формули є теоремами, «істинними висловлюваннями»), називається суперечливою. В іншому випадку теорія називається несуперечливою. З'ясування суперечливості теорії - одна з найважливіших і іноді найскладніших завдань формальної логіки. Після з'ясування суперечливості теорія, як правило, не має подальшого ні теоретичного, ні практичного застосування.

Повнота[ред.ред. код]

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

Незалежність аксіом[ред.ред. код]

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

Розв'язність[ред.ред. код]

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

Найважливіші висновки[ред.ред. код]

  • У 30-і рр.. XX століття Курт Гедель показав, що є цілий клас теорій першого порядку, що є неповними. Більш того, формула, яка стверджує несуперечність теорії, також не виведені засобами самої теорії (див. Теореми Геделя про неповноту). Цей висновок мав величезне значення для математики, так як формальна арифметика (а на ній базується теорія дійсних чисел, без якої не можна уявити сучасну математику) є якраз такою теорією першого порядку, а отже, формальна арифметика і всі теорії, що містять її, у тому числі теорія дійсних чисел, є неповними.
  • Проблема нерозв'язності логіки предикатів. Черчем доведено, що не існує алгоритму, який для будь формули логіки предикатів встановлює, логічно загальнозначуща формула чи ні.
  • Числення висловлень є несуперечливою, повною, вирішуваною теорією, причому всі три твердження доказові в рамках самої логіки висловлювань.

Примітки[ред.ред. код]

  1. {{книга  | Автор = Кліні С. До | заголовок = Введення в метаматематику  | Посилання = http://eqworld.ipmnet.ru/ru/library/books/Klini1957ru.djvu  | Місце = М. | Видавництво = ІЛ | рік = 1957 | сторінки = 59-60 }}
  2. {{книга  | Автор = Мендельсон Е. | заголовок = Введення в математичну логіку  | Посилання = http://eqworld.ipmnet.ru/ru/library/books/Mendelson1971ru.djvu  | Місце = М. | Видавництво = «Наука» | рік = 1971 | сторінки = 36 }}

Література[ред.ред. код]

Див. також[ред.ред. код]

Приклади формальних теорій