ГЕЙТИНГА ФОРМАЛЬНАЯ СИСТЕМА это:

ГЕЙТИНГА ФОРМАЛЬНАЯ СИСТЕМА

Гейтипга исчисление,- название трех формальных систем конструктивной логики, предложенных А. Рейтингом [1]. Первая из них - гейтинговское, или интуиционистское, исчисление высказываний- формализация принципов конструктивной логики высказываний; вторая - гейтинговское, или интуиционистское, исчисление предикатов- формализация конструктивной логики предикатов; третья - гейтинговская, или интуиционистская, арифметика - формализация принципов элементарной конструктивной теории чисел. Задуманные первоначально как формализации соответствующих разделов интуиционистской логики и математики, эти системы не содержат, однако, никакой чисто интуиционистской специфики.

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

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

Гейтингсвская арифметика удовлетворяет условиям Гёделя теоремы о неполноте. В ней невыводим принцип Маркова для конкретной примитивно рекурсивной формулы R, хотя этот принцип истинен как при конструктивном понимании суждений в смысле Маркова - Шанина, так и при интерпретации Гёделя. Неполнота логических Г. ф. с. относительно интерпретации реализуемости следует из наличия невыводимой, но реализуемой, пропозициональной формулы. Вопрос о полноте геитинговского исчисления высказываний относительно гёделевской интерпретации остается (1977) открытым.

Всякая формула, выводимая в Г. ф. с., выводима в соответствующей классич. системе. Обратное утверждение опровергается на примере (закон исключенного третьего), однако имеется погружение классич. систем в Г. ф. с., не меняющее формул (если рассматривать их с точностью до эквивалентности в классич. системе) и сохраняющее не только доказуемость формул, но и структуру доказательств: всякий вывод формулы Аиз списка в классич. системе легко перестраивается в вывод формулы из списка в соответствующей Г. ф. с. Здесь обозначает результат дописыванпя перед всеми подформулами формулы А(в случае исчисления высказываний достаточно вставить только перед самой формулой А). Таким образом, формулы вида выводимы классически тогда и только тогда, когда они выводимы в Г. ф. с., что дает доказательство относительной непротиворечивости для классич. систем. Сохраняющее структуру выводов погружение Г. ф. с. в классич. системы невозможно, однако имеется погружение Г. ф. с. в классич. системы с дополнительной связкой ("доказуемо").

В исчислении предикатов все связки независимы. В арифметике выражается через - через , . Можно сконструировать логическую связку, через к-рую выражаются все остальные, напр.

Теоретико-множественная теория моделей для Г. ф. с. использует интенсиональные модели, в к-рых истинность высказывания не определяется раз и навсегда, а зависит от рассматриваемого "момента времени". Для изучения геитинговского исчисления высказываний используются псевдобулевы, алгебры.

В современной теории доказательств Г. ф. с. изучаются в основном как части систем, включающих более мощные принципы конструктивной математики (принцип Маркова, реализуемость) или интуиционистской математики (брауэровский принцип непрерывности, бар-индукция и т. д.).

Лит.:[1] Неуting A., "Sitzungsber. Dtsch. Akad. Wise. Phys.-math. Klasse", 1930, Bd 16, №1, S.42-56, 57-71, № 10-12, S. 158-69; [2] КлиниС. К., Введение в метаматематику, пер. с англ., М., 1957; [3] Карри X. Б., Основания математической логики, пер. с англ., М., 1969; [4] Fitting М., Intuitionistic logic model theory and forcing, Amst.- L., 1969. Г. Е. Минц.


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

Смотреть что такое "ГЕЙТИНГА ФОРМАЛЬНАЯ СИСТЕМА" в других словарях:

  • ИНТУИЦИОНИЗМ — (от позднелат. intuitio, от лат. intueor пристально смотрю) направление в обосновании математики и логики, согласно которому конечным критерием приемлемости методов и результатов этих наук является наглядно содержательная интуиция. Вся математика …   Философская энциклопедия

  • Список статей по логике —   Это служебный список статей, созданный для координации работ по развитию темы.   Данное предупреждение не ус …   Википедия

  • ИСЧИСЛЕНИЕ — (формальная система) система символов, основными компонентами которой являются: 1) алфавит (совокупность элементарных символов букв. цифр, скобок и т.п.), 2) правила построения формул из символов алфавита, 3) аксиомы (исходные доказуемые формулы) …   Философская энциклопедия

  • МНОГОЗНАЧНАЯ ЛОГИКА — совокупность логических систем, опирающихся на многозначности принцип. В классической двузначной логике выражения при интерпретации принимают только два значения «истинно» и «ложно», в М.л. рассматриваются и др. значения, напр. «неопределенно»,… …   Философская энциклопедия

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

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


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

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