Определение формального исчисления
Введем общее понятие формального исчисления. Будем говорить, что формальное исчисление I определено, если выполняются четыре условия. 1. Имеется некоторое множество А символов – алфавит исчисления I. Конечные последовательности символов называются словами или выражениями исчисления I. Обозначим через S множество всех слов алфавита исчисления I. 2. Задано подмножество F 3. Выделено множество Ах 4. Имеется конечное множество K отношений R1, R2, …, Rn между формулами, называемых правилами вывода, причем если (φ 1, …, φ m, φ) Итак, исчисление I есть четверка (А, F, Ах, K). Выводом в исчислении I называется последовательность формул φ 1, φ 2, …, φ n такая, что для любого i (1≤ i≤ n) формула φ i есть либо аксиома исчисления I, либо непосредственное следствие каких-либо предыдущих формул. Формула φ называется теоремой исчисления I, выводимой в I, или доказуемой в I, если существует вывод φ 1, …, φ n, φ, который называется выводом формулы φ или доказательством теоремы φ;. Вообще говоря, может не существовать алгоритма, с помощью которого для произвольной формулы φ через конечное число шагов можно определить, является ли φ выводимой в исчислении I или нет. Если такой алгоритм существует, то исчисление называется разрешимым. Исчисление называется непротиворечивым, если не все его формулы доказуемы.
|
S, называемое множеством формул исчисления I. Элементы множества F называются формулами.
Ri, то φ называется непосредственным следствием формул φ 1, …, φ m по правилу Ri.
