Конструктивная логика А. А. Маркова

Проблема конструктивного понимания логических связок, в частности отрицания и импликации, требует применения в ло­гике специальных точных формальных языков. В основе конст­руктивной математической логики А. А. Маркова лежит идея ступенчатого построения формальных языков. Сначала вводится формальный язык Я_о , в котором предложения выражаются по

определенным правилам в виде формул; в нем имеется определе­ние смысла выражения этого языка, т. е. семантика. Правила вывода позволяют, исходя из верных предложений, всегда полу­чать верные предложения.

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

Новое понимание логических связок требует новой логики. Мы считаем утверждение А. А. Маркова о неединственности логики верным и весьма глубоким: «В самой идее неединствен­ности логики, разумеется, нет ничего удивительного. В самом деле, с какой стати все наши рассуждения, о чем бы мы ни рассуждали, должны управляться одними и теми же законами? Для этого нет никаких оснований. Удивительным, наоборот, было бы, если бы логика была единственна»³⁹.

В конструктивную математическую логику А. А. Марков вводит понятие «разрешимое высказывание» и связанное с ним понятие «прямое отрицание». В логике А. А. Маркова имеется и другой вид отрицания — усиленное отрицание, относящееся к так называемым полуразрешимым высказываниям.

Кроме материальной и усиленной импликации, при установ­лении истинности которых приходится заботиться об истинности посылки и заключения, А. А. Марков вводит дедуктивную имп­ликацию, определяемую по другому принципу. Дедуктивная имп­ликация «если А, то В» выражает возможность выведения В из А по фиксированным правилам, каждое из которых в применении к верным формулам даст верные формулы. Всякое высказывание, выводимое из истинного высказывания, будет истинным.

Через дедуктивную импликацию А. А. Марков определяет редукционное отрицание (reductio ad absurdum). Редукционное отрицание высказывания А (сформулированного на данном язы­ке) понимается как дедуктивная импликация «если А, то Л», где через Л обозначен абсурд. Это определение отрицания соответ­ствует обычной практике рассуждений математика: математик отрицает ту посылку, из которой вытекает абсурд. Для установ­ления истинности редукционного отрицания высказывания не требуется вникать в смысл этого высказывания. Высказывание, для которого установлена истинность редукционного отрицания, не может быть истинным.

Эти три различных понимания отрицания не вступают в конф­ликт друг с другом, они согласованы, что, по мнению А. А. Маркова, даст возможность объединить все эти понимания отрицания.

Показательно такое обстоятельство: А. А. Марков строит свои конструктивные логические системы для обоснования конст­руктивной математики таким образом, что у него получается не одна законченная система, а целая иерархия систем. Это система языков Я ₀, Я ₁ Я ₂, Я ₃, Я ₄, Я ₅,..., Я _N (где N — натуральное число) и объемлющего их языка Я _ω после Я _ω строится язык Я _{ω `}.

Итак, мы склонны думать, что развивающуюся конструктив­ную логику и математику невозможно вместить в одно формаль­ное исчисление, для этого нужна система, состоящая из целой иерархии систем, в которой будет иерархия отрицаний.

Проблемами конструктивной логики и теории алгоритмов занимается российский математик Н. М. Нагорный и др.