Simple second-order languages for which unification is undecidable

We improve Goldfarb's Theorem on the undecidability of the second-order unification problem. More precisely, we prove that there is a natural number n such that the unification problem is undecidable for all second-order languages containing a binary function constant and at 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 languages 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.