Математическая энциклопедия - конструктивная логика

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

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

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

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

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

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

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

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