-
исчисление,
символы и правила которого могут быть интерпретированы в терминах логики. Любое исчисление представляет собой знаковую систему, которая, как чисто синтаксическая
структура, однозначно определяется двумя порождающими процедурами: 1)
образованием элементов синтаксических категорий, т. е. правильных выражений
языка исчисления из символов его алфавита; 2) преобразованием синтаксических выражений исчисления посредством системы аксиом и правил
вывода. Аксиомы представляют собой фиксируемый в языке исчисления набор исходных выражений, принимаемых непосредственно (как
постулаты). Правила вывода - это правила вида "из формул F1, ..., Fm выводима формула G", символическая запись: (F1, ..., Fm) G. Формулы F1, ..., Fm называются посылками вывода, a G - заключением вывода. В каждом конкретном правиле формулы F1, ..., Fm, G имеют конкретный вид,
число посылок (m) также принимает
конкретное значение. Приписывание символам исчисления значений, т. е.
интерпретация, превращает исчисление в семантическую систему (
формализованный язык). И. л. представляет собой логически интерпретированное исчисление, изучение которого предполагает тщательное построение и
анализ трех металогических уровней языка: синтаксического, семантического и прагматического.
Доказательством формулы F в И. л. называется последовательность формул HI, ..., Hm, F, в которой каждая формула - либо
аксиома исчисления, либо выводима из некоторых предыдущих (т. е. уже доказанных) формул с помощью одного из правил вывода. Для каждого И. л. важное значение имеют
вопросы о его непротиворечивости (в непротиворечивом исчислении не выводимы одновременно какое-либо
выражение и его
отрицание), полноте (исчисление является полным, если множество его истинных утверждений совпадает с множеством утверждений, доказуемых в нем), решении проблемы разрешимости (исчисление является разрешимым, если существует
алгоритм, позволяющий для любого утверждения определять, выводимо оно в нем или нет) и др.
Решение данных вопросов определяет логическую
возможность интерпретации исчисления и является необходимым
условием его практической реализуемости, Различные теории вывода представляют И. л., отличающиеся своими свойствами. А. Г. Кислое
