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

Формальная теория (или исчисление) - это:

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

2. множество F слов в алфавите A, FÌA, которые называются формулами;

3. подмножество В формул, BÌF, которые называются аксиомами;

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

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

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

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

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

Итак, исчисление есть четверка (A, F, В, R).

Выводом в исчислении называется последовательность формул F₁,F₂,...,F_n такая, что для любого k (1≤kn) формула F_k есть либо аксиома исчисления либо непосредственное следствие каких-либо предыдущих формул, полученное по правилу вывода.

Формула G называется теоремой исчисления (выводимой в или доказуемой в , если существует вывод F₁,F₂,...,F_n,G который называется выводом формулы G или доказательством теоремы G. Записывается это следующим образом:

F₁,F₂,...,F_n+ G.

Исчисление называется непротиворечивым, если не все его формулы доказуемы. Можно дать другое определение непротиворечивости: Исчисление называется непротиворечивым, если в нем не являются выводимыми одновременно формулы F и ┐F (отрицание F).

Исчисление называется полным (или адекватным), если каждому истинному высказыванию М соответствует теорема теории

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

Дата добавления: 2014-01-04