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

Раздел математической логики, изучающий рассуждения о конструктивных объектах и конструкциях. При таком понимании К. л. шире, чем логика конструктивной математики. Самое заметное отличие от традиционной (классической) логики состоит в отсутствии исключенного третьего закона и двойного отрицания закона При обозначении систем чистой логики (исчисление высказываний, предикатов) термины "конструктивное", "интуиционистское", "гейтинговское" часто считаются синонимами (см. Рейтинга формальная система). Под конструктивной арифметикой иногда понимают гейтпнговскую арифметику, а иногда — ее расширение, получаемое добавлением принципа Маркова (см. Конструктивного подбора принцип )и схемы выражающей эквивалентность формулы и утверждения о ее реализуемости (см. Конструктивная семантика). Эта расширенная система, достаточная для доказательства основных результатов конструктивного математич. анализа, не является, в отличие от гейтинговских систем, подсистемой классич. арифметики: в ней опровергается закон исключенного третьего Иногда к К. л. относят системы интуиционистской логики, содержащие средства описания специфически интуиционистских понятий. Общая черта подавляющего большинства систем К. л., отражающая специфику конструктивного понимания связки и квантора — явная реализация этих связок: выводимость (соответственно существование хА (х))влечет выводимость одной из формул А, В (соответственно 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- — система гёделевских примитивно рекурсивных функционалов. Для формальных систем К. л. доказаны теоремы нормализации: любой вывод может быть конечным числом стандартных преобразований (редукций) приведен к нормальной форме, не содержащей "лишних" участков (см. Генцена формальная система). Нормальные выводы обладают (в полной мере или, в случае арифметики и более широких систем, частично) свойством подформульности. Имеются связи между К. л. и теорией категорий. Так, понятию "декартовой замкнутой категории" соответствует гейтинговское исчисление высказываний. Иногда к К. л. относят все логические рассмотрения, в к-рых требуется, чтобы все изучаемые объекты были конструктивными, независимо от применяемой логики. С этой тенденцией связано название конструктивных по Гёделю множеств. Лит.:[1] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; [2] Troelstra A. S., в кн.: Metamathematical investigation of intuitionistic arithmetic and analysis, B.-Hdlb.-N. Y., 1973; [3] Hовиков П. С, Конструктивная математическая логика с точки зрения классической, М., 1977; t4] Kreisel G., Mathematical logic, в кн.: Lectures on modern mathematics, v. 3, N. Y., 1965, p. 95-195. Г. Е. Минц.