КОНСТРУКТИВНАЯ ЛОГИКА


КОНСТРУКТИВНАЯ ЛОГИКА

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

При обозначении систем чистой логики (исчисление высказываний, предикатов) термины "конструктивное", "интуиционистское", "гейтинговское" часто считаются синонимами (см. Рейтинга формальная система). Под конструктивной арифметикой иногда понимают гейтпнговскую арифметику, а иногда - ее расширение, получаемое добавлением принципа Маркова (см. Конструктивного подбора принцип )и схемы выражающей эквивалентность формулы и утверждения о ее реализуемости (см. Конструктивная семантика). Эта расширенная система, достаточная для доказательства основных результатов конструктивного математич. анализа, не является, в отличие от гейтинговских систем, подсистемой классич. арифметики: в ней опровергается закон исключенного третьего Иногда к К. л. относят системы интуиционистской логики, содержащие средства описания специфически интуиционистских понятий. Общая черта подавляющего большинства систем К. л., отражающая специфику конструктивного понимания связки и квантора - явная реализация этих связок: выводимость (соответственно существование хА (х))влечет выводимость одной из формул А, В (соответственно 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.

Г. Е. Минц.


Математическая энциклопедия. — М.: Советская энциклопедия. . 1977—1985.

Смотреть что такое "КОНСТРУКТИВНАЯ ЛОГИКА" в других словарях:

  • КОНСТРУКТИВНАЯ ЛОГИКА —         1) то же, что и интуиционистская логика; 2) ветвь логики, в которой изучаются финитные (см. Финитизм) рассуждения о конструктивных объектах и процессах (см. Конструктивное направление) и строится соответств. семантика. В К. л. отвергается …   Философская энциклопедия

  • конструктивная логика —         КОНСТРУКТИВНАЯ ЛОГИКА (от лат. constructio построение) совокупность логических принципов, признаваемых приемлемыми представителями конструктивизма в математике. Предметом конструктивизма являются конструктивные объекты и конструктивные… …   Энциклопедия эпистемологии и философии науки

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

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

  • Логика — Гр …   Википедия

  • Логика (философия) — Логика (др. греч. λογική «наука о рассуждении», «искусство рассуждения» от λόγος  «речь», «рассуждение»)  наука о формах, методах и законах интеллектуальной познавательной деятельности, формализуемых с помощью логического языка. Поскольку это… …   Википедия

  • КОНСТРУКТИВНАЯ МАТЕМАТИКА — конструктивное направление в математике, математика, строящаяся в соответствии с тем или иным конструктивным математич. мировоззрением, обыкновенно стремящимся связывать утверждения о существовании математнч. объектов с возможностью их построения …   Математическая энциклопедия

  • ЛОГИКА — наука о формах, законах и методах правильного (т. с. построенного в соответствии с определенными логическими стандартами) мышления. Различают формальную и содержательную логику. Формальная логика изучает мышление опосредованно, только через… …   Философия науки: Словарь основных терминов

  • ЛОГИКА В РОССИИ — эволюция современной (математической) логики в России. Кон. 19 в. и нач. 20 в. знаменуют выход логики за рамки силлогистики и появление логиков новаторов, таких как П.С. Порецкий, М.В. Каринский, Л.В. Рутковский, СИ. Поварнин, и др. Казанский… …   Философская энциклопедия

  • ЛОГИКА ВЫСКАЗЫВАНИЙ — раздел логики, в котором изучаются истинностные взаимосвязи между высказываниями. В рамках данного раздела высказывания (пропозиции, предложения) рассматриваются только с т.зр. их истинности или ложности, безотносительно к их внутренней субъектно …   Философская энциклопедия

Книги



Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.