$\forall\exists^\ast$-Equational Theory of Context Unification is $\Pi_1^0$-Hard

\begin{abstract} Context unification is a particular case of second-order unification, where all second-order variables are \emph{unary} and only \emph{linear} functions are sought for as solutions. Its decidability is an open problem. We present the simplest (currently known) undecidable quantified fragment of the theory of \emph{context unification} by showing that for every signature containing a $\geq\!2$-ary symbol one can construct a \emph{context equation} ${\mathcal E}\,(p,r,\overline{F},\overline{w})$ with parameter $p$, first-order variables $r$, $\overline{w}$, and context variables $\overline{F}$ such that the set of true sentences of the form \[\forall r\;\exists\;\overline{F}\;\exists\;\overline{w}\;\; {\mathcal E}(p,r,\overline{F},\overline{w})\] is $\Pi_1^0$-hard (i.e., every co-r.e. set is many-one reducible to it), as $p$ ranges over finite words of a binary alphabet. Moreover, the existential prefix above contains just 5 context and 3 first-order variables. \end{abstract