Structural subtyping of non-recursive types is decidable

We show that the first-order theory of structural subtyping of non-recursive types is decidable, as a consequence of a more general result on the decidability of term powers of decidable theories. Let Σ be a language consisting of function symbol and let 𝒞; (with a finite or infinite domain C) be an L-structure where L is a language consisting of relation symbols. We introduce the notion of Σ-term-power of the structure 𝒞; denoted 𝒫;_Σ(𝒞;). The domain of 𝒫;_Σ(𝒞;) is the set of Σ-terms over the set C. 𝒫;_Σ(𝒞;) has one term algebra operation for each f ∈ Σ, and one relation for each r ∈ L defined by lifting operations of 𝒞; to terms over C. We extend quantifier for term algebras and apply the Feferman-Vaught technique for quantifier elimination in products to obtain the following result. Let K be a family of L-structures and K_P the family of their Σ-term-powers. Then the validity of any closed formula F on K_P can be effectively reduced to the validity of some closed formula q(F) on K. Our result implies the decidability of the first-order theory of structural subtyping of non-recursive types with covariant constructors, and the construction generalizes to contravariant constructors as well.