Loading article…
形式体系、特に数理論理学において、関数記号は、議論領域上の関数または写像を表す非論理記号であるが、形式的には何も表す必要はない。関数記号は、形式言語において項を形成するための基本的な構成要素である。具体的には、記号がが関数記号である場合、任意の定数記号が与えられます。言語でオブジェクトを表す、また、言語内のオブジェクトも表します。同様に、言語の用語で、関数記号もまた用語である。そのため、関数記号の解釈は議論領域全体にわたって定義されなければならない。関数記号は原始的な概念であり、したがって他のより基本的な概念によって定義されるものではない。
型付き論理において、Fは、型Tのオブジェクトを表す任意のシンボルXが与えられたとき、F ( X ) が型Uのオブジェクトを表すシンボルである場合に、ドメイン型Tおよびコドメイン型Uの関数シンボルである。同様に、複数の変数を持つ関数と同様に、複数の変数を持つ関数シンボルを定義することもできる。変数がゼロの関数シンボルは、単に定数シンボルである。
ここで、形式言語のモデルを考えてみましょう。型TとUは集合[ T ] と [ U ]でモデル化され、型Tの各記号X は[ T ] の要素 [ X ]でモデル化されます。すると、F は集合でモデル化できます。
これは単に定義域 [ T ] と値域 [ U ]を持つ関数です。一貫性のあるモデルの要件は、[ X ] = [ Y ] のとき [ F ( X )] = [ F ( Y ) ]が成り立つことです。
述語論理において新しい述語記号を導入できるような扱い方をする場合、新しい関数記号も導入できるようにしたいものです。関数記号FとGが与えられたとき、すべての X に対して( F ∘ G )( X ) = F ( G ( X ))を満たす、 FとGの合成である新しい関数記号F ∘ Gを導入できます。もちろん、この等式の右辺は、 Fのドメイン型がGのコドメイン型と一致しない限り、型付き論理では意味をなさないため、合成を定義するにはこの一致が必要です。
また、特定の関数記号も自動的に得られます。型なし論理では、すべてのXに対してid( X ) = Xを満たす同一性述語id が存在します。型付き論理では、任意の型 T が与えられた場合、ドメイン型とコドメイン型がTである同一性述語 id Tが存在し、型TのすべてのXに対してid T ( X ) = X を満たします。同様に、T がUのサブタイプである場合、同じ等式を満たすドメイン型Tとコドメイン型Uの包含述語が存在します。古い型から新しい型を構築する他の方法に関連付けられた追加の関数記号もあります。
さらに、適切な定理を証明した後、関数述語を定義することもできます。（定理を証明した後に新しい記号を導入できない形式体系で作業している場合は、次のセクションのように、関係記号を使用してこの問題を回避する必要があります。）具体的には、すべてのX（または特定の型のすべてのX ）に対して、ある条件Pを満たす一意のYが存在することを証明できる場合、これを示す関数記号Fを導入できます。これは定義による拡張と呼ばれます。P自体は、 XとY の両方を含む関係述語であることに注意してください。したがって、そのような述語Pと定理がある場合、次のようになります。
すると、定義域型T、終域型Uの関数記号Fを導入することができ、それは以下の条件を満たす。
述語論理の多くの扱いでは、関数述語は許容されず、関係述語のみが許容されます。これは、例えば、メタ論理定理（ゲーデルの不完全性定理など）を証明する際に、新しい関数記号（あるいはその他の新しい記号）の導入を許容したくない場合に便利です。しかし、関数記号が出現する箇所すべてにおいて、関数記号を関係記号に置き換える方法があります。さらに、この方法はアルゴリズム的であるため、ほとんどのメタ論理定理を結果に適用するのに適しています。
具体的には、F がドメイン型Tとコドメイン型Uを持つ場合、F は型 ( T , U ) の述語Pに置き換えることができます。直感的に言えば、P ( X , Y ) はF ( X ) = Yを意味します。そして、文中にF ( X ) が現れるたびに、それを型Uの新しい記号Yに置き換え、別の文P ( X , Y ) を含めることができます。同じ推論を行うには、追加の命題が必要です。
（もちろん、これは前の節で新しい関数記号を導入する前に定理として証明しなければならなかった命題と同じものです。）
関数述語の排除は、いくつかの目的には便利で可能であるため、形式論理の多くの扱いでは関数記号を明示的に扱わず、代わりに関係記号のみを使用します。別の言い方をすれば、関数述語は特別な種類の述語であり、具体的には上記の命題を満たすものです。関数述語Fにのみ適用される命題スキーマを指定したい場合、これは問題のように思えるかもしれません。それがその条件を満たすかどうかを事前にどのように知るのでしょうか? スキーマの同等の定式化を得るには、まずF ( X ) の形式のものをすべて新しい変数Yに置き換えます。次に、対応するXが導入された直後(つまり、Xが量化された後、またはXが自由変数の場合はステートメントの先頭) に、各Yに対して全称量化を行い、量化をP ( X , Y )で保護します。最後に、ステートメント全体を上記の関数述語の一意性条件の実質的な帰結とします。
ツェルメロ＝フレンケル集合論における置換の公理図式を例にとってみましょう。（この例では数学記号を使用しています。）この図式は（ある形式で）1変数の任意の関数述語Fに対して、次のように述べます。
まず、F ( C )を別の変数Dに置き換える必要があります。
もちろん、この記述は正しくありません。DはC の直後に量化されなければなりません。
この定量化を保護するためには、Pを導入する必要がある。
これはほぼ正しいのですが、適用できる述語が多すぎます。私たちが本当に求めているのは次のことです。
この置換公理図式のバージョンは、新しい関数記号の導入を許容しない形式言語での使用に適しています。あるいは、元の記述をそのような形式言語の記述として解釈することもできます。それは単に、最後に生成された記述の省略形にすぎません。
解釈されない関数[ 1 ]とは、名前とn項形式以外の特性を持たない関数のことである。解釈されない関数の理論は、自由に生成されるため自由オブジェクトであることから自由理論、あるいは（初期代数になぞらえて）文の集合が空である理論であることから空理論とも呼ばれる。方程式の集合が空でない理論は、等式理論として知られている。自由理論の充足可能性問題は構文的統一によって解決される。後者のアルゴリズムは、Prologなどの様々なコンピュータ言語のインタプリタで使用されている。構文的統一は、他のいくつかの等式理論の充足可能性問題のアルゴリズムにも使用されている。統一（コンピュータ科学）を参照のこと。
SMT-LIB の未解釈関数の例として、この入力がSMT ソルバーに与えられた場合：
![{\displaystyle [F]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \}},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b4330f8ae04afd533c5bf1fbe3fc20c065056d4d)
(declare-fun f (Int) Int) (assert (= (f 10) 1)) SMTソルバーは「この入力は充足可能です」と返します。これは、がf未解釈関数（つまり、についてわかっているのはfそのシグネチャのみ）であるため、となる可能性があるからですf(10) = 1。しかし、以下の入力を適用すると：
(declare-fun f (Int) Int) (assert (= (f 10) 1)) (assert (= (f 10) 42)) SMTソルバーは「この入力は充足不可能です」と返します。これはf、関数である が同じ入力に対して異なる値を返すことは決してないためです。
自由理論の決定問題は、多くの理論がそれによって還元できるため、特に重要である。[ 2 ]
自由理論は、共通部分式を探索して合同閉包を形成することで解くことができる。解法には、充足可能性法理論の解法などが含まれる。