【定理】\(\varphi\)は量化子・演算子・\(x\)以外の変項を含まない論理式で、\(\mathcal{A}\)は\(\varphi\)をその上の論理式とする最小の言語であるとする。このとき\[\vDash\exists x\varphi\Longleftrightarrow\ \vDash\bigvee_{\tau\in H_\mathcal{A}}\varphi[\tau/x]\]が成り立つ。
（証明）\(\vDash\exists x\varphi\)と仮定すると、\(\mathcal{A}\)上の任意のエルブラン解釈\(\langle H,h\rangle\)に対し\([\![\varphi]\!]_{H,h[x\mapsto \tau]}=1\)すなわち\([\![\varphi[\tau/x]]\!]_{H,h}=1\)なる\(\tau\in H_\mathcal{A}\)が存在するが、いま\(H_\mathcal{A}\)が有限集合であることに注意すると、これは\([\![\bigvee_{\tau\in H_\mathcal{A}}\varphi[\tau/x]]\!]_{H,h}=1\)と言い換えられる。この論理式は量化子を含まないので、補題5.105から恒真となる。
逆に\(\vDash\bigvee_{\tau\in H_\mathcal{A}}\varphi[\tau/x]\)と仮定すると、各\(\tau_i\in H_\mathcal{A}\)について\(\varphi[\tau_i/x]\vDash\exists x\varphi\)であることに対し構成的両刃論法・カットを有限回施すことにより\(\vDash\exists x\varphi\)が導かれる。■
