Об интуиционистской элементарной арифметике

Доказывается невыводимость формулы $\forall_y^{p(x)}v(x,y)=0\vee\neg\forall_y^{p(x)}v(x,y)=0$, где множество $A=\{n:N\mid=\forall_y^{p(n)}v(n,y)=0\}$ $\operatorname{co}$-$\mathbf{NP}$-полное в элементарной интуиционистской арифметике с естественным ограничением на индукционную формулу в аксиоме индукции.
Библиогр. 7.