Undecidable Fragments of Term Algebras with Subterm Relation

Article type: Research Article

Authors: Marongiu, Gabriele^{a; b; *} | Tulipani, Sauro^{a; b; *; **}

Affiliations: [a] Università di Bologna, Dipartimento di Matematica, P.zza di Porta S. Donato 5, I-40127 Bologna | [b] Università di Camerino, Dipartimento di Matematica e Fisica, via Madonna delle Carceri, I-62032 Camerino

Note: [*] The authors thanks MURST for partial support.

Note: [**] E-mail: [email protected]

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 ∑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 ∑11. 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.

DOI: 10.3233/FI-1993-193-408

Journal: Fundamenta Informaticae, vol. 19, no. 3-4, pp. 371-382, 1993