Undecidable Fragments of Term Algebras with Subterm Relation

Abstract

In this paper we give a new proof of undecidability results about term algebras with subterm relation. This proof yields a novel result which states that, in presence of the subterm relation and in signatures with symbols of arity greater than one, the ${\sum }_1$ theory of rational trees is properly included in the ${\sum }_1$ theory of infinite trees. Moreover, these theories are quite different; in fact, the first is r.e. and the second has degree not less than ${\sum }_1^1$ . Here, in analogy with the arithmetical hierarchy, we call ${\mathrm{\Delta }}_0$ the prenex formulas, whose quantifiers are bounded by the predicate ⩽, and we call ${\sum }_1$ the formulas which are existential quantification of ${\mathrm{\Delta }}_0$ formulas.