署名（ロジック）

数理論理学において、シグネチャとは形式言語の非論理記号の記述である。普遍代数において、シグネチャは代数構造を特徴付ける演算を列挙する。モデル理論において、シグネチャは両方の目的で用いられる。論理学のより哲学的な扱いにおいて、シグネチャが明示的に示されることは稀である。

意味

正式には、（単一ソート）署名は、4つの組として定義することができ、ここで、およびは、それぞれと呼ばれる他の基本論理記号を含まない 互いに素な集合である。${\displaystyle \sigma =\left(S_{\operatorname {func} },S_{\operatorname {rel} },S_{\operatorname {const} },\operatorname {ar} \right),}$ ${\displaystyle S_{\operatorname {func} }}$ ${\displaystyle S_{\operatorname {rel} }}$

• 関数記号（例：）、${\displaystyle +,\times }$
• 関係記号または述語（例：）、${\displaystyle \,\leq ,\,\in }$
• 定数記号（例：）、${\displaystyle 0,1}$

そして、すべての関数または関係記号にアリティと呼ばれる自然数を割り当てる関数です。関数または関係記号は、そのアリティが-aryである場合に-aryと呼ばれます。一部の著者は、ゼロアリティ（-ary）の関数記号を定数記号として定義し、そうでない場合は定数記号は別途定義されます。 ${\displaystyle \operatorname {ar} :S_{\operatorname {func} }\cup S_{\operatorname {rel} }\to \mathbb {N} }$ ${\displaystyle n}$ ${\displaystyle n.}$ ${\displaystyle 0}$

関数記号を含まないシグネチャは関係署名と呼ばれ、関係記号を含まない署名は代数的署名。 ^{[ 1 ]} A有限署名とは、とが有限でような署名である。より一般的には、署名の濃度は次のように定義される。${\displaystyle S_{\operatorname {func} }}$ ${\displaystyle S_{\operatorname {rel} }}$ ${\displaystyle \sigma =\left(S_{\operatorname {func} },S_{\operatorname {rel} },S_{\operatorname {const} },\operatorname {ar} \right)}$ ${\displaystyle |\sigma |=\left|S_{\operatorname {func} }\right|+\left|S_{\operatorname {rel} }\right|+\left|S_{\operatorname {const} }\right|.}$

その署名の言語とは、その署名内のシンボルと論理システム内のシンボルから構築された、適切に形成されたすべての文の集合です。

その他の条約

普遍代数学では、入力または類似性タイプは「シグネチャ」の同義語としてよく使われる。モデル理論では、シグネチャはしばしば${\displaystyle \sigma }$ 語彙、あるいは非論理記号 を提供する（第一階）言語 。しかし、言語の濃度は常に無限である。が有限である。 ${\displaystyle L}$ ${\displaystyle L}$ ${\displaystyle \sigma }$ ${\displaystyle |L|}$ ${\displaystyle \aleph_{0}}$

正式な定義は日常使用には不便であるため、特定の署名の定義は次のように非公式に省略されることがよくあります。

「アーベル群の標準的なシグネチャは、単項演算子です。」${\displaystyle \sigma =(+,-,0),}$ ${\displaystyle -}$

代数的シグネチャは、次のように、単なる引数のリストとして扱われることがあります。

「アーベル群の相似型は」${\displaystyle \sigma =(2,1,0).}$

正式には、シグネチャの関数シンボルは(これは 2 項)、(これは 1 項)、(これは 0 項) のように定義されますが、実際にはこの規則に関連しても通常の名前が使用されます。 ${\displaystyle f_{2}}$ ${\displaystyle f_{1}}$ ${\displaystyle f_{0}}$

数理論理学では、多くの場合、記号はゼロ引数であることが許されないため、定数記号はゼロ引数関数記号としてではなく、別個に扱う必要があります。定数記号は、引数関数が定義されていないものとは互いに素な集合を形成します。しかし、このことは、特に式の構造に対する帰納法による証明では追加のケースを考慮しなければならないため、問題を複雑にするだけです。ゼロ引数関係記号も、このような定義では許されませんが、その値はすべての要素で同じであることを表す文を添えた単項関係記号でエミュレートできます。この変換は、空の構造（慣例により除外されることが多い）の場合のみ失敗します。ゼロ引数記号が許される場合、命題論理のすべての式は、一階述語論理の式でもあります。 ${\displaystyle S_{\operatorname {const} }}$ ${\displaystyle S_{\operatorname {func} },}$ ${\displaystyle \operatorname {ar} }$

