Исторически понятие формальной теории было разработано в период интенсивных исследований в области оснований математики для формализации собственно логики и теории доказательства. Сейчас этот аппарат широко используется при создании специальных исчислений для решения конкретных прикладных задач.
Выводимость
Пусть F1, …, Fn, G — формулы теории Т, то есть F1, …, Fn, G являются ППФ. Если существует такое правило вывода R , что (F1, …, Fn, G) Î R, то говорят, что формула G непосредственно выводима из формул F1, …, Fn по правилу вывода R. Обычно этот факт записывают следующим образом:
, где формулы F1, …, Fn называются посылками, а формула G – заключением.
ЗАМЕЧАНИЕ. Обозначение правила вывода справа от черты, разделяющей посылки и заключение, часто опускают, если оно ясно из контекста.
Если в теории Т существует вывод формулы G из формул F1, …, Fn, то это записывают следующим образом:
F1, …, Fn├ Т G, где формулы F1, …, Fn называются гипотезами вывода. Если теория Т подразумевается, то ее значение обычно опускают.
Если ├ Т G, то формула G называется теоремой теории Т (то есть теорема – это формула, выводимая только из аксиом, без гипотез).
Если Г├ Т G, то Г, D├ Т G, где Г и D- любые множества формул (то есть при добавлении лишних гипотез выводимость сохраняется).
Правила вывода делятся на прямые и непрямые. Прямые правила вывода – это правила непосредственного перехода от одних формул к другим, т.е. переход от посылки к заключению. Им сопоставляются определенные шаги формального вывода. Непрямые правила вывода суть правила перехода от одних формальным выводам к другим. Таким правилам соответствуют мета утверждения о преобразованиях одних формальных выводов в другие.
Еще одним интересным способом рассуждения, который может быть оформлен в виде непрямого производного правила, является метод доказательства от противного. Суть его сводится к следующему. Пусть нам надо доказать вывод формулы А из посылок Г. Тогда применяют следующий формальный прием: отрицание формулы А добавляют к множеству формул Г и пытаются получить из посылок ØА, Г противоречие. Если такое противоречие получено, то это означает, что можно построить вывод А из Г
Синтаксис
Синтаксисом называется набор правил конструирования ППФ.
Семантика
Семантикой называется набор правил интерпретации формул.
Интерпретация
Интерпретацией называется приписывание формуле одного из двух значений истинности: 1 (истинно) или 0 (ложно). Композиционность семантики заключается в том, что приписываемое значение истинности некоторой формулы зависит от значений истинности составляющих высказываний и структуры формулы.