David M. Cerna ; Julian Parsert - One is all you need: Second-order Unification without First-order Variables

lmcs:15782 - Logical Methods in Computer Science, April 9, 2026, Volume 22, Issue 2 - https://doi.org/10.46298/lmcs-22(2:3)2026
One is all you need: Second-order Unification without First-order VariablesArticle

Authors: David M. Cerna ; Julian Parsert

We introduce a fragment of second-order unification, referred to as \emph{Second-Order Ground Unification (SOGU)}, with the following properties: (i) only one second-order variable is allowed, and (ii) first-order variables do not occur. We study an equational variant of SOGU where the signature contains \textit{associative} binary function symbols (ASOGU) and show that Hilbert's 10$^{th}$ problem is reducible to ASOGU unifiability, thus proving undecidability. Our reduction provides a new lower bound for the undecidability of second-order unification, as previous results required first-order variable occurrences, multiple second-order variables, and/or equational theories involving \textit{length-reducing} rewrite systems. Furthermore, our reduction holds even in the case when associativity of the binary function symbol is restricted to \emph{power associative}, i.e. f(f(x,x),x)= f(x,f(x,x)), as our construction requires a single constant.


Volume: Volume 22, Issue 2
Published on: April 9, 2026
Imported on: June 2, 2025
Keywords: Logic in Computer Science