The Undecidability of the First-Order Theories of One Step Rewriting in Linear Canonical Systems

AbstractBy reduction from the halting problem for Minsky's two-register machines we prove that there is no algorithm capable of deciding the ∃∀∀∀-theory of one step rewriting of an arbitrary finite linear confluent finitely terminating term rewriting system (weak undecidability). We also present a fixed such system with undecidable ∃∀*-theory of one step rewriting (strong undecidability). This improves over all previously known results of the same kind