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.