Note on a Translation to Characterize Constructivity

This note describes a straightforward translation $\mathcal C^{(1)}$ such that $T\vdash A(t)$ for some term $t$ $\Leftrightarrow$ $\mathcal C^{(1)}(T)\vdash \mathcal C^{(1)}(\exists xA(x))$ for universal $T$ and purely existential $\exists xA(x)$. The correspondence is based on the properties of resolution calculus.