Simple Second-Order Languages for which Unification is Undecidable
William M. Farmer
1991
Abstract
We improve Goldfarb's Theorem on the undecidability of the
second-order unification problem. More precisely, we prove that there
is an natural number n such that the unification problem is
undecidable for all second-order languages containing a binary
function constant and a least n function variables with arity >= 1.
This result allows one to draw a sharp line between second-order
languages for which unification is decidable and second-order language
for which unification is undecidable. It also answers a question
raised by the k-provability problem that is not answered by Goldfarb's
result. Our proof utilizes term rewriting concepts and several
unification coding tricks.