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

 

Введем общее понятие формального исчисления. Будем говорить, что формальное исчисление 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 или нет. Если такой алгоритм существует, то исчисление называется разрешимым. Исчисление называется непротиворечивым, если не все его формулы доказуемы.