Критерий сильной конструктивизируемости однородной модели

Доказано, что для сильной конструктивизируемости однородной модели $\mathfrak{M}$ полной разрешимой теории $T$ вычислимость семейства $S$ всех типов, реализуемых в $\mathfrak{M}$, недостаточна. Приводится соответствующий контрпример, а также точный критерий сильной конструктивизируемости $\mathfrak{M}$, включающий, кроме вычислимости $S$, некоторое условие эффективности для расширений типов из $S$.