Погружение интуиционистской теории типов в безотрицательную теорию типов

Предложена аксиоматическая система $HATT^N$, предназначенная для описания безотрицательной теории типов. Построена погружающая операция формул обычной интуиционистской теории типов $HATT$ в множество формул $HATT^N$, позволяющая доказать консервативность $HATT$ относительно $HATT^N$. В частности, установлено, что для любой формулы $A$ языка $HA$ (интуиционистская арифметика), не содержащей логических символов $\bot$, $\vee$ и $\supset$, $A$ выводима в $HATT$ в том и только в том случае, если $A$ выводима в $HATT^N$. Библиогр. 7 назв.