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

ГЕЙТИНГА ФОРМАЛЬНАЯ СИСТЕМА, Гейтинга исчисление, - название трех формальных систем конструктивной логики, предложенных А. Гейтингом [1]. Первая из них - гейтинговское, или интуиционистское, исчисление высказываний - формализация принципов конструктивной логики высказываний; вторая - гейтинговское, или интуиционистское, исчисление предикатов - формализация конструктивной логики предикатов; третья - гейтинговская, или интуиционистская, арифметика - формализация принципов элементарной конструктивной теории чисел. Задуманные первоначально как формализации соответствующих разделов интуиционистской логики и математики, эти системы не содержат, однако, никакой чисто интуиционистской специфики.

Логические Г. ф. с. (исчисление высказываний и исчисление предикатов) получаются из обычных вариантов соответствующих классич. систем с полным комплектом (&, ∨, ⊃, ¬, ∀, ∃) логических связок (см. Логические исчисления) путем замены «неконструктивного постулата» (обычно это исключенного третьего закон А ∨ ¬А или двойного отрицания закон ¬¬A⊃A) на противоречия закон (А & ¬А) ⊃ В. Гейтинговская арифметика получается тем же способом из классической арифметики формальной. Генценовские логистические (секвенциальные) системы (см. Генцена формальная система) для Г. ф. с. обычно отличаются от соответствующих классич. систем ограничением: все секвенции, входящие в вывод, односукцедентны.

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

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

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

В исчислении предикатов все связки независимы. В арифметике ¬ выражается через ⊃, a ∨ - через ∃, &, ⊃. Можно сконструировать логическую связку, через к-рую выражаются все остальные, напр. (((р ∨ q) & r) ∨ (¬p & (r ≡ ∀x∃y s(x,y)))). Теоретико-множественная теория моделей для Г. ф. с. использует интенсиональные модели, в к-рых истинность высказывания не определяется раз и навсегда, а зависит от рассматриваемого «момента времени». Для изучения гейтинговского исчисления высказываний используются псевдобулевы алгебры.

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

Лит.: [1] Heyting A., «Sitzungsber. Dtsch. Akad. Wiss. 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.

Г. E. Минц.

Источники:

1. Математическая Энциклопедия. Т. 1 (А - Г). Ред. коллегия: И. М. Виноградов (глав ред) [и др.] - М., «Советская Энциклопедия», 1977, 1152 стб. с илл.