エルブランの解釈

数理論理学において、エルブラン解釈とは、すべての定数と関数記号に非常に単純な意味が割り当てられる解釈である。 ^[1]具体的には、すべての定数はそれ自身として解釈され、すべての関数記号は項への適用関数として解釈される。この解釈ではまた、述語記号が関連するエルブラン基底のサブセットを表すものとして定義され、どの基底原子が解釈において真であるかを効果的に指定する。これにより、一連の節内の記号を、実際のインスタンス化とは切り離して、純粋に統語的な方法で解釈することができる。

エルブラン解釈の重要性は、与えられた節集合S を満たす解釈が存在する場合、その節を満たすエルブラン解釈が存在するということです。さらに、エルブランの定理は、 Sが不満足な場合、 Sによって定義されたエルブラン宇宙からの基底インスタンスの有限の不満足な集合が存在すると述べています。この集合は有限であるため、その不満足性は有限時間内に検証できます。ただし、確認すべきそのような集合は無限に存在する可能性があります。