Гейтинговское исчисление предикатов с эпсилон-символом

Известно, что добавление к гейтинговскому исчислению предикатов $\varepsilon$-символа с $\varepsilon$-аксиомам $A[t]\to A[\varepsilon x A]$ дает неконсервативное расширение. Например, становится выводимой формула
$$ \exists x(\rceil P_x\to\rceil Pb\&\rceil Pa). $$
Консервативное расширение получается, если рассматривать $\varepsilon$-символ по аналогии с $\iota$-символом: для любого вхождения символа $\varepsilon x A[x,\alpha_1,\dots,\alpha_n]$ в некоторую секвенцию из данного вывода в антецедент этой секвенции должна входить формула $\forall\alpha_1\dots\forall\alpha_n\exists x A$. Для получающейся системы $HPC^{\varepsilon}$ доказывается устранимость сечения. Указывается, что доказательство допускает обобщение на $HPC$ с разрешимым равенством, на гейтинговскую арифметику со свободными функциональными переменными и принципом выбора:
$$ \Gamma\to\forall x\exists y A;\quad\forall x A_y[f(x)],\quad\Gamma\to C\vdash\Gamma\to C. $$
Распространение на гейтинговскую арифметику со связанными переменными более высоких типов и соответствующими принципами выбора требует привлечения новых идей.