Замечания об исчислениях конструктивной логики с подчиненными переменными и аксиомой полной индукции

В настоящей заметке строятся исчисления $\mathbf{NK}_3^\Sigma$ и $\mathbf{NN}_3$, являющиеся расширениями исчислений $\mathbf{NK}_1^\Sigma$ и $\mathbf{NN}_1$ (РЖМат. 1966, 2А73) и получающиеся в результате присоединения к последним аксиомы полной индукции для базисных нормальных формул и аксиом, выражающих свойства конкретного алгорифма, аналогичного частично-рекурсивной функции $\rho$, использованной в пункте 13 доказательства теоремы 62 книги С. К. Клини (РЖМат, 1957, 7591). Указывается, что в рамках исчисления $\mathbf{NN}_3$ можно провести обоснование исчисления $\mathbf{NK}_3^\Sigma$, аналогичное обоснованию исчисления $\mathbf{NK}_1^\Sigma$. Доказывается выводимость в исчислении $\mathbf{NK}_3^\Sigma$ нескольких формул, выражающих различные варианты принципа полной индукции для формул с подчиненными переменными.
Библ. – 2 назв.