Дедуктивная система

Дедуктивная система - это способ задания множества путем указания исходных элементов (аксиом исчисления) и правил вывода, каждое из которых описывает, как строить новые элементы из исходных. Используются различные термины для обозначения понятия дедуктивной системы: исчисление, формальная (аксиоматическая) теория (система). Это синонимы, хотя имеется некий скрытый подтекст: например, исчислениями называют наиболее важные дедуктивные системы, - исчисление высказываний, исчисление предикатов. Когда некоторую неформальную (математическую или содержательную) теорию можно представить в виде дедуктивной системы, например арифметику или теорию множеств, то говорят о формальной теории - формальной арифметике или аксиоматической теории множеств. Когда говорят о языках программирования, предложения которых построены на основе строгих правил таким образом, чтобы для любой последовательности символов можно было сказать, является ли она правильно построенной конструкцией этого языка или нет, то говорят о языке как о формальной системе.