Выразимость в элементарной теории рекурсивно-перечислимых множеств с логикой реализуемости

Для замкнутых формул языка первого порядка в сигнатуре $\langle \varnothing, N, W_0, W_1,\dots; \cup,\cap,'\rangle$ индукцией по построению формулы определяется реализуемость по Клини. Например, $e \,r\!\!\!\!\mathrm{O}\, \forall \mathfrak{X} \mathfrak{A}(\mathfrak{X})\leftrightharpoons(\forall x)[!\varphi e(x)\& \varphi e(x)\,r\!\!\!\!\mathrm{O}\,\mathfrak{A}(Wx)]$. Теорией $\mathscr{E}_r$ называется множество реализуемых формул, не содержащих констант $W_i$. Предикат $P(\mathfrak{X}_1,\dots,\mathfrak{X}_n)$, определенный на р. п. множествах, называется выразимым в $\mathscr{E}_r$, если существует такая формула $\mathfrak{A}(\mathfrak{X}_1,\dots,\mathfrak{X}_n)$ без констант $W_i$, что $\,r\!\!\!\!\mathrm{O}\,\mathfrak{A}(W_{i_1},\dots,W_{i_n})\Leftrightarrow P(W_{i_1},\dots,W_{i_n})=t$, и арифметическим, если множество $\{\langle i_1,\dots,i_n\rangle\mid P(W_{i_1},\dots,W_{i_n})=t\}$ арифметическое. Доказано, что предикат $P$ выразим в $\mathscr{E}_r$ тогда и только тогда, когда $P$ — рекурсивно-инвариантный арифметический предикат. Отсюда следует выразимость в $\mathscr{E}_r$ практически всех предикатов содержательной теории р. п. множеств. Показано, что в $\mathscr{E}_r$ можно погрузить арифметику, откуда следует неразрешимость $\mathscr{E}_r$.