The embeddability-complexity conjecture for finitely presented groups

Let $P_1,P_2,\ldots$ be an enumeration of all finite presentations of groups, with $P_i=\langle X_i\mid R_i\rangle$, and define

$$K=\{\langle i,j\rangle\in\mathbb{N}\mid \overline{P}_i\hookrightarrow\overline{P}_j\}.$$

Embeddability-complexity conjecture. The set $K$ is $\Sigma^0_3$-complete. Equivalently, deciding whether $\overline{P}_i$ embeds into $\overline{P}_j$ for finite presentations $P_i$ and $P_j$ is a $\Sigma^0_3$-complete problem. The preceding results establish that $K$ is $\Sigma^0_2$-hard and $\Pi^0_2$-hard and has a $\Sigma^0_3$ description; the conjecture asserts that this upper bound is sharp.