エルブランの定理
, y n ) {\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})} が恒真になる必要十分条件は、ある自然数 k {\displaystyle k} とエルブラン領域の項 t i 1 , ... , t i n {\displaystyle t_{i1},\ldots ,t_{in}} ( 1 ≤ i ≤ k {\displaystyle 1\leq i\leq k} )が存在し、
F ( t 11 , ... , t 1 n ) ∨ ... ∨ F ( t k 1 , ... , t k n ) {\displaystyle F(t_{11},\ldots ,t_{1n})\vee \ldots \vee F(t_{k1},\ldots ,t_{kn})}
が恒真になることである。
このようなエルブランの定理の証明は、ゲーデルの完全性定理により恒真性が証明可能性に置き換えられることを利用し、ゲンツェンのカット除去定理を用い ⊢ ( ∃ y 1 , ... , y n ) F ( y 1 , ... , y n ) {\displaystyle \vdash (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})} のカット規則を除去した証明を求めるものが一般的である。
エルブランが定理を証明した時にゲンツェンのカット除去定理はまだ知られておらず、ゲーデルの完全性定理も発表されていなかった。そのためエルブランによる証明はエルブラン版のカット除去定理や独自の完全性定理を含むもので、任意の一階述語論理式を対象としていた。