Emil: Thanks for explaining this patiently to an outsider!

Unfortunately I do not know what $PV_1$ is. Could you please define it or give a reference?

Note. The positive result of the Theorem can be obtained with just a finite fragment $Q^+$ of $IE_1^-$: Fix a Diophantine formula $\phi(x,y,z)$ representing some 2-ary universal partial computable function $f$ in $IE_1^-$, satisfying conditions 1 and 2. Let $Q^+:=Q+\forall x,y,z,z'(\phi(x,y,z)\wedge\phi(x,y,z')\rightarrow z=z')$. As $Q$ is $\Sigma_1$ complete, $\phi$ still represents $f$ in $Q^+$. Then by universality/coding, $Q^+$ represents all partially computable functions via Diophantine formulas, e.g. 2-ary functions via the formulas $\phi(\bar{e},(x+y)(x+y+1)+2x,z)$, $e\in\mathbb{N}$.

Emil: With the last edit, your answers now have considerably sharpened the boundary between theories which can (e.g. $IE_1^-$) or cannot (e.g. $Q$) witness essential incompleteness (or represent disjoint pairs of r.e. sets) via diophantine formulas - which was the intent of my original question. Splendid!

Yes, I think I see it now, thanks again! One more question: Does your counterexample for diophantine formulas generalize to $\exists$-formulas? Or is there a $\exists$-formula witnessing the essential incompleteness of $Q$? (A $\exists$-formula is one of the form $\exists \vec{y} \psi(\vec{x},\vec{y})$ with $\psi$ quantifier free.)

Thanks Emil! I will summarize your main counterexample as a separate answer, at least for my own benefit. A question on your finitely axiomatizable counterexample: $Q$ $+$ commutative semirings $+$ $\exists x \forall y (x+y=x)$. Let $D_0=$ the set of diophantine sentences of the form $\exists \vec{y}(f(\vec{y}) = g(\vec{y}))$ in which one of the polynomials $f$ and $g$ is a constant, and $D_1=$ the set of such sentences in which both $f$ and $g$ are non-constant. I see how this theory proves all sentences of $D_1$, but how does it prove all the $\neg\sigma$ for false $\sigma \in D_0$?