Форма́льна систе́ма (форма́льна тео́рія, аксіомати́чна тео́рія) (англ. formal system) — абстрактна структура та формалізації аксіоматичної системи (теорії), яка використовується для виведення теорем з аксіом за допомогою набору правил виведення.^[1]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Геометрія

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

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

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

Формальна аксіоматична теорія числення висловлень є повною відносно своєї моделі алгебри висловлень.

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

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

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

• Рудик О. Б. Числення висловлювань і предикатів // Інформатика та інформаційні технології в навчальних закладах. — Київ : КУБГ, 2013.
• Галиев Ш. И. Математическая логика и теория алгоритмов. — Казань : Издательство КДТУ им. А. Н. Туполева, 2002. (рос.)
• Клини С. Введение в математику. — М. : ИЛ, 1957. (рос.)
• Клини С. Математическая логика. — М. : Мир, 1973. (рос.)
• Мендельсон Е. Введення в математичну логіку. — М. : Наука, 1971. (рос.)
• Новиков Ф. А. Дискретная математика для программистов. — СПб. : Питер, 2000. (рос.)
• Яновская С. А. Из истории аксиоматики // Историко-математические исследования. — М. : ГИТТЛ, 1958. — С. 63-96. (рос.)

• Повна у вузькому розумінні логічна система // Літературознавча енциклопедія : у 2 т. / авт.-уклад. Ю. І. Ковалів. — Київ : ВЦ «Академія», 2007. — Т. 2 : М — Я. — С. 226.

• Теорія множин
• Формальна логіка
• Формалізм (математика)
• Система кодування
• Автоформалізація
• Gödel, Escher, Bach

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

• Теорії першого порядку
  • Числення висловлень
  • Числення предикатів першого порядку
  • Формальна арифметика
  • Аксіоматична теорія множин
  • Теорія груп
• Теорії вищих порядків
• Лямбда-числення
  • Лямбда-числення з типами
  • Числення конструкцій
  • Числення індуктивних конструкцій