伝統的エルブラン理論

伝統的エルブラン理論を定義し直したいのだけど、とりあえず伝統的エルブラン理論の概念・用語をまとめておく。

構文は、変数、定数、関数、述語（記号達）で構成する。関数と述語を最初から明白に区別するのが特徴。変数、定数、関数で項を作り、それと述語と論理結合子（例えば∧、⊃、¬）で論理式を作る。ソート（型記号）はあってもなくてもよいが、ソート付きを考える。

変数を含まない項を基礎項（ground term）、論理結合子を含まない（述語だけ）の論理式は原子論理式（atomic formula）と呼ぶ。論理式の集まりを公理系と呼ぶことにする。

ソートがsの基礎項の全体をソートsのエルブラン空間またはエルブラン宇宙（Herbrand universe）と呼ぶ。ソートsのの基礎項に述語を適用した形である原子論理式の全体をソートsのエルブラン基底（Herbrand base）と呼ぶ。エルブラン基底をエルブラン領域と訳すこともあるが、良くないと思うので使わない。

各ソートに集合を対応させ、各ソートの基礎項に集合の要素を対応させ、関数記号に写像を、述語記号に集合の部分集合を対応させることを解釈（intepretation）と呼ぶ。ソートsにそのエルブラン空間を対応させ、基礎項や関数も自明nに拡張して対応付ける解釈をエルブラン解釈と呼ぶ。

Aが公理系であるとき、Aに含まれる論理式が真になるような解釈で、しかもエルブラン解釈であるものをAのエルブラン・モデルと呼ぶ。Aが空のときは、Aのエルブラン・モデルは単なるエルブラン解釈なので、エルブラン解釈とエルブラン・モデルを神経質に区別する必要はない。

ソートsごとにエルブラン基底の部分集合を与えることと、エルブラン解釈は１：１に対応する。公理系Aに対して、論理式pが妥当であることは、すべてのモデルを検査する必要はなくて、Aのエルブラン・モデルだけを調べればいいことが知られている。