Undecidable Fragments of Term Algebras with Subterm Relation
Gabriele Marongiu, Sauro Tulipani · Fundamenta Informaticae · 1993
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 ∑ 1 theory of rational trees is properly included in the ∑ 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 ∑ 1 1 . Here, in analogy with the arithmetical hierarchy, we call Δ 0 the prenex formulas, whose quantifiers are bounded by the predicate ⩽, and we call ∑ 1 the formulas which are existential quantification of Δ 0 formulas.