hide
Free keywords:
-
Abstract:
\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}
