О построении разрешимых сингулярных теорий двух функций следования с дополнительным предикатом

Получено усиление результата Рабина о разрешимости теории $S2S$, т. е. сингулярной теории второго порядка двух функций следования. Установлена разрешимость ряда теорий вида $S2S[P]$, получаемых из теории $S2S$ введением дополнительного унарного предиката $P$. Теория $S2S[P]$ разрешима, когда предикат $P:\{0,1\}^*\to\{\text{И, Л}\}$ задан так, что $P(w)=\text{И}\sim|w|\in I$, где $I$ — область значений функции, возникающей из функций $x!$, $x^a$, $a^x$ ($a=1,2,\dots$) конечным применением операций суперпозиции, суммирования и мультиплицирования.