エルブランの定理
( t 1 , t 2 , . . . , t n {\displaystyle t_{1},t_{2},...,t_{n}} は変数 a 1 , a 2 , . . . , a n {\displaystyle a_{1},a_{2},...,a_{n}} をエルブラン領域の要素で置き換えたもの)
前と同様、上の(2)と(3)はエルブランの定理の別の表現であり、(1)、(2)、(3)は同値である。
ここで、F が充足不能のとき(すなわち G = ¬F が恒真のとき)を考える。 Q ( a 1 , . . . , a n ) {\displaystyle Q(a_{1},...,a_{n})} を n = 1 {\displaystyle n=1} 、 n = 2 {\displaystyle n=2} と調べていくと、 Q ( a 1 , . . . , a n ) {\displaystyle Q(a_{1},...,a_{n})} が偽となるような n が存在する(そうでなければ全ての n で真となるため充足可能となってしまう)。またその逆も成り立つ。 これを利用し、任意の恒真な論理式 G の証明を行いたい場合、論理式の否定 ¬G の充足不能性を調べることで、エルブラン解釈の下での有限回の操作で調べることができる。
G = ¬F、R = ¬Q、S = ¬P と置いて双対を考えると、上と等価な3つの特性を得ることができる。
G {\displaystyle G} は証明可能(provable)、つまり命題論理の演繹システムで G {\displaystyle G} を導くことができること。これは次のように表記する: ⊢ G {\displaystyle \vdash G}
G {\displaystyle G} は恒真(valid)、つまり G {\displaystyle G} は全てのモデルで真になる。これは次のように表記する: ⊨ G {\displaystyle \vDash G} .
ある n {\displaystyle n} に対し、以下の R ( a 1 , . . . , a n ) {\displaystyle R(a_{1},...,a_{n})} が恒真になるような n {\displaystyle n} が存在すること。これは次のように表記する: ⊨ R ( a 1 , . . . , a n ) {\displaystyle \vDash R(a_{1},...,a_{n})}
S ( t 1 , t 1 ) ∨ S ( t 1 , t 2 ) ∨ S ( t 2 , t 1 ) ∨ ⋯ ∨ S ( t 1 , t n ) ∨ ⋯ ∨ S ( t n − 1 , t n ) ∨ S ( t n , t 1 ) ∨ ⋯ ∨ S ( t n , t n ) {\displaystyle S(t_{1},t_{1})\lor S(t_{1},t_{2})\lor S(t_{2},t_{1})\lor \cdots \lor S(t_{1},t_{n})\lor \cdots \lor S(t_{n-1},t_{n})\lor S(t_{n},t_{1})\lor \cdots \lor S(t_{n},t_{n})}