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

Гейтипга исчисление,- название трех формальных систем конструктивной логики, предложенных А. Рейтингом [1]. Первая из них - гейтинговское, или интуиционистское, исчисление высказываний- формализация принципов конструктивной логики высказываний; вторая - гейтинговское, или интуиционистское, исчисление предикатов- формализация конструктивной логики предикатов; третья - гейтинговская, или интуиционистская, арифметика - формализация принципов элементарной конструктивной теории чисел. Задуманные первоначально как формализации соответствующих разделов интуиционистской логики и математики, эти системы не содержат, однако, никакой чисто интуиционистской специфики. Логические Г. ф. с. (исчисление высказываний и исчисление предикатов) получаются из обынных вариантов соответствующих классич. систем с полным комплектом [img: http://localhost:8080/file/010409-12.jpg] логических связок (см. Логические исчисления).путем замены "неконструктивного постулата" (обычно это исключенного третьего закон [img: http://localhost:8080/file/010409-13.jpg] или двойного отрицания закон [img: http://localhost:8080/file/010409-14.jpg] на противоречия закон [img: http://localhost:8080/file/010409-15.jpg] Гейтинговская арифметика получается тем же способом из классической арифметики формальной. Генценовские логистические (секвенциальные) системы (см. Генцена формальная система).для Г. ф. с. обычно отличаются от соответствующих классич. систем ограничением: все секвенции, входящие в вывод, односукцедентны. Г. ф. с. корректны относительно (различных вариантов) конструктивного понимания математик, суждений: в частности, формулы, выводимые в этих системах, рекурсивно реализуемы и имеют истинные Гёде-ля интерпретации. Для Г. ф. с. допустимы интуиционистские (см. Интуиционизм).приемы оперирования с логическими связками, содержащими конструктивную задачу: из выводимости формулы вида [img: http://localhost:8080/file/010409-16.jpg] (формулы вида [img: http://localhost:8080/file/010409-17.jpg]) следует выводимость формулы A(t).при нек-ром t(соответственно, одной из формул А, В). При этом в случае арифметики рассматриваемые формулы должны быть замкнутыми. Справедливо также правило Маркова: из выводимости замкнутой формулы [img: http://localhost:8080/file/010409-18.jpg], где R - примитивно рекурсивная бескванторная формула, следует выводимость R(N).при нек-ром N. Гейтингсвская арифметика удовлетворяет условиям Гёделя теоремы о неполноте. В ней невыводим принцип Маркова [img: http://localhost:8080/file/010409-19.jpg] для конкретной примитивно рекурсивной формулы R, хотя этот принцип истинен как при конструктивном понимании суждений в смысле Маркова - Шанина, так и при интерпретации Гёделя. Неполнота логических Г. ф. с. относительно интерпретации реализуемости следует из наличия невыводимой, но реализуемой, пропозициональной формулы. Вопрос о полноте геитинговского исчисления высказываний относительно гёделевской интерпретации остается (1977) открытым. Всякая формула, выводимая в Г. ф. с., выводима в соответствующей классич. системе. Обратное утверждение опровергается на примере (закон исключенного третьего), однако имеется погружение классич. систем в Г. ф. с., не меняющее формул (если рассматривать их с точностью до эквивалентности в классич. системе) и сохраняющее не только доказуемость формул, но и структуру доказательств: всякий вывод формулы Аиз списка [img: http://localhost:8080/file/010409-20.jpg] в классич. системе легко перестраивается в вывод формулы [img: http://localhost:8080/file/010409-21.jpg] из списка [img: http://localhost:8080/file/010409-22.jpg] в соответствующей Г. ф. с. Здесь [img: http://localhost:8080/file/010409-23.jpg] обозначает результат дописыванпя [img: http://localhost:8080/file/010409-24.jpg] перед всеми подформулами формулы А(в случае исчисления высказываний достаточно вставить [img: http://localhost:8080/file/010409-25.jpg] только перед самой формулой А). Таким образом, формулы вида [img: http://localhost:8080/file/010409-26.jpg] выводимы классически тогда и только тогда, когда они выводимы в Г. ф. с., что дает доказательство относительной непротиворечивости для классич. систем. Сохраняющее структуру выводов погружение Г. ф. с. в классич. системы невозможно, однако имеется погружение Г. ф. с. в классич. системы с дополнительной связкой [img: http://localhost:8080/file/010409-27.jpg] ("доказуемо"). В исчислении предикатов все связки независимы. В арифметике [img: http://localhost:8080/file/010409-28.jpg] выражается через [img: http://localhost:8080/file/010409-29.jpg] - через [img: http://localhost:8080/file/010409-30.jpg], [img: http://localhost:8080/file/010409-31.jpg]. Можно сконструировать логическую связку, через к-рую выражаются все остальные, напр. [img: http://localhost:8080/file/010409-32.jpg] Теоретико-множественная теория моделей для Г. ф. с. использует интенсиональные модели, в к-рых истинность высказывания не определяется раз и навсегда, а зависит от рассматриваемого "момента времени". Для изучения геитинговского исчисления высказываний используются псевдобулевы, алгебры. В современной теории доказательств Г. ф. с. изучаются в основном как части систем, включающих более мощные принципы конструктивной математики (принцип Маркова, реализуемость) или интуиционистской математики (брауэровский принцип непрерывности, бар-индукция и т. д.).