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

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

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

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

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

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

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

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