Undecidability in First-Order Theories of Term Algebras Extended with a Substitution Operator
Logic
2021-11-02 v1
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.
Keywords
Cite
@article{arxiv.2111.00573,
title = {Undecidability in First-Order Theories of Term Algebras Extended with a Substitution Operator},
author = {Juvenal Murwanashyaka},
journal= {arXiv preprint arXiv:2111.00573},
year = {2021}
}