Simple second-order languages for which unification is undecidable (Q807609)

Second-order substitutions are applied to terms constructed from individual and function constants and variables. Such a substitution \(\sigma\) assigns terms to individual variables and \(\lambda\)-expressions of the form \(\lambda x_ 1...\lambda x_ n t\) to n-place function variables. \(\sigma\) unifies terms s, u if \(s\sigma\) and \(u\sigma\) are equal after \(\lambda\)-conversion is performed. The author proved earlier [Ann. Pure Appl. Logic 39, No.2, 131-174 (1988; Zbl 0655.03004)] that the second-order unification problem is decidable when all function constants are monadic. Goldfarb proved that there is a language for which the second-order unification problem is undecidable. In the paper under review the author proves that for certain n this problem is undecidable for any language which has a nonmonadic constant and at least n function variables.