A new method for undecidability proofs of first order theories

Abstract

We claim that the reduction of Post’s Correspondence Problem to the decision problem of a theory provides a useful tool for proving undecidability of first order theories given by an interpretation. The goal of this paper is to propose a framework for such reduction proofs. The method proposed is illustrated by proving the undecidability of the theory of a term algebra modulo AC and the theory of a partial lexicographic path ordering.