О независимых принципах в совместной логике задач и высказываний. Часть 1

Поскольку аксиомы логики задач и высказываний QHC являются попыткой более полной (по сравнению с обычными аксиомами интуиционистской логики) формализации наиболее известных интуитивных “объяснений” интуиционистской логики (а именно, задачной интерпретации Колмогорова–Гейтинга–Крайзеля и доказуемостной интерпретации Орлова–Гейтинга–Гёделя – которые с точки зрения аксиом QHC имеют непустое пересечение, но не сводятся друг к другу), представляет самостоятельный интерес исследование принципов, выразимых в языке логики QHC, но не доказуемых и не опровержимых в ней.
Если ограничиться рассмотрением принципов, добавление которых к QHC не нарушает её консервативности ни над интуиционистской, ни над классической логикой, то из нескольких десятков бескванторных схем, выражающих простейшие напрашивающиеся предположения о возможностях QHC (в основном это эквивалентности, в которых одна из импликаций легко выводится из аксиом), каждая оказывается равносильной одному из 6 принципов; все импликации между этими 6 принципами установлены. С учётом кванторов добавляется ещё не более 6 принципов. Некоторые попарные конъюнкции данных 12 принципов уже не консервативны над интуиционистской логикой – и имеют в качестве следствий (а иногда даже в качестве эквивалентных переформулировок) принцип де Моргана, сильный принцип Маркова, принцип сдвига двойного отрицания, принцип постоянной области, принцип независимости от посылки.
Львиная доля содержательных переформулировок почему-то приходится на два из 12 упомянутых принципов – ровно те из них, которые были высказаны (в неформальном виде) уже Гильбертом и Колмогоровым. Оба этих принципа (в их исторической форме) относятся к вариациям интуиционистских понятий “разрешимости” ($\alpha\lor\neg\alpha$) и “стабильности” ($\neg\neg\alpha\to\alpha$). В логике QHC кроме разрешимых и стабильных задач естественным образом обнаруживаются также разрешимые и стабильные высказывания, а также полустабильные и полуразрешимые задачи и высказывания. Принцип стабильности Колмогорова (сформулированный им в письме к Гейтингу, опубликованном лишь в 1988 г.) состоит в том, что всякое предложение есть либо задача (в смысле, вполне согласующемся с интуиционистской логикой), либо “экспериментально проверяемое” высказывание; с учётом формальных свойств “экспериментально проверяемых” высказываний, явно указанных Колмогоровым, в рамках логики QHC естественно отождествить их со стабильными (или, эквивалентно, полустабильными) высказываниями (а не только с высказываниями типа $\Pi_1$).
Гильбертов принцип “non ignorabimus” (о разрешимости всякой математической проблемы, “либо в форме фактического ответа на поставленный вопрос, либо через доказательство невозможности его решения”) был сформулирован им в предисловии к известному списку из 23 проблем, и спустя 25 лет дословно повторен в статье, содержащей набросок (ошибочного) доказательства континуум-гипотезы, “первый и важнейший шаг которого состоит в доказательстве разрешимости всякой математической проблемы”. Хотя утверждение Гильберта о том, что всякий математик разделяет его убеждение о разрешимости всех математических проблем, было вскоре опровергнуто Брауэром (не разделявшим этого убеждения ни в каком виде), Гильберт недвусмысленно указывал, что он говорит не об общем методе решения, а лишь о его существовании в каждом отдельно взятом случае. Поэтому в QHC гильбертов принцип “non ignorabimus” (отсылающий к латинской максиме “ignoramus et ignorabimus”, кодирующей в свою очередь популярную в конце 19-го века позицию в естествознании, отстаивавшуюся Э. Дюбуа-Реймоном) естественно понимать как полуразрешимость (или, эквивалентно, полустабильность) всех задач. В таком виде этот принцип оказывается весьма далёк от принципа разрешимости всех задач одним общим методом, отвергаемого в интуиционистской логике (и обычно отождествляемого интуиционистами вслед за Брауэром с принципом исключённого третьего для высказываний – чего конечно не следует делать при подходе Колмогорова, на котором основана логика QHC). Действительно, не только гильбертов “non ignorabimus”, но и принцип стабильности Колмогорова, который оказывается строго более сильным, не влечёт ни метода разрешения всех задач, ни какого-либо другого независимого принципа интуиционистской логики.