Effectively infinite classes of weak constructivizations of models (Q1346921)

Weak constructivizations of strongly constructive models are studied. An enumerated model \((M, \nu)\), where \(\nu\) is an enumeration of \(M\), is called strongly constructive (constructive) if there exists an algorithm to recognize all (quantifier-free) formulas \(\varphi(\overline x)\) and tuples \(\overline m\) of natural numbers for which \(M\models \varphi(\nu\overline m)\) holds. A model \(M\) is called \(n\)-complete if, for each formula \(\varphi(x_ 1, \dots, x_ m)\) which has at most \(n\) alternations of quantifiers and for each tuple \(a_ 1,\dots, a_ m\in M\), there exists an \(\exists\)-formula \(\psi(x_ 1,\dots, x_ m)\) such that \(M\models \psi(x_ 1,\dots, x_ m)\) and \(M\models \forall\overline x(\varphi\to \psi)\). A model \(M\) is called limit-\(\omega\)-complete if, for any \(n\), it possesses a finite \(n\)-complete enrichment by constants, but it has no finite complete enrichments by constants. Theorem 1. If a model \(M\) is limit-\(\omega\)-complete and possesses a strong constructivization, then, given any computable class \(S\) of constructivizations of \(M\) we can effectively build a non-strong constructivization that is not equivalent to any constructivization from \(S\). Theorem 2. If \(M\) is strongly and weakly constructivizable, then, for a given computable class of its constructivizations, we can effectively build a weak constructivization of \(M\) that is not autoequivalent to any constructivization in this class. It follows that the class of weak constructivizations of a strongly constructivizable model is either empty or effectively infinite, and in this case, it is not computable.