Decidability of definability. (English) Zbl 1327.03008

Let a structure of a finite relational signature be given. The authors study the decidability of the following algorithmic problem: given quantifier-free formulas \(\phi_0,\phi_1,\ldots,\phi_n\) of its language, whether one can find a primitive positive formula using \(\phi_1,\ldots,\phi_n\) as basic predicates which is equivalent to \(\phi_0\) on this structure? A formula is called primitive positive if it is built from the basic predicates by means of conjunctions and existential quantifications only.
The main result of this paper is the proof of the decidability of this problem as well as of some of its variations under some restrictions: the structure must be ordered, homogeneous, Ramsey, and finitely bounded (see the definitions in the reviewed paper). An application of the main result is given as well as example showing that it is impossible to omit some of these restrictions on a structure. Some open problems are formulated.


03B25 Decidability of theories and sets of sentences
03C40 Interpolation, preservation, definability
Full Text: DOI arXiv Euclid