Определение формального исчисления

Введем общее понятие формального исчисления. Будем говорить, что формальное исчисление I определено, если выполняются четыре условия.

1. Имеется некоторое множество А символов – алфавит исчисления I. Конечные последовательности символов называются словами или выражениями исчисления I. Обозначим через S множество всех слов алфавита исчисления I.

2. Задано подмножество F S, называемое множеством формул исчисления I. Элементы множества F называются формулами.

3. Выделено множество Ах F формул, называемых аксиомами исчисления I.

4. Имеется конечное множество K отношений R₁, R₂, …, R_n между формулами, называемых правилами вывода, причем если (φ ₁, …, φ _m, φ) R_i, то φ называется непосредственным следствием формул φ ₁, …, φ _m по правилу R_i.

Итак, исчисление I есть четверка (А, F, Ах, K).

Выводом в исчислении I называется последовательность формул φ ₁, φ ₂, …, φ _n такая, что для любого i (1≤ i≤ n) формула φ _i есть либо аксиома исчисления I, либо непосредственное следствие каких-либо предыдущих формул.

Формула φ называется теоремой исчисления I, выводимой в I, или доказуемой в I, если существует вывод φ ₁, …, φ _n, φ, который называется выводом формулы φ или доказательством теоремы φ;.

Вообще говоря, может не существовать алгоритма, с помощью которого для произвольной формулы φ через конечное число шагов можно определить, является ли φ выводимой в исчислении I или нет. Если такой алгоритм существует, то исчисление называется разрешимым. Исчисление называется непротиворечивым, если не все его формулы доказуемы.