КОНСТРУКТИВНЫЕ ЛОГИКИ

Еще в 1908 г. голландский аспирант (Э.Л.Я. Брауэр опубликовал на голландском языке диссертацию под наглым названием: «De onbetrouwbaarheid der logische principes», что означает «Недостоверность логических принципов». Брауэр аргументировал, что причина тех неприятностей, с которыми столкнулась математика в начале XX века (и которые не преодолены и до сих пор; к ним просто привыкли и стали игнорировать), не в каких-то частных принципах теории множеств, а в самой логике[5].

Логика создавалась для конечных объектов, а перенесли её на бесконечные. В частности, для бесконечных объектов нельзя считать автоматически выполненным закон исключенного третьего « или не » (на символическом языке современной логики ), поскольку мы можем просто не уметь распознать эти два случая. Брауэр показал, что закон исключенного третьего в обычной логике эквивалентен ещё одному общепринятому закону: снятия двойного отрицания , который в курсе математики выступает в качестве доказательств от противного: «Нужно доказать A . Предположим, что не верно A … Получаем абсурд. Полученное противоречие доказывает теорему» Как всегда у первооткрывателей, гениальные прозрения у Брауэра сочетались с некорректными объяснениями. Если причина недоразумений в самой логике, почему же эллины, создавшие и отработавшие классическую логику на примере геометрии, в которой также рассматривается бесконечная совокупность объектов, ни с какими неприятностями, проистекающими от нее, не сталкивались? Да дело просто в том, что гениальная интуиция и потрясающее чувство гармонии эллинов воспрепятствовали им использовать в геометрии числа. Тем самым они избежали попадания в область неразрешимых проблем. А, как показал Гёдель, там, где появляются натуральные числа, возникают и неразрешимые проблемы. Но, конечно же, неразрешимые проблемы возникают лишь для бесконечных совокупностей объектов. А там, где возникают неразрешимые проблемы, закон исключенного третьего выглядит до глупости оптимистичным: как мы можем утверждать, что или не, когда мы в принципе не можем знать ни того, ни другого? Но самое важное у Брауэра было то, что он полностью видоизменил приоритеты математики[6].

Если традиционная математика занимается поиском и доказательством теорем, то он начал её рассматривать как источник построений. Мало доказать теорему, нужно, чтобы обоснование дало нам построение объекта, существование которого утверждается в теореме. А использование доказательств в качестве источника построений — именно то, что нужно от математики информатику .

Конструктивная логика - раздел математической логики, изучающий рассуждения о конструктивных объектах и конструкциях. При таком понимании конструктивная логика шире, чем логика конструктивной математики. Самое заметное отличие от традиционной (классической) логики состоит в отсутствии исключенного третьего закона и двойного отрицания закона

При обозначении систем чистой логики (исчисление высказываний, предикатов) термины "конструктивное", "интуиционистское", "гейтинговское" часто считаются синонимами (см. Рейтинга формальная система). Под конструктивной арифметикой иногда понимают гейтпнговскую арифметику, а иногда - ее расширение, получаемое добавлением принципа Маркова и схемы выражающей эквивалентность формулы и утверждения о ее реализуемости. Эта расширенная система, достаточная для доказательства основных результатов конструктивного математического анализа, не является, в отличие от гейтинговских систем, подсистемой классической арифметики: в ней опровергается закон исключенного Иногда к конструктивной логике относят системы интуиционистской логики, содержащие средства описания специфически интуиционистских понятий. Общая черта подавляющего большинства систем К. л., отражающая специфику конструктивного понимания связки и квантора - явная реализация этих связок: выводимость (соответственно существование хА (х)) влечет выводимость одной из формул А, В (соответственно A(t) для некоторого терма t). При этом в случае прикладных систем (арифметика, анализ) требуется замкнутость рассматриваемых формул. Большинство систем К. л. (включая все гейтинговские системы) корректны относительно различных понятий реализуемости, включая реализуемость по Клини и Гёделя интерпретацию: все выводимые формулы реализуемы, в частности истинны, в конструктивной семантике. С другой стороны, формальные системы К. л. обычно неполны относительно естественной конструктивной семантики. Для систем, содержащих арифметику, это следует из Гёделя теоремы о неполноте.

Множество реализуемых предикатных формул неперечислимо, поэтому конструктивное исчисление предикатов неполно относительно реализуемости, а из его полноты относительно "наивной" конструктивной семантики следовала бы интуиционистская истинность принципа 'конструктивного подбора. Конструктивное исчисление высказываний также неполно относительно реализуемости, но полно при некоторой интерпретации в терминах систем Поста. Арифметическая полуформальная система, полная относительно конструктивной семантики Маркова - Шанина, получается, если добавить к формальной конструктивной арифметике со схемой и принципом конструктивного подбора эффективное w-правило: из А(0), А(1), . . . вывести Для гейгинговских систем установлены теоремы полноты относительно теоретико-модельных семантик Крипке и Бета, использующих "возможные миры" (эти семантики связаны с теоретико-множественным вынуждением), а также относительно алгебраических и топологических моделей.

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

В некоторых системах К. л. справедливы суждения, ложные при классическом истолковании, например, отрицание закона исключенного третьего или специфически интуиционистские утверждения о последовательностях. Такие системы S сводятся к классическим системам с помощью подходящего понятия реализуемости р. Доказывают, что влечет существование t такого, что причем если А- числовое равенство, то Отсюда следует непротиворечивость S относительно

Конструктивная логика исследует истинность суждений также в нетрадиционных языках, отличных от языков логики предикатов арифметики, анализа и т. д. Наряду с традиционным отрицанием основанным на приведении к противоречию, изучается сильное отрицание предусматривающее построение контрпримера. Для справедливы многие из законов классической логики, например.

но теорема об эквивалентной замене верна лишь в виде

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

Безотрицательная логика Грисса - Нельсона стремится избежать использования отрицания и ограничить класс свойств, о которых делаются утверждения, такими, для которых уже построены объекты, удовлетворяющие этим свойствам. Язык такой логики содержит связку причем понимается приблизительно как

В теории конструкций исследуются сами правила построения и доказательства, лежащие в основе конструктивной математики. Конструкции строятся из исходных с помощью фиксированного набора комбинаторов и операции применения функции к аргументу. Формулы строятся из равенства с помощью связок логики высказываний и предиката доказуемости я, причем p(a, х-a(х)) читается "а есть доказательство того, что a(х) верно для всех x". В качестве аксиом берутся, в частности, все классические тавтологии (включая закон исключенного третьего), т. е. отношение "быть доказательством" предполагается разрешимым. Имеется корректная и точная интерпретация гейтинговских систем в теории конструкции.

Рассмотрение в конструктивной логике бескванторных систем вызвано стремлением получить финитные (в том или ином смысле) доказательства рассматриваемых суждений или их мажорант. Многие традиционные системы SК. л. погружаются в бескванторные системы S~ таким образом, что выводимость в S-суждения с бескванторной формулой R влечет выводимость в S-формулы R(x,j(х)). для подходящего j. Если S- арифметика без индукции, то S-примитивно рекурсивная арифметика; если S- гейтинговская арифметика, то S- - система гёделевских примитивно рекурсивных функционалов.

Для формальных систем конструктивной логики доказаны теоремы нормализации: любой вывод может быть конечным числом стандартных преобразований (редукций) приведен к нормальной форме, не содержащей "лишних" участков. Нормальные выводы обладают (в полной мере или, в случае арифметики и более широких систем, частично) свойством подформульности.

Имеются связи между конструктивной логикой и теорией категорий. Так, понятию "декартовой замкнутой категории" соответствует гейтинговское исчисление высказываний.

Иногда к конструктивной логике относят все логические рассмотрения, в которых требуется, чтобы все изучаемые объекты были конструктивными, независимо от применяемой логики. С этой тенденцией связано название конструктивных по Гёделю множеств.