Исчисления. Слово «исчисление» ещё не встречается в «Толковом словаре живого великорусского языка» (1863-1866) Владимира Даля в качестве отдельной статьи, хотя слово «исчислить» встречается несколько раз. В «Толковом словаре русского языка» (2006) С.И. Ожегова и Н.Ю. Шведовой также встречается слово «исчислить» в общепринятом «вычислить», «высчитать», а слово «исчисление» рассматривается как существительное, используемое в специальной математической терминологии для обозначения дифференциального и интегрального исчислений, например. Можно заметить, что толковый словарь Ожегова и Шведовой продолжает линию трактовки данного термина, заложенную уже в «Энциклопедическом словаре Брокгауза и Ефрона» (1890-1907), где он определяется как название «отдельных частей математики» (вариационного исчисления, дифференциального и интегрального исчислений и исчисления конечных разностей).

Развернутое пояснение общеупотребимого содержания понятия исчисление дается только в третьем издании «Большой Советской Энциклопедии» (1972), в статье, написанной Ю.А. Гастевым – известным ученым, логиком, осуществившим, в частности, в 1973 году перевод на русский язык «Математической логики» С.К. Клини. Гастев определяет исчисление, как «основанный на чётко сформулированных правилах формальный аппарат оперирования со знаками определённого вида, позволяющий дать исчерпывающе точное описание некоторого класса задач, а для некоторых подклассов этого класса (лишь для наиболее простых исчислений, совпадающих с ним) — и алгоритмы решения». Примерами исчислений выступают: совокупность правил оперирования с цифрами, т.е. числовыми символами в арифметике, «буквенное» исчисление в элементарной алгебре, вышеупомянутые дифференциальное и интегральное исчисления, а также вариационное и другие направления математического анализа и теории функций.

Как справедливо отмечает Ю.А. Гастев, несмотря на раннее происхождение, термин «исчисление» употреблялся в математике до последней трети двадцатого века без строгого общего определения. Необходимость в формулировке подобного определения, как и общей теории исчислений, возникла с развитием математической логики, когда данный термин стал подвергаться «более последовательной формализации». С этого момента исчисление стало пониматься как некое целое, система, включающая, главным образом, три следующих составляющих: 1) некоторый алфавит – совокупность простейших, элементарных символов, которые, по аналогии с алфавитом естественного языка, могут быть названы буквами; однако, в отличие от естественного языка, количество таких букв может считаться (в различных исчислениях) бесконечным – несмотря на то, что число таких букв конечно; 2) любая последовательность таких простейших символов объявляется словом, но при построении исчисления нас интересуют не все возможные слова, которые из данных символов могут быть построены, а только те, которые построены по определенным правилам – правилам образования; такие, построенные по точно сформулированным правилам образования последовательности элементарных знаков называются формулами (если снова воспользоваться аналогией с естественным языком, то можно считать их «словами»); 3) некоторые из таких «правильно построенных» выражений объявляются аксиомами, а из них с помощью правил преобразования (или, иначе, правил вывода) «выводятся» новые формулы, которые называются теоремами данного исчисления.

Исчисления, понимаемые подобным образом, могут быть отождествлены с формальными теориями, или формальными системами, поэтому многие ученые считают выражения «исчисление» и «формальная теория» тождественными по смыслу и значению. Особенностью исчислений, понимаемых исключительно как формальные системы, является то, что все три вышеуказанные группы выражений – простейшие знаки (формальные символы), выражения, построенные из этих знаков по правилам образования (формулы), и последовательности формул, построенные по правилам преобразования, рассматриваются как автонимные – то есть обозначающие самих себя. Поэтому о подобном способе построения теорий также часто говорят, что это – синтаксис, а семантикой называют такой способ построения исчислений, при котором все группы вышеуказанных выражений допускают интерпретацию – то есть какое-либо приписывание им значений. Представление содержательных логических и математических теорий в виде формализованных языков и исчислений составляет характерную особенность современной математической логики.

О формальных и дедуктивных системах, как синонимах исчислений, говорят и авторы статьи «Исчисление» в «Большой Российской Энциклопедии» (2008) весьма авторитетные специалисты – С.И. Адян и Л.Д. Беклемишев. Они рассматривают понятие исчисление как столь же фундаментальное, сколь и понятие алгоритма, поскольку «в частности, класс множеств, которые могут быть заданы с помощью исчисления, совпадает с классом алгоритмически перечислимых множеств». Специальные виды исчислений широко используются в математике для задания алгебраических систем (групп, полугрупп и др.), в математической лингвистике – для описания грамматик формальных языков, а в информатике – для описания синтаксиса языков программирования. Примерами полностью разработанных формализованных систем были логические системы Готлоба Фреге и Давида Гильберта.

