Recursive model theory
recursively presented model theory
A branch of mathematics that is on the border-line between model theory, algebra and the theory of recursive functions (cf. Recursive function), and related to the study of questions of effectiveness in models and algebras.
A.I. Mal'tsev's article Constructive algebras [1] was the first overviewing work on recursively presented models. In it the basic concepts were developed and systematized, and the road to further development of this theory was indicated. A major role in the erection and development of this branch of mathematics was played by Yu.L. Ershov and his students, who solved a number of fundamental problems, worked out new concepts and determined new directions of research in recursive model theory (cf. [2]).
The basic notions and results in recursive model theory are formulated below. All considerations are, usually, in a fixed signature
$$ \sigma _ {0} = < P _ {0} ^ {n _ {0} } \dots P _ {k} ^ {n _ {k} } , . . . > _ {k < \omega } $$
such that the function $ f $: $ f ( k) = n _ {k} $ is recursive. When considering algebraic systems, function symbols may occur in the signature. The signature
$$ \sigma _ {1} = \sigma _ {0} \cup \langle a _ {0} \dots a _ {k} , . . . \rangle _ {k < \omega } , $$
which is obtained from $ \sigma _ {0} $ by adjoining a countable number of individual constants, is also used. It is always understood that $ n _ {0} = 2 $ and that the predicate $ P _ {0} ^ {2} $ is defined on any model as equality. Let $ L _ {i} $, $ i = 0 , 1 $, be the collection of all formulas of restricted predicate calculus with equality $ ( P _ {0} ^ {2} ) $ of signatures $ \sigma _ {i} $, $ i = 0 , 1 $, and let $ g $ be a fixed Gödel enumeration (cf. [3]) of $ L _ {1} $( $ g : \mathbf N \rightarrow L _ {1} $). A subset $ S \subseteq L _ {1} $ is called decidable if the set $ g ^ {-} 1 ( S) $ is recursive (cf. Recursive set theory). An enumerated model (of signature $ \sigma _ {0} $) is a pair $ ( \mathfrak M , \nu ) $, where $ \mathfrak M = \langle M , P _ {0} ^ {n _ {0} } \dots P _ {k} ^ {n _ {k} } , \dots \rangle _ {k < \omega } $ is a model of signature $ \sigma _ {0} $ and $ \nu $ is a enumeration of the underlying set $ M $ of $ \mathfrak M $. An enumerated model $ ( \mathfrak M , \nu ) $ is called a recursively presented model if the set
$$ \overline{D}\; ( \mathfrak M , \nu ) = \ \{ {\langle k , x _ {1} \dots x _ {n _ {k} } \rangle } : { \mathfrak M \vDash P _ {k} ^ {n _ {k} } ( \nu ( x _ {1} ) \dots \nu ( x _ {n _ {k} } ) ) } \} $$
is recursive.
For each enumerated model $ ( \mathfrak M , \nu ) $ one can construct some $ \sigma _ {1} $- saturation $ \mathfrak M _ \nu $ of $ \mathfrak M $, i.e. a model of signature $ \sigma _ {1} $, with underlying set that of $ \mathfrak M $, with predicates from $ \sigma _ {0} $ in $ \mathfrak M _ \nu $ coinciding with the corresponding predicates of $ \mathfrak M $, and with constants defined by: As the element $ a _ {k} , $ $ k < \omega $, one takes $ \nu ( k) \in M $. Let $ \mathop{\rm Th} ( \mathfrak M ) $ be the elementary theory of $ \mathfrak M $, i.e. the set of closed formulas of signature $ \sigma _ {0} $ that are true on $ \mathfrak M $. Let $ \mathop{\rm Th} ( \mathfrak M , \nu) $ be the elementary theory of the enumerated model $ \mathfrak M _ \nu $. An enumerated model $ ( \mathfrak M , \nu ) $ is called strongly recursively presented or decidable if $ \mathop{\rm Th} ( \mathfrak M , \nu ) $ is a decidable theory. From the definition it is immediately clear that a strongly recursively presented model is recursively presented.
One of the basic problems in recursive model theory is the existence of recursively presented models with various elementary properties, i.e. with properties describable in the language of restricted predicate calculus. A number of interesting and important theorems have been obtained (1990) in this direction. The following yields the existence of a large class of strongly recursively presented models: If $ T \subseteq L _ {0} $ is a decidable theory, then there is a sequence of strongly recursively presented models
$$ ( \mathfrak M _ {0} , \nu _ {0} ) \dots ( \mathfrak M _ {k} , \nu _ {k} ) \dots \ \ k < \omega , $$
such that $ T = \cap _ {k < \omega } \mathop{\rm Th} ( \mathfrak M _ {k} ) $ and the set $ \{ {\langle x , y \rangle } : {g ( y) \in \mathop{\rm Th} ( \mathfrak M _ {x} , \nu _ {x} ) } \} $ is recursive. It has been noticed that there are formulas having no recursively presented models. The following two theorems give some sufficient conditions for the existence of recursively presented models for a theory with a recursively-enumerable set of axioms.
If $ T $ is a recursively-enumerable $ \forall \exists $- theory having a model $ \mathfrak M $ with a recursively-enumerable $ \exists $- theory, then $ T $ has a recursively presented model.
A theory $ T $ of finite signature $ \sigma = \langle P _ {0} ^ {n _ {0} } \dots P _ {k} ^ {n _ {k} } , c _ {0} \dots c _ {l} \rangle $ is called $ \forall $- finite if the universal theory of any extension $ T ^ \prime \supseteq T $( of the same signature) is finitely axiomatizable (by universal statements). A theory $ T $ is called strongly $ \forall $- finite if for any finite set $ \langle c _ {l+} 1 \dots c _ {N} \rangle $ of individual constants the theory $ T ^ {*} $ is $ \forall $- finite. Here $ T ^ {*} $ is defined to be $ T $ but now in the language of the signature $ \sigma ^ {*} = \sigma \cup \langle c _ {l+} 1 \dots c _ {N} \rangle $.
If a theory $ T $ is strongly $ \forall $- finite, and $ \widetilde{T} $ is a recursively-enumerable extension of $ T $, then $ \widetilde{T} $ has a recursively presented model.
Another circle of problems is related to the existence, for a given model $ \mathfrak M $, of enumerations $ \nu $ such that $ ( \mathfrak M , \nu ) $ becomes a (strongly) recursively presented model. Models for which such an enumeration exists are called (strongly) recursively presentable, while the corresponding enumeration is called a (strong) recursive presentation. For the solution of a number of problems related to the recursive presentability of models, Ershov's kernel theorem turns out to be useful. Its application to concrete algebraic systems allows one to solve a number of natural problems. In particular, it has been established that: 1) any recursively presented locally nilpotent torsion-free group has a recursively presented completion; and 2) if $ ( F , \nu ) $ is a recursively presented field and $ F _ {0} $ is an algebraic extension of $ F $, then $ \nu $ extends to a recursive presentation of $ F _ {0} $ if and only if the family of finite sets of polynomials over $ F $ in a countable number of variables, with roots in $ F _ {0} $, is recursively enumerable.
A large class of recursively presented models is given by the following theorem: Any countable model of an $ \aleph _ {1} $- categorical (cf. Categoricity in cardinality) decidable theory is strongly recursively presentable. The problem of the (strong) recursive presentability of special models of complete theories, in particular of simple and universal models, is of interest. Sufficient and necessary conditions for the (strong) recursive presentability of simple (and countable saturated) models of a complete theory have been found. Examples of complete theories with non-recursively presentable simple and universal models have been constructed. It has been proved that a simple model of a complete decidable theory that has a strongly recursively presentable universal model or a finite number of pairwise non-isomorphic countable models, is always strongly recursively presentable.
The question of the number of inequivalent recursive presentations for a given model has been investigated. Two recursive presentations $ \nu $ and $ \mu $ of a model $ \mathfrak M $ are called (recursively) equivalent if there exists an isomorphism $ \phi $( $ \phi = \mathop{\rm id} _ {\mathfrak M } $) and a recursive function $ f $ such that $ \phi \nu = \mu f $. A model is called self-stable (recursively stable) if any two recursive presentations of it are (recursively) equivalent.
For a large class of algebraic systems it has been proved that there exists either only one (up to equivalence) or a countable number of inequivalent recursive presentations [4], [5]. For the theories of fields, Boolean algebras, torsion-free Abelian groups, and some other classes of algebraic systems the question of the number of inequivalent recursive presentations has been solved completely [11], and the self-stable models have been described [2]. It has also been demonstrated that questions of self-stability are related to the study of computability of classes of recursively presented models.
References
[1] | A.I. Mal'tsev, "Constructive algebras I" Russian Math. Surveys , 16 : 3 (1961) pp. 77–129 ((Also in: A.I. Mal'cev, The metamathematics of algebraic systems, North-Holland, 1971, Chapt. 18)) Uspekhi Mat. Nauk , 16 : 3 (1962) pp. 3–60 |
[2] | Yu.L. Ershov, "Theory of enumerations" , 3. Constructive models , Novosibirsk (1974) (In Russian) |
[3] | Yu.L. Ershov, I.A. Lavrov, A.D. Taimanov, M.A. Taitslin, "Elementary theories" Russian Math. Surveys , 20 : 4 (1965) pp. 35–105 Uspekhi Mat. Nauk , 20 : 4 (1965) pp. 37–108 |
[4] | S.S. Goncharov, "Selfstability, and computable families of constructivizations" Algebra and Logic , 14 : 6 (1975) pp. 392–408 Algebra i Logika , 14 : 6 (1975) pp. 647–680 |
[5] | A.T. Nurtazin, "Strong and weak constructivizations, and enumerable families" Algebra and Logic , 13 : 3 (1974) pp. 177–184 Algebra i Logika , 13 : 3 (1974) pp. 311–323 |
[6] | A. Cobham, , Summaries of talks presented at the summer institute for symbolic logic Cornell University, 1957 , Washington, D.C. (1960) pp. 391–395 |
[7] | A. Fröhlich, J.C. Shepherdson, "Effective procedures in field theory" Phil. Trans. Royal. Soc. London Ser. A. , 2458 (1956) pp. 407–428 |
[8] | A. Mostowski, "A formula with no recursively enumerable model" Fund. Math. , 42 : 1 (1955) pp. 125–140 |
[9] | M.O. Rabin, "Computable algebra, general theory and theory of computable fields" Trans. Amer. Math. Soc. , 95 : 2 (1960) pp. 341–360 |
[10] | R.L. Vaught, "Sentences true in all constructive models" J. Symb. Logic , 25 : 1 (1960) pp. 39–58 |
[11] | S.S. Goncharov, "Problem of the number of non-self-equivalent constructivizations" Algebra and Logic , 19 : 6 (1980) pp. 401–414 Algebra i Logika , 19 : 6 (1980) pp. 621–639 |
Comments
The theory of recursive functions can be mixed with model theory in several ways. First, one can study recursive models, i.e. models (corresponding to a recursive vocabulary) over the natural numbers with all of their relations and functions recursive. By the Gödel completeness theorem, every consistent (first-order) sentence has a model. However, not every such sentence has a recursive model (Mostowski's theorem). There are conditions under which recursive models exist, e.g., each recursively enumerable $ \forall \exists $- theory allowing a model with a recursively enumerable $ \exists $- theory has a recursive model also. And each countable model of an $ \aleph _ {1} $- categorical decidable theory has an equivalent $ ( \mathbf N ,\dots ) $ which is strongly recursive in the sense that the theory of its expansion $ ( \mathbf N \dots n) _ {n \in \mathbf N } $ is decidable. By the Gödel incompleteness theorem, Peano's arithmetic has many models besides its standard (recursive) one, although none of these is recursive (Tennenbaum's theorem). However, the subject is broader than just the study of recursive models. For instance, one can try to "effectivize" model-theoretic results. E.g.: by the interpolation theorem, for every valid (first-order) implication $ \varphi \rightarrow \psi $ there exists an "interpolant" $ \chi $ whose vocabulary is contained in the common part of those of $ \varphi $ and $ \psi $ such that both $ \varphi \rightarrow \chi $ and $ \chi \rightarrow \psi $ are valid. Such an interpolant cannot always be obtained recursively from $ \varphi $ and $ \psi $( Friedman's theorem). By Lindenbaum's theorem, every consistent (first-order) theory has a complete extension. How complex will this extension be, given that the initial theory is (say) recursive? (Answer: $ \Delta _ {1} ^ {2} $( cf. Descriptive set theory) suffices. Note that, by a theorem of Tarski, the complete theory of the standard model of arithmetic is not even arithmetical.)
Constructive model theory. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Constructive_model_theory&oldid=43315