無限署名の例では、とを使用して、無限スカラー体上のベクトル空間に関する式と方程式を形式化します。ここで、それぞれは、によるスカラー乗算の単項演算を表します。このようにして、署名とロジックは、ベクトルが唯一のソートである状態で、単一ソートされた状態に保つことができます。^{[ 2 ]}${\displaystyle S_{\operatorname {func} }=\{+\}\cup \left\{f_{a}:a\in F\right\}}$ ${\displaystyle S_{\operatorname {rel} }=\{=\}}$ ${\displaystyle F,}$ ${\displaystyle f_{a}}$ ${\displaystyle a.}$

論理と代数におけるシグネチャの使用

第一階論理の文脈では、署名内の記号は非論理記号とも呼ばれます。これは、署名内の記号が論理記号とともに、署名上の項の集合と署名上の（整形式の）式の集合という 2 つの形式言語を帰納的に定義する基礎となるアルファベットを形成するためです。

構造では、解釈によって関数記号と関係記号が、その名前を正当化する数学的オブジェクトに結び付けられます。定義域を持つ構造 内の- 項関数記号の解釈は関数であり、 - 項関係記号の解釈は関係です。ここで は定義域とそれ自身の-倍直積を表すため、 は実際には- 項関数であり、-項関係です。 ${\displaystyle n}$ ${\displaystyle f}$ ${\displaystyle \mathbf {A} }$ ${\displaystyle A}$ ${\displaystyle f^{\mathbf {A} }:A^{n}\to A,}$ ${\displaystyle n}$ ${\displaystyle R^{\mathbf {A} }\subseteq A^{n}.}$ ${\displaystyle A^{n}=A\times A\times \cdots \times A}$ ${\displaystyle n}$ ${\displaystyle A}$ ${\displaystyle f}$ ${\displaystyle n}$ ${\displaystyle R}$ ${\displaystyle n}$

多種多様な署名

多ソート論理および多ソート構造の場合、シグネチャはソートに関する情報をエンコードする必要があります。これを行う最も簡単な方法は、一般化されたアリティの役割を果たすシンボル型。 ^{[ 3 ]}

シンボルの種類

を記号を含まない集合（のようなもの）とする。${\displaystyle S}$ ${\displaystyle \times }$ ${\displaystyle \to .}$

上の記号型は、アルファベット上の特定の単語です。関係記号型と、非負の整数および関数記号型です(式は空の単語を表します)。 ${\displaystyle S}$ ${\displaystyle S\cup \{\times ,\to \}}$ ${\displaystyle s_{1}\times \cdots \times s_{n},}$ ${\displaystyle s_{1}\times \cdots \times s_{n}\to s^{\prime },}$ ${\displaystyle n}$ ${\displaystyle s_{1},s_{2},\ldots ,s_{n},s^{\prime }\in S.}$ ${\displaystyle n=0,}$ ${\displaystyle s_{1}\times \cdots \times s_{n}}$

サイン

（多ソート）署名は、以下の三つ組から構成される。 ${\displaystyle (S,P,\operatorname {type} )}$

• ある種のセット、${\displaystyle S}$
• 一連のシンボル、そして${\displaystyle P}$
• シンボルタイプ内のすべてのシンボルに関連付けられたマップ${\displaystyle \operatorname {type} }$ ${\displaystyle P}$ ${\displaystyle S.}$

参照

• 項代数 – 与えられた署名上で自由に生成された代数構造

注記

1. Mokadem, Riad; Litwin, Witold; Rigaux, Philippe; Schwarz, Thomas (2007年9月). 「代数的署名を用いてエンコードされたデータに対するnGramベースの高速文字列検索」(PDF) .第33回国際超大規模データベース会議 (VLDB) . 2019年2月27日閲覧.
2. George Grätzer (1967). 「IV. 普遍代数」. James C. Abbot (編). Trends in Lattice Theory . プリンストン/ニュージャージー: Van Nostrand. pp.  173– 210.ここ: p.173。
3. Many-Sorted Logic 、 Calogero G. Zarba著のLecture notes on Decision Proceduresの第 1 章。

参考文献

• バリス、スタンリー・N.; サンカッパナヴァール、H.P. (1981). 『普遍代数講座』シュプリンガー. ISBN 3-540-90578-2。無料のオンライン版。
• ホッジス、ウィルフリッド（1997年）『短縮モデル理論』ケンブリッジ大学出版局、ISBN 0-521-58713-1。

外部リンク

• スタンフォード哲学百科事典：「モデル理論」—ウィルフレッド・ホッジス著。
• PlanetMath:エントリ「Signature」は、ソートが導入されていない場合の概念について説明します。
• Baillie, Jean、「抽象データ型の代数仕様入門」