エルブランの定理

エルブランの定理は、ジャック・エルブラン（1930）によって得られた数理論理学の基本的な結果である。 ^{[1]それは本質的に、}一階述語論理を命題論理にある種の還元することを可能にする。エルブランの定理は、ほとんどの自動定理証明器の論理的基礎である。エルブランはもともと一階述語論理の任意の式に対して定理を証明したが、^{[2]ここで示した、}存在量指定子のみを含む冠頭形式の式に制限したより単純なバージョンの方が人気が高まった。

させて

${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$

は、量指定子のない一階述語論理の式であるが、追加の自由変数を含む場合がある。このバージョンのエルブランの定理は、上記の式が、おそらく言語の拡張における有限の項 列が存在する場合にのみ有効であることを述べている。 ${\displaystyle F(y_{1},\ldots,y_{n})}$ ${\displaystyle t_{ij}}$

${\displaystyle 1\leq i\leq r}$そして、${\displaystyle 1\leq j\leq n}$

そのような

${\displaystyle F(t_{11},\ldots ,t_{1n})\vee \ldots \vee F(t_{r1},\ldots ,t_{rn})}$

有効である。有効である場合、それはエルブラン選言と呼ばれる。

${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n}).}$

非公式には、存在量指定子のみを含む冠頭形式の式は、量指定子のない部分式の置換インスタンスで構成される選言がトートロジー（命題的に導出可能）である場合に限り、一階述語論理で証明可能（有効）である。 ${\displaystyle A}$${\displaystyle A}$

存在量指定子のみを含む冠頭形式の式への制限は、定理の一般性を制限するものではありません。なぜなら、式は冠頭形式に変換でき、その全称量指定子はHerbrandizationによって削除できるからです。構造的Herbrandization を実行すれば、冠頭形式への変換を回避できます。Herbrandization は、Herbrand 論理和で許可される変数依存関係に追加の制限を課すことで回避できます。

定理の非自明な方向の証明は、次の手順で構築できます。

1. 式が正しい場合、ゲンツェンのカット除去定理から導かれるカットフリーシーケント計算の完全性により、 のカットフリー証明が存在します。${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$ ${\displaystyle \vdash (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$
2. 葉から始めて下に向かって作業し、存在量指定子を導入する推論を削除します。
3. 以前存在量化された式の縮約推論を削除します。これは、量化子推論の削除後に式 (以前に量化された変数が用語に置き換えられたもの) が同一ではなくなる可能性があるためです。
4. 縮約を除去すると、シーケントの右側にある の関連する置換インスタンスがすべて蓄積され、 の証明が得られ、そこからエルブラン選言が得られます。${\displaystyle F(y_{1},\ldots,y_{n})}$${\displaystyle \vdash F(t_{11},\ldots ,t_{1n}),\ldots ,F(t_{r1},\ldots ,t_{rn})}$

しかし、エルブランの証明の時点ではシーケント計算とカット消去法は知られておらず、エルブランはより複雑な方法で定理を証明しなければならなかった。

• エルブランの定理は、展開木証明を使用することで高階論理に拡張されました。 ^[3]展開木証明の深い表現は、一階論理に制限すると、エルブランの選言に対応します。
• エルブラン選言と拡張ツリー証明は、カットの概念によって拡張されました。カット除去の複雑さのため、カットを含むエルブラン選言は、標準的なエルブラン選言よりも非要素的に小さくなる可能性があります。
• エルブラン選言はエルブラン シーケントに一般化されており、エルブランの定理をシーケントに対して述べることができます。「スコレム化されたシーケントは、エルブラン シーケントを持つ場合にのみ導出可能です。」

• エルブラン構造
• エルブランの解釈
• エルブランの宇宙
• コンパクト性定理

• Buss, Samuel R. (1995)、「エルブランの定理について」、Maurice, Daniel、Leivant, Raphaël (編)、『論理と計算の複雑さ』、Lecture Notes in Computer Science、ベルリン、ニューヨーク: Springer-Verlag、pp. 195–209、ISBN 978-3-540-60178-4。