On the Undecidability of Second-Order Unification

There is a close relationship between word unification and second-order unification. This similarity has been exploited, for instance, in order to prove decidability of monadic second-order unification and decidability of linear second-order unification when no second-order variable occurs more than twice. The attempt to prove the second result for (nonlinear) second-order unification failed and led instead to a natural reduction from simultaneous rigid E-unification to this second-order unification. This reduction is the first main result of this paper, and it is the starting point for proving some novel results about the undecidability of second-order unification presented in the rest of the paper. We prove that second-order unification is undecidable in the following three cases: (1) each second-order variable occurs at most twice and there are only two second-order variables; (2) there is only one second-order variable and it is unary; (3) the following conditions (i)–(iv) hold for some fixed integer n: (i) the arguments of all second-order variables are ground terms of size <n, (ii) the arity of all second-order variables is <n, (iii) the number of occurrences of second-order variables is ⩽5, (iv) there is either a single second-order variable or there are two second-order variables and no first-order variables.