Каждое рекурсивно-перечислимое расширение теории линейного порядка имеет конструктивную модель

Теорема. Пусть $T$ — произвольная рекурсивно-перечислимая теория сигнатуры $\sigma=\langle =, <, R_1^1, R_2^1\ldots, R_n^1\rangle$, расширяющая теорию $T_{0}$ линейного порядка сигнатуры $\sigma_{0}=\langle =,<\rangle$. Тогда $T$ имеет конструктивную модель.
Отмечается, что вместе с тем существует наследственно неразрешимое рекурсивно-перечислимое расширение теории $T_{0}$ даже в сигнатуре без дополнительных одноместных предикатов.