Гейтинга Формальная Система

Гейтипга исчисление,- название трех формальных систем конструктивной логики, предложенных А. Рейтингом [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. Г. Е. Минц.