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

2.8.1. Определение формальной теории

Формальная теория Т это:

1) Множество A символов образующих алфавит;

2) Множество F слов в алфавите А которые называются

формулами;

3) Подмножество Аx формул (), которые называются аксиомами;

4) Множество R отношений на множестве формул, которые называются правиламивывода.

Таким образом формальная теория Т есть четвёрки < A, F, Ax, R >.

Обычно для образования символов А используются конечные множества.

Множество формул F задается индуктивным определением с помощью формальной грамматики. Это множество, как правило, бесконечно.

Множества А и F в совокупности определяют язык или сигнатуру формальной теории.

Множество аксиом Аx может быть конечным или бесконечным. Бесконечное множество аксиом задается с помощью конечного множества схем аксиом и правил порождения аксиом из схем аксиом.

Множество правил вывода R обычно конечно.

Факт вывода формулы G непосредственно из формул по правилу вывода R записывается следующим образом:

.

При этом формулы называется посылками, а G - заключением.

Выводом формулы G из формул формальной теории T называется последовательность формул , в которой последняя формула , а любая другая формула - либо аксиома, либо исходная формула , либо непосредственно выводима из предыдущих формул.

Этот факт записывается так:

G.

При этом называются гипотезами вывода.

Если G, то формула G называется теоремой теории, то есть формула выводится из аксиом (без гипотез).

Интерпретацией формальной теории Т в области интерпретации М называется функция , которая каждой формуле F формальной теории Т однозначно сопоставляет некоторое содержательное высказывание относительно объектов множества М. Интерпретация I называется моделью формальной теории Т, если все теоремы этой теории выполняются в интерпретации I.

Формула называется общезначимой (тавтологией) если она истина в любой интерпретации.

Формула называется противоречивой, если она ложна в любой интерпретации.

Формальная теория Т называется непротиворечивой, если хотя бы одна ее теорема не является противоречием.

Формальная теория Т является полной (адекватной), если каждому истинному высказыванию М соответствует теорема в теории Т.

Если для множества М существует формальная полностью не противоречивая теория Т, то М называется аксиоматизируемым (формализуемым).

Система аксиом формально не противоречивой теории Т называется независимой, если никакая из аксиом не выводится из остальных по правилам вывода теории Т.

Формальная теория Т называется разрешимой, если существует алгоритм, который для любой формулы теории определяет, является ли эта формула теоремой теории или нет.