シグネチャ (論理学)

数理論理学において、シグネチャ（テンプレート:Lang-en-short）とは、形式言語の非論理記号を記述したものである。普遍代数学では、シグネチャは代数的構造を特徴づける演算の一覧を与える。モデル理論では、シグネチャは両方の目的に用いられる。より哲学的な論理学の取り扱いにおいて、シグネチャが明示されることはまれである。

定義

形式的には、（単一ソートの）シグネチャは4つ組 $\sigma =(S_{\mathrm{func}},S_{\mathrm{rel}},S_{\mathrm{const}},\mathrm{ar}),$ として定義される。ここで $S_{\mathrm{func}}$ と $S_{\mathrm{rel}}$ は、他の基本的な論理記号を含まない互いに素な集合であり、それぞれ次のように呼ばれる。

• 関数記号（例: $+,\times$）
• 関係記号 あるいは 述語（例: $\le ,\in$）
• 定数記号（例: $0,1$）

さらに、すべての関数記号・関係記号に対してアリティと呼ばれる自然数を割り当てる関数 $\mathrm{ar}:S_{\mathrm{func}}\cup S_{\mathrm{rel}}\to \mathbb{N}$ が与えられる。関数記号または関係記号のアリティが $n$ であるとき、その記号は $n$ 項であるという。著者によっては0項の関数記号を定数記号と定義することがあり、そうでない場合には定数記号が別個に定義される。

関数記号を持たないシグネチャは関係シグネチャと呼ばれ、関係記号を持たないシグネチャは代数シグネチャと呼ばれる。 有限シグネチャとは、$S_{\mathrm{func}}$ と $S_{\mathrm{rel}}$ がともに有限であるようなシグネチャのことである。より一般に、シグネチャ $\sigma =(S_{\mathrm{func}},S_{\mathrm{rel}},S_{\mathrm{const}},\mathrm{ar})$ の濃度は $|\sigma |=\left|S_{\mathrm{func}}\right|+\left|S_{\mathrm{rel}}\right|+\left|S_{\mathrm{const}}\right|$ と定義される。

シグネチャの言語とは、そのシグネチャに属する記号と論理体系の記号とから構成される、整式であるすべての文の集合である。

その他の慣用

普遍代数学では、「シグネチャ」の同義語として型あるいは相似型という語がしばしば用いられる。モデル理論では、シグネチャ $\sigma$ はしばしば語彙と呼ばれ、あるいはそれが非論理記号を提供する（一階の）言語 $L$ と同一視される。ただし、言語 $L$ の濃度は常に無限であり、$\sigma$ が有限であれば $|L|$ は ${\mathrm{\aleph }}_0$ となる。

形式的な定義は日常的な使用には不便であるため、特定のシグネチャの定義はしばしば次のように略式で書かれる。

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

また、代数シグネチャが単なるアリティの列とみなされることもある。

「アーベル群の相似型は $\sigma =(2,1,0)$ である。」

形式的には、これはシグネチャの関数記号を $f_2$（2項）、$f_1$（単項）、$f_0$（0項）のように定義することになるが、実際にはこの慣用に関しても通常の名称が用いられる。

数理論理学では、記号が0項であることを許さないことが非常に多くテンプレート:要出典、そのため定数記号は0項の関数記号としてではなく別個に扱われなければならない。それらは $S_{\mathrm{func}}$ と互いに素な集合 $S_{\mathrm{const}}$ をなし、その上ではアリティ関数 $\mathrm{ar}$ は定義されない。しかしこれは事態を複雑にするだけであり、特に論理式の構造に関する帰納法による証明では、追加の場合分けを考慮しなければならなくなる。そのような定義の下では同様に許されない0項の関係記号は、単項の関係記号と、その値がすべての元について同一であることを述べる文とによって模倣することができる。この翻訳が失敗するのは空構造の場合のみである（空構造は慣例上除外されることが多い）。0項記号が許されるならば、命題論理のすべての論理式は一階述語論理の論理式でもある。

無限シグネチャの例としては、無限のスカラー体 $F$ 上のベクトル空間に関する式や方程式を形式化するために $S_{\mathrm{func}}=\{+\}\cup \{f_a:a\in F\}$ および $S_{\mathrm{rel}}=\{=\}$ を用いるものがある。ここで各 $f_a$ は $a$ によるスカラー倍という単項演算を表す。このようにすれば、ベクトルを唯一のソートとして、シグネチャと論理を単一ソートに保つことができる。

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

一階述語論理の文脈では、シグネチャに属する記号は非論理記号としても知られる。これは、論理記号とともに、2つの形式言語（シグネチャ上の項の集合と、シグネチャ上の（整式である）論理式の集合）が帰納的に定義される際の基礎となるアルファベットをなすからである。

構造においては、解釈が関数記号と関係記号を、その名にふさわしい数学的対象に結びつける。領域 $A$ をもつ構造 $𝐀$ における $n$ 項関数記号 $f$ の解釈は関数 $f^{𝐀}:A^n\to A$ であり、$n$ 項関係記号の解釈は関係 $R^{𝐀}\subseteq A^n$ である。ここで $A^n=A\times A\times \cdots \times A$ は領域 $A$ 自身の $n$ 重直積を表し、したがって $f$ は実際に $n$ 項関数であり、$R$ は $n$ 項関係である。

多ソートのシグネチャ

多ソート論理および多ソート構造に対しては、シグネチャはソートに関する情報を符号化しなければならない。そのための最も直接的な方法は、一般化されたアリティの役割を果たす記号型を用いることである。

記号型

$S$ を、記号 $\times$ と $\to$ を含まない（ソートの）集合とする。

$S$ 上の記号型とは、アルファベット $S\cup \{\times ,\to \}$ 上のある種の語である。すなわち、非負整数 $n$ と $s_1,s_2,\dots ,s_n,s^{\prime }\in S$ に対する、関係的記号型 $s_1\times \cdots \times s_n$ と関数的記号型 $s_1\times \cdots \times s_n\to s^{\prime }$ である（$n=0$ のとき、式 $s_1\times \cdots \times s_n$ は空語を表す）。

シグネチャ

（多ソートの）シグネチャとは、次のものからなる三つ組 $(S,P,\mathrm{type})$ である。

• ソートの集合 $S$
• 記号の集合 $P$
• $P$ の各記号に $S$ 上の記号型を対応させる写像 $\mathrm{type}$

関連項目

• 項代数

参考文献

• テンプレート:Cite book Free online edition.
• テンプレート:Cite book

外部リンク

• Stanford Encyclopedia of Philosophy: "Model theory" — by Wilfred Hodges.
• PlanetMath: Entry "Signature" describes the concept for the case when no sorts are introduced.
• Baillie, Jean, "An Introduction to the Algebraic Specification of Abstract Data Types."