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

2021/10/31 by Juvenal Murwanashyaka, Murwanashyaka, Juvenal
Computer Science · #Advanced Algebra and Logic #Computability, Logic, AI Algorithms #FOS: Mathematics #Logic (math.LO) #Logic, programming, and type systems #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.2111.00573

openalex publication_date 2021/10/31 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28

Abstract

We introduce a first-order theory of finite full binary trees and then\nidentify decidable and undecidable fragments of this theory. We show that the\nanalogue of Hilbert`s 10th Problem is undecidable by constructing a many-to-one\nreduction of Post`s Correspondence Problem. By a different method, we show that\ndeciding truth of sentences with one existential quantifier and one bounded\nuniversal quantifier is undecidable.\n

Related

• Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering
• Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
• The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable
• One Henkin Quantifier in the empty vocabulary suffices for undecidability
• On Generalizing Decidable Standard Prefix Classes of First-Order Logic