関数記号
テンプレート:Otheruses テンプレート:出典の明記 形式体系、特に数理論理学において、関数記号（かんすうきごう、テンプレート:Lang-en-short）とは、議論領域上の関数あるいは写像を表す非論理記号の一種である。ただし形式的には、実際には何も表さなくてもよい。関数記号は項を形成するための形式言語の基本的構成要素である。具体的には、記号 が関数記号であるとき、言語上の対象を表す任意の定数記号 に対して、 もまた言語上の対象を表す。同様に、 がその言語における項であれば、 もまた項である。したがって、関数記号の解釈は議論領域全体にわたって定義されていなければならない。関数記号は原始概念であり、それゆえに、より基本的な他の概念を用いて定義されない。
テンプレート:仮リンクにおいて、記号 F が定義域の型 T および値域の型 U をもつ関数記号であるとは、型 T の対象を表す任意の記号 X に対して、F(X) が型 U の対象を表す記号となることをいう。多変数の関数と同様に、多変数の関数記号も同じように定義できる。0 変数の関数記号は単に定数記号である。
いま、形式言語のモデルにおいて、型 T および U が集合 [T] と [U] によってモデル化され、型 T の各記号 X が [T] の元 [X] によってモデル化されているとする。このとき F は以下の集合によってモデル化される。
これは単に、定義域 [T] および値域 [U] をもつ関数である。矛盾のないモデルとしては、[X] = [Y] のときは常に [F(X)] = [F(Y)] となることが要求される。
新しい関数記号の導入
新しい述語記号の導入を許す述語論理の扱いでは、新しい関数記号も導入できるようにしたい。関数記号 F と G が与えられているとき、新しい関数記号 F ∘ G を、F と G の合成として、あらゆる X に対して (F ∘ G)(X) = F(G(X)) を満たすものとして導入できる。もちろん、型付き論理においてはこの等式の右辺は、F の定義域の型が G の値域の型と一致していない限り意味をなさないため、合成が定義されるにはこの一致が必要である。
自動的に得られる関数記号もある。型なし論理においては、あらゆる X に対して id(X) = X を満たす恒等述語（identity predicate）id が存在する。型付き論理においては、任意の型 T に対して、定義域と値域の型がともに T である恒等述語 idT が存在し、型 T のあらゆる X に対して idT(X) = X を満たす。同様に、T が U の部分型である場合、定義域の型を T、値域の型を U とする包含述語（inclusion predicate）が存在し、同じ等式を満たす。また、古い型から新しい型を構築する他の方法に付随する追加の関数記号も存在する。
さらに、適切な定理を証明したうえで、関数的述語（functional predicate）を定義することもできる。（定理の証明後に新しい記号を導入することが許されない形式体系で作業している場合には、次節に示すように、これを回避するために関係記号を用いなければならない）。具体的には、任意の X（あるいは特定の型のあらゆる X）に対して、条件 P を満たす一意の Y が存在することを証明できれば、これを示すために関数記号 F を導入することができる。これはテンプレート:仮リンクと呼ばれる。ここで P は、X と Y の両方に関わる関係的な述語である。したがって、そのような述語 P と、次の定理が存在する場合を考える：
- 型 T の任意の X に対して、P(X, Y) を満たす型 U の一意の Y が存在する。
このとき、定義域の型を T、値域の型を U とする関数記号 F を導入し、次を満たすものとして定めることができる：
- 型 T の任意の X および型 U の任意の Y に対して、P(X, Y) であることは Y = F(X) であることと同値である。
関数的述語を使わずにすませる
述語論理の多くの扱いでは、関数的述語を許さず、関係的な述語しか許さない。これはたとえば、ゲーデルの不完全性定理のようなメタ論理的定理を証明する文脈で有用である。そこでは新しい関数記号（また、そもそもあらゆる新しい記号）の導入を許したくないからである。しかし、関数記号が出現しうる箇所では、それを関係記号に置き換える方法が存在する。しかも、それはアルゴリズム的であり、したがって多くのメタ論理的定理をその結果に適用するのに適している。
具体的には、F が定義域の型 T、値域の型 U をもつとき、これを型 (T, U) の述語 P で置き換えることができる。直観的には、P(X, Y) は F(X) = Y を意味する。すると、F(X) が言明中に現れるときは常に、それを型 U の新しい記号 Y で置き換え、追加の言明 P(X, Y) を含めればよい。同じ推論を行えるようにするために、以下の追加の命題が必要となる：
（もちろん、これは前節で新しい関数記号を導入する前に定理として証明する必要のあった命題と同じである。）
関数的述語の消去はある目的にとって便利であり、しかも可能であるため、多くの形式論理の扱いでは関数記号を明示的には扱わず、関係記号のみを用いる。これは別の見方をすれば、関数的述語は述語の特殊な種類、すなわち上記の命題を満たすものである、ということでもある。関数的述語 F のみに適用される命題スキーマを規定したい場合、これは問題に見えるかもしれない。事前に、F がその条件を満たすかどうかをどう知ればよいのか。同等の定式化を得るには、まず F(X) の形をしたものすべてを新しい変数 Y で置き換える。次に、対応する X が導入された直後（すなわち X が量化された後、あるいは X が自由変数である場合には言明の冒頭）で各 Y を全称量化し、その量化を P(X, Y) で守る。最後に、言明全体を、上に示した関数的述語の一意性条件の物質的帰結とする。
例として、ツェルメロ＝フレンケル集合論における置換公理図式を取り上げよう。（この例では数学記号を用いる。）この図式は、1 変数の任意の関数的述語 F に対して、次の（一つの形式の）主張をする：
まず、F(C) を別の変数 D に置き換えなければならない：
もちろんこの言明は正しくない。D は C の直後で量化されなければならない：
さらに、この量化を守るために P を導入しなければならない：
これはほぼ正しいが、あまりにも多くの述語に適用されてしまう。実際に必要なのは次の形である：
このバージョンの置換公理図式は、これで新しい関数記号の導入を許さない形式言語での使用に適したものとなった。あるいは、元の言明をそのような形式言語における言明として解釈することもできる。それは、末尾で得られる言明の略記にすぎなかったのである。
未解釈関数
未解釈関数（テンプレート:Lang-en-short）[1]とは、その名称と n 項形以外に何の性質も持たない関数である。未解釈関数の理論は、自由に生成されるがゆえに自由対象となる自由理論（free theory）、あるいは始代数に類比してのことだが文の空集合をもつ理論としての空理論（empty theory）とも呼ばれる。空でない等式集合をもつ理論はテンプレート:仮リンクとして知られる。自由理論の充足可能性問題はテンプレート:仮リンクによって解かれる。この単一化のためのアルゴリズムは、Prolog などのさまざまなコンピュータ言語のインタプリタで用いられている。統語論的単一化は、他のある種の等式理論に対する充足可能性問題のアルゴリズムでも用いられる。詳細はユニフィケーションを参照。
例
SMT-LIB における未解釈関数の例として、SMT ソルバに次の入力を与えると:
(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]。
自由理論は、共通部分式を探索してテンプレート:仮リンクを形成することで解ける。ソルバには充足可能性モジュロ理論ソルバなどが含まれる。