Undecidability in First-Order Theories of Term Algebras Extended with a Substitution Operator

TL;DR

This paper investigates the logical properties of a first-order theory of finite binary trees, identifying decidable and undecidable fragments, and demonstrating undecidability through reductions from classical problems.

Contribution

It introduces a new first-order theory of binary trees and establishes undecidability results for certain logical fragments using novel reductions.

Findings

Undecidability of the analogue of Hilbert's 10th Problem for the theory.

Undecidability of sentences with one existential and one bounded universal quantifier.

Identification of decidable fragments within the theory.

Abstract

We introduce a first-order theory of finite full binary trees and then identify decidable and undecidable fragments of this theory. We show that the analogue of Hilbert`s 10th Problem is undecidable by constructing a many-to-one reduction of Post`s Correspondence Problem. By a different method, we show that deciding truth of sentences with one existential quantifier and one bounded universal quantifier is undecidable.