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

- раздел математической логики, изучающий рассуждения о конструктивных объектах и конструкциях. При таком понимании К. л. шире, чем логика конструктивной математики. Самое заметное отличие от традиционной (классической) логики состоит в отсутствии исключенного третьего закона [img: http://localhost:8080/file/021235-5.jpg] и двойного отрицания закона [img: http://localhost:8080/file/021235-6.jpg] При обозначении систем чистой логики (исчисление высказываний, предикатов) термины "конструктивное", "интуиционистское", "гейтинговское" часто считаются синонимами (см. Рейтинга формальная система). Под конструктивной арифметикой иногда понимают гейтпнговскую арифметику, а иногда - ее расширение, получаемое добавлением принципа Маркова (см. Конструктивного подбора принцип)и схемы [img: http://localhost:8080/file/021235-7.jpg] выражающей эквивалентность формулы и утверждения о ее реализуемости (см. Конструктивная семантика). Эта расширенная система, достаточная для доказательства основных результатов конструктивного математич. анализа, не является, в отличие от гейтинговских систем, подсистемой классич. арифметики: в ней опровергается закон исключенного третьего [img: http://localhost:8080/file/021235-8.jpg] Иногда к К. л. относят системы интуиционистской логики, содержащие средства описания специфически интуиционистских понятий. Общая черта подавляющего большинства систем К. л., отражающая специфику конструктивного понимания связки [img: http://localhost:8080/file/021235-9.jpg] и квантора [img: http://localhost:8080/file/021235-10.jpg] - явная реализация этих связок: выводимость [img: http://localhost:8080/file/021235-11.jpg] (соответственно существование хА (х))влечет выводимость одной из формул А, В (соответственно A(t)для нек-рого терма t). При этом в случае прикладных систем (арифметика, анализ) требуется замкнутость рассматриваемых формул. Большинство систем К. л. (включая все гейтинговские системы) корректны относительно различных понятий реализуемости, включая реализуемость по Клини и Гёделя интерпретацию:. все выводимые формулы реализуемы, в частности истинны, в конструктивной семантике. С другой стороны, формальные системы К. л. обычно неполны относительно естественной конструктивной семантики. Для систем, содержащих арифметику, это следует из Гёделя теоремы о неполноте. Множество реализуемых предикатных формул неперечислпмо, поэтому конструктивное исчисление предикатов неполно относительно реализуемости, а из его полноты относительно "наивной" конструктивной семантики следовала бы интуиционистская истинность принципа 'конструктивного подбора. Конструктивное исчисление высказываний также неполно относительно реализуемости, но полно при нек-рой интерпретации в терминах систем Поста. Арифметическая полуформальная система, полная относительно конструктивной семантики Маркова - Шанина, получается, если добавить к формальной конструктивной арифметике со схемой [img: http://localhost:8080/file/021235-12.jpg] и принципом конструктивного подбора эффективное w-правило: из А(0), А(1),... вывести [img: http://localhost:8080/file/021235-13.jpg] Для гейгинговских систем установлены теоремы полноты относительно теоретико-модельных семантик Крипке и Бета, использующих "возможные миры" (эти семантики связаны с теоретико-множественным вынуждением), а также относительно алгебраических и топологических моделей. Классические формальные системы обычно погружаются в соответствующие системы К. л. (с сохранением отношения выводимости из гипотез) с помощью негативного перевода, т. е. приписывания двойного отрицания [img: http://localhost:8080/file/021235-14.jpg] перед всеми подформулами. Поэтому системы арифметики, анализа и типов теории, основанные на классич. логике, изоморфно вкладываются в соответствующие системы, основанные на К. л. Имеются системы теории множеств, основанные на К. л., в к-рые погружаются классич. системы. Гейтинговские системы погружаются в модельные расширения классических с помощью d-перевода, т. е. приписывания знака необходимости Dперед всеми подформулами. При этом Dможно читать "доказуемо". В нек-рых системах К. л. справедливы суждения, ложные при классическом истолковании, напр, отрицание закона исключенного третьего или специфически интуиционистские утверждения о последовательностях. Такие системы Sсводятся к классическим системам [img: http://localhost:8080/file/021235-15.jpg] с помощью подходящего понятия реализуемости р. Доказывают, что [img: http://localhost:8080/file/021235-16.jpg] влечет существование tтакого, что [img: http://localhost:8080/file/021235-17.jpg] причем если А- числовое равенство, то [img: http://localhost:8080/file/021235-18.jpg] Отсюда следует непротиворечивость Sотносительно [img: http://localhost:8080/file/021235-19.jpg] К. л. исследует истинность суждений также в нетрадиционных языках, отличных от языков логики предикатов арифметики, анализа и т. д. Наряду с традиционным отрицанием [img: http://localhost:8080/file/021235-20.jpg] основанным на приведении к противоречию, изучается сильное отрицание [img: http://localhost:8080/file/021235-21.jpg] предусматривающее построение контрпримера. Для [img: http://localhost:8080/file/021235-22.jpg] справедливы многие из законов классич. логики, напр. [img: http://localhost:8080/file/021235-23.jpg] но теорема об эквивалентной замене верна лишь в виде [img: http://localhost:8080/file/021235-24.jpg] К системе сильного отрицания близки системы, основанные на симметричной трактовке истинности и ложности. Семантика для них предусматривает указание не только вида конструкций, обосновывающих истинность, но и вида конструкций, обосновывающих ложность рассматриваемого суждения. Безотрицательная логика Грисса - Нельсона стремится избежать использования отрицания и ограничить класс свойств, о к-рых делаются утверждения, такими, для к-рых уже построены объекты, удовлетворяющие этим свойствам. Язык такой логики содержит связку [img: http://localhost:8080/file/021235-25.jpg] причем [img: http://localhost:8080/file/021235-26.jpg] понимается приблизительно как [img: http://localhost:8080/file/021235-27.jpg] Втеории конструкций исследуются сами правила построения и доказательства, лежащие в основе конструктивной математики. Конструкции строятся из исходных с помощью фиксированного набора комбинаторов и операции применения функции к аргументу. Формулы строятся из равенства с помощью связок логики высказываний и предиката доказуемости я, причем p(a, х-a(х))читается "а есть доказательство того, что a(х)верно для всех x". В качестве аксиом берутся, в частности, все классические тавтологии (включая закон исключенного третьего), т. е. отношение "быть доказательством" предполагается разрешимым. Имеется корректная и точная интерпретация гейтинговских систем в теории конструкции. Рассмотрение в К. л. бескванторных систем вызвано стремлением получить финитные (в том или ином смысле) доказательства рассматриваемых суждений или их мажорант (см. Конструктивная семантика). Многие традиционные системы SК. л. погружаются в бескванторные системы S~ таким образом, что выводимость в Sсуждения [img: http://localhost:8080/file/021235-28.jpg] с бескванторной формулой Rвлечет выводимость в S- формулы R(x,j(х)). для подходящего j. Если S- арифметика без индукции, то S- примитивно рекурсивная арифметика; если S- гейтинговская арифметика, то S- - система гёделевских примитивно рекурсивных функционалов. Для формальных систем К. л. доказаны теоремы нормализации: любой вывод может быть конечным числом стандартных преобразований (редукций) приведен к нормальной форме, не содержащей "лишних" участков (см. Генцена формальная система). Нормальные выводы обладают (в полной мере или, в случае арифметики и более широких систем, частично) свойством подформульности. Имеются связи между К. л. и теорией категорий. Так, понятию "декартовой замкнутой категории" соответствует гейтинговское исчисление высказываний. Иногда к К. л. относят все логические рассмотрения, в к-рых требуется, чтобы все изучаемые объекты были конструктивными, независимо от применяемой логики. С этой тенденцией связано название конструктивных по Гёделю множеств.