機能述語

形式論理および数学の関連分野において、関数述語、または関数記号は、オブジェクト項に適用されて別のオブジェクト項を生成する論理記号です。関数述語はマッピングと呼ばれることもありますが、この用語には数学では追加の意味があります。モデルでは、関数記号は関数によってモデル化されます。

具体的には、形式言語のシンボルFが関数シンボルであるとは、その言語でオブジェクトを表す任意のシンボルXが与えられたときに、 F ( X )がやはりその言語でオブジェクトを表すシンボルであることを意味します。型付きロジックでは、型Tのオブジェクトを表す任意のシンボルXが与えられたときに、F ( X ) が型Uのオブジェクトを表すシンボルである場合、Fはドメイン型Tおよびコドメイン型Uを持つ関数シンボルです。複数の変数を持つ関数シンボルを同様に定義することもできます。これは、複数の変数を持つ関数に似ています。変数が0個の関数シンボルは、単なる定数シンボルです。

ここで、形式言語のモデルを考えてみましょう。型TとUは集合[ T ]と[ U ]でモデル化され、型Tの各シンボルXは[ T ]の要素[ X ]でモデル化されます。すると、Fは集合

[F]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \}},

これは単純に定義域 [ 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 を満たす同一性述語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型のすべてのXと、 U型の一意のYに対して、P ( X , Y ) は、

すると、次の式を満たすドメイン型Tとコドメイン型Uの関数シンボルF を導入できます。

T型のすべてのX、U型のすべてのYについて、Y = F ( X )の場合にのみP ( X , Y )となります。

関数述語を使わない

述語論理の多くの処理では、関数述語は許可されておらず、関係述語のみが許可されています。これは、たとえば、新しい関数記号 (または他の新しい記号) の導入を許可したくないメタ論理定理 (ゲーデルの不完全性定理など) を証明するコンテキストで役立ちます。ただし、関数記号が出現する場所では、関数記号を関係記号に置き換える方法があります。さらに、これはアルゴリズム的であるため、ほとんどのメタ論理定理を結果に適用するのに適しています。

具体的には、F がドメイン型Tとコドメイン型U を持つ場合、型 ( T、U ) の述語Pに置き換えることができます。直感的には、P ( X、Y ) はF ( X ) = Yを意味します。その後、ステートメントにF ( X ) が出現するたびに、それを型Uの新しいシンボルYに置き換え、別のステートメントP ( X、Y ) を含めることができます。同じ推論を行うには、追加の命題が必要です。

T型のすべてのXと、U型の一意のYに対して、P ( X , Y ) となります。

(もちろん、これは前のセクションで新しい関数記号を導入する前に定理として証明する必要があった命題と同じです。)

機能述語の除去は、いくつかの目的には便利であり、また可能であるため、形式論理の多くの処理では、機能記号を明示的には扱わず、関係記号のみを使用します。別の考え方としては、機能述語は特別な種類の述語であり、具体的には上記の命題を満たす述語であるということです。機能述語Fにのみ適用される命題スキーマを指定したい場合、これは問題のように思えるかもしれません。その条件を満たすかどうかを事前に知るにはどうすればよいのでしょうか。スキーマの同等の定式化を得るには、まず形式F ( X ) のすべてを新しい変数Yに置き換えます。次に、対応するXが導入された直後(つまり、Xが量化された後、またはXが自由であればステートメントの先頭) に各Yに対して普遍量化し、量化をP ( X , Y )でガードします。最後に、ステートメント全体を上記の機能述語の一意性条件の重要な帰結にします。