モデル理論および関連する数学分野において、型とは、数学的構造における(実数または可能性のある)要素、あるいは有限個の要素の集合がどのように振る舞うかを記述する対象である。より正確には、型とは、自由変数x 1 , x 2 ,..., x nを持つ言語Lにおける一階述語論理式の集合であり、 L構造のn組の集合に対して真となるものである。文脈によっては、型は完全なものにも部分的なものにもなり得、構造体から固定定数セットAを使用する場合があります。実際の要素を表すタイプはどれかという問題飽和モデルや省略型といった概念につながる。
構造物について考えてみましょう言語Lについて。Mを構造の全体とする。すべてのA ⊆ Mに対して、L ( A ) を、すべてのa ∈ Aに対して定数c aを加えることによってLから得られる言語とする。言い換えれば、
1型() 上のAは、自由変数xが最大で 1 つであるL ( A )の式の集合p ( x ) であり、任意の有限部分集合p 0 ( x ) ⊆ p ( x ) に対して、 p 0 ( x )に依存するあるb ∈ Mが存在し、 。 言い換えると、より一般的には、n型 (A上の )は、 L ( A )の式の集合p ( x 1 ,..., x n ) = p ( x ) として定義され、各式の自由変数は、与えられたn個の自由変数x 1 ,..., x nの中にのみ出現し、任意の有限部分集合p 0 ( x ) ⊆ p ( x ) に対して、いくつかの要素b 1 ,..., b n ∈ Mが存在し、 。
完全なタイプのA上の は包含に関して最大である。言い換えれば、すべての に対してどちらか または 完全でない型は部分型と呼ばれます。たとえば、唯一の完全な 0 型は、すべての文の集合です。によってモデル化される。
一般的に「型」という言葉は、選択された任意のパラメータセット(空集合の場合もある)上の、部分的または完全なn型を指します。
n型p ( x )は、実現要素b ∈ M nが存在し、 コンパクト性定理により、任意の型が実現可能であるが、その実現はの何らかの基本的な拡張で行われる可能性がある。ではなくそれ自体。完全型がbによって実現される場合すると、その型は通常次のように表記されます。そして、 A上のbの完全型 と呼ばれます。
型p ( x ) は、、 のためにすべての場合我々は持っています型の有限部分集合は常に実現されるため常に、 φ ( b )が真となる要素b ∈ M nが存在する。 ; つまりしたがって、b は完全な孤立型を実現します。そのため、孤立型はすべての基本部分構造または拡張で実現されます。このため、孤立型を省略することはできません(下記参照)。
1つの二項関係記号を持つ言語Lを考えます。これを次のように表します。。 させて構造物であるこの言語では、序数標準的な整列順序を持つ。は、。
L (ω)式の集合を考えるまず、これは型であると主張します。有限部分集合である見つける必要があるすべての公式を満たすでは、一連の式の中で言及されている最大の順序数の次の数を取るだけでよい。そうすれば、明らかに、ここで言及されているすべての序数が含まれることになります。したがって、次のようになります。は型です。次に、実現しないなぜなら、もしそうであれば、あらゆる要素を含む型を実現したい場合、構造を検討したくなるかもしれません。これは確かに型を実現する。残念ながら、この拡張は基本的ではなく、例えば、特に、次の文この構造によって満たされ、。
そこで、基本拡張で型を実現したい。これは、新しいL構造を定義することによって実現できる。これを次のように表記する。構造のドメインはどこは、次のように装飾された整数の集合です。。 させて通常の順序を示す我々はその記号を解釈する新しい構造では。つまり、私たちは「-チェーン」、または整数のコピー、とりわけ有限順序数。明らかに、そのタイプを認識するさらに、この拡張が基本的なものであることを検証できる。
別の例として、自然数のメンバーとして考えた場合、空集合上の数 2 の完全な型は、変数xを記述するすべての一次命題 (ペアノ算術の言語で) の集合であり、 x = 2のときに真となるものです。この集合には、次のような式が含まれます。 、、 そしてこれは孤立型の例です。自然数の理論に基づいて計算すると、式は次のようになります。これは、数2に関して真である他のすべての公式を暗示する。
さらに例として、声明
そして
2の平方根を表す式は順序体の公理と整合しており、完全な型に拡張できます。この型は有理数の順序体では実現されませんが、実数の順序体では実現されます。同様に、(空集合上の)無限の式の集合{x>1, x>1+1, x>1+1+1, ...}は実数の順序体では実現されませんが、超実数の順序体では実現されます。同様に、型を指定できます。それは、アルキメデスの性質に違反する無限小の超実数によって実現される。
パラメータをモデルの特定の部分集合に制限することが有用な理由は、満たすことができる型と満たすことができない型を区別するのに役立つからです。たとえば、実数全体をパラメータとして使用すると、次のような数えきれないほどの式が生成される可能性があります。、、…これはxのあらゆる可能な実数値を明確に排除するため、実数の範囲内で実現することは決してできません。
A上の完全なn型集合を位相空間として考えることは有用である。Aのパラメータを持つ自由変数x 1 ,..., x nの式に関する次の同値関係を考える。
示すことができるのはそれらがまったく同じ完全型に含まれている場合に限ります。
この同値関係までのA上の自由変数x 1 ,..., x nの式の集合はブール代数であり(そして、M nのA定義可能な部分集合の集合と正準的に同型である)。完全なn型は、このブール代数の超フィルターに対応する。完全なn型の集合は、与えられた式を含む型の集合を開集合の基底とすることで位相空間にすることができる。これにより、ブール代数に関連付けられたストーン空間が構築される。これはコンパクトでハウスドルフ空間であり、完全に不連結な空間である。
例。標数0の代数的閉体の完全理論には量化子消去があり、それによって(空集合上の)可能な完全1型が以下に対応することを示すことができる。
言い換えれば、1型は有理数体Q上の多項式環Q [ x ]の素イデアルに正確に対応します。rが型pのモデルの要素である場合、 pに対応するイデアルはr を根とする多項式の集合です( rが超越数の場合は零多項式のみ)。より一般的には、完全なn型は多項式環Q [ x 1 ,..., x n ]の素イデアル、つまりこの環の素スペクトルの点に対応します。 (ストーン空間の位相は、実際にはブール代数から自然な方法で誘導されるブール環のザリスキー位相と見なすことができます。ザリスキー位相は一般にはハウスドルフ位相ではありませんが、ブール環の場合はハウスドルフ位相です。)例えば、 q ( x , y )が2変数の既約多項式である場合、q ( x , y )=0となる要素のペア( x , y )が(非公式に)実現される2型が存在します。
完全なn型pが与えられたとき、 pを省略する 理論モデルが存在するかどうか、言い換えれば、pを実現するnタプルがモデルに存在しないかどうかを問うことができる。pがストーン空間の孤立点、つまり { p } が開集合である場合、すべてのモデルがp を実現することは容易にわかる(少なくとも理論が完全である場合)。省略型定理は、逆にpが孤立点ではない場合、 pを省略する可算モデルが存在することを述べている(言語が可算である場合)。
例:標数0の代数的閉体の理論では、素体Q上の超越元によって表される1型が存在する。これはストーン空間の非孤立点である(実際には唯一の非孤立点である)。代数的数の体はこの型を省略したモデルであり、有理数の任意の超越拡大の 代数的閉包はこの型を実現するモデルである。
他のすべての型は「代数的数」(より正確には、与えられた代数的数によって満たされる一階述語論理の命題の集合)であり、そのようなすべての型は、標数0のすべての代数的に閉じた体で実現される。