One is all you need: Second-order Unification without First-order Variables
<|reference_start|>One is all you need: Second-order Unification without First-order Variables: 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.<|reference_end|>
@article{cerna2024one,
    title={One is all you need: Second-order Unification without First-order
  Variables},
    author={David M. Cerna and Julian Parsert},
    journal={arXiv preprint arXiv:2404.10616},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.10616},
    primaryClass={cs.LO}
}