В чем же особенность исчисления высказываний и исчисления предикатов по сравнению с дифференциальным, интегральным, вариационным и другими математическими исчислениями? Они считаются логическими, и это совершенно справедливо, и именно об этом нам сообщают авторы "Словаря по логике" и "Краткого словаря по логике" - Д.П. Горский, А.А. Ивин и А.Л. Никифоров.

«Логическое исчисление строится на базе некоторого формализованного языка, [в котором] задается набор исходных символов, из которых c помощью четко определенных правил строятся формулы рассматриваемого исчисления. Некоторые из этих формул выбираются в качестве аксиом, из которых с помощью правил преобразования получают новые формулы, называемые теоремами. После того как к исчислению добавляется интерпретация, придающая значение ее исходным символам и формулам, исчисление превращается в язык, описывающий некоторую предметную область».

Обратим внимание на такой забавный нюанс: в словарях Горского, Ивина и Никифорова в обеих версиях в статьях Исчисление присутствует ссылка на статьи "См. Исчисление высказываний" и "См. Исчисление предикатов" в этих словарях, которые в действительности отсутствуют.

Выводом (или доказательством) в данном исчислении называют конечную последовательность формул, всякий элемент которой либо является аксиомой, либо получается из предшествующих ему элементов по одному из правил вывода. Последние формулы вывода называют выводимыми формулами или теоремами данного исчисления. Для логического исчисления указанного типа часто используется термин «формальная (аксиоматическая) теория». Иногда этот термин относят не только к чисто синтаксису исчислений, описывающему формальный процесс порождения определённых цепочек символов, но и к исчислению, снабжённому семантикой, т. е. интерпретацией, определяющей смысл формул рассматриваемого языка.

В исчислении высказываний формально-аксиоматическим методом изучаются сложные (составные) высказывания, составленные из простых (элементарных, не анализируемых) высказываний с помощью логических связок «и», «или», «если..., то» и «неверно, что». При этом ставится цель охарактеризовать общезначимые в том или ином смысле высказывательные формы, т. е. те формулы, которые при любой подстановке высказываний вместо переменных дают высказывания, верные в соответствующем смысле. Теоремами этого исчисления являются в точности все тавтологии – формулы, отвечающие тождественно истинным булевым функциям. Отсюда следует алгоритмическая разрешимость, т.е. существование алгоритма, распознающего теоремы данного исчисления.

За формальную точность в исчислении высказываний и в исчислении предикатов приходится расплачиваться подробностью и объемом доказательств.

Например, в гильбертовом (классическом) исчислении высказываний в его представлении Клини:

доказательство дистрибутивности дизъюнкции относительно конъюнкции только в одну сторону будет иметь 25 следующих шагов:

Вот что об изучении исчислений в математической логике пишут академик Российской академии наук Ю.Л. Ершов и профессор кафедры алгебры и математической логики Новосибирского государственного университета Е.А. Палютин (Ершов Ю.Л., Палютин Е.А. Математическая логика. – 6-е изд., испр. – М.: ФИЗМАТЛИТ, 2011. С.11. – ISBN 978-5-9221-1301-4): «Изучение исчислений составляет синтаксическую часть математической логики. Наиболее глубокое изучение (синтаксического) понятия доказательства в тех или иных исчислениях составляет самостоятельный раздел математической логики, который носит название теории доказательств. Наряду с синтаксическим изучением исчислений проводится также семантическое изучение формальных языков математической логики. Основным понятием семантики является понятие истинности для выражений (формул, секвенций и т. п.) формального языка. Семантические понятия также получили точные математические определения, что дало возможность систематического и строгого изучения различных понятий истинности. Классическая семантика языка исчисления предикатов составила весьма богатый раздел математической логики — теорию моделей, которая активно развивается, а ее методы и результаты успешно применяются и в других областях математики (алгебре, анализе). Основателями теории моделей являются А. Тарский и А. И. Мальцев».

Как заявляют авторы в их учебном издании «Математической логики»: «Изложение исчисления высказываний и исчисления предикатов не является традиционным и начинается с изучения секвенциальных вариантов исчислений натурального вывода (хотя традиционные исчисления также появляются здесь под названием гильбертовских). Основанием к этому являются: 1) возможность хорошего объяснения смысла всех правил вывода; 2) возможность более быстрого приобретения навыка формальных доказательств; 3) практическая возможность проделать все необходимые в курсе формальные доказательства в таких исчислениях. Многолетний опыт чтения старшим из авторов курса математической логики на математическом факультете Новосибирского государственного университета … показывает, что указанные выше возможности вполне реализуются».