Тип (теория модели)

В теории моделей и смежных областях математики тип — это объект, который описывает, как может вести себя (реальный или возможный) элемент или конечный набор элементов в математической структуре . Точнее, это набор формул первого порядка языка L со свободными переменными x ₁ , x ₂ ,..., x _n, которые верны для набора из n -кортежей -структуры L . ${\mathcal {M}}$ . В зависимости от контекста типы могут быть полными или частичными и могут использовать фиксированный набор констант A из структуры. ${\mathcal {M}}$ . Вопрос о том, какие типы представляют собой действительные элементы ${\mathcal {M}}$ приводит к идеям насыщенных моделей и пропуска типов .

Формальное определение [ править ]

Рассмотрим структуру ${\mathcal {M}}$ для языка Л. Пусть M будет вселенной структуры. Для каждого A ⊆ M пусть L ( A ) — язык, полученный из добавлением константы для _ca каждого a ∈ A. L Другими словами,

L(A)=L\cup \{c_{a}:a\in A\}.

1 -тип (из ${\mathcal {M}}$ ) над A — это множество p ( x ) формул из L ( A ) не более чем с одной свободной переменной x (следовательно, 1-го типа) такое, что для любого конечного подмножества p ₀ ( x ) ⊆ p ( x ) существует некоторое b ∈ M в зависимости от p ₀ ( x ), причем ${\mathcal {M}}\models p_{0}(b)$ (т.е. все формулы из p ₀ ( x ) верны в ${\mathcal {M}}$ когда x заменяется на b ).

Аналогично n -тип (из ${\mathcal {M}}$ ) над A определяется как набор p ( x ₁ ,..., x _n ) = p ( x ) формул в L ( A ), каждая из которых имеет свои свободные переменные, встречающиеся только среди заданных n свободных переменных x ₁ , ..., x _n , такие, что для любого конечного подмножества p ₀ ( x ) ⊆ p ( x ) существуют некоторые элементы b ₁ ,..., b _n ∈ M такие, что ${\mathcal {M}}\models p_{0}(b_{1},\ldots ,b_{n})$ .

Полный тип ${\mathcal {M}}$ над A является максимальным по включению . Эквивалентно для каждого $\phi ({\boldsymbol {x}})\in L(A,{\boldsymbol {x}})$ или $\phi ({\boldsymbol {x}})\in p({\boldsymbol {x}})$ или $\lnot \phi ({\boldsymbol {x}})\in p({\boldsymbol {x}})$ . Любой неполный тип называется частичным типом . Таким образом, слово тип в целом относится к любому n -типу, частичному или полному, по любому выбранному набору параметров (возможно, пустому набору).

) n - типа p ( x Говорят, что реализуется в ${\mathcal {M}}$ если существует элемент b ∈ M ^н такой, что ${\mathcal {M}}\models p({\boldsymbol {b}})$ . Существование такой реализации гарантируется для любого типа теоремой компактности , хотя реализация может иметь место в некотором элементарном расширении ${\mathcal {M}}$ , а не в ${\mathcal {M}}$ сам. Если полный тип реализуется b в ${\mathcal {M}}$ , то тип обычно обозначается $tp_{n}^{\mathcal {M}}({\boldsymbol {b}}/A)$ называется полным типом b над A. и

Тип p ( x ) называется изолированным $\varphi$ , для $\varphi \in p(x)$ , если для всех $\psi ({\boldsymbol {x}})\in p({\boldsymbol {x}}),$ у нас есть $\operatorname {Th} ({\mathcal {M}})\models \varphi ({\boldsymbol {x}})\rightarrow \psi ({\boldsymbol {x}})$ . Поскольку конечные подмножества типа всегда реализуются в ${\mathcal {M}}$ , всегда существует элемент b ∈ M ^н такой, что φ ( b ) истинно в ${\mathcal {M}}$ ; т.е. ${\mathcal {M}}\models \varphi ({\boldsymbol {b}})$ , таким образом, b реализует весь изолированный тип. Таким образом, изолированные типы будут реализованы в каждой элементарной подструктуре или расширении. По этой причине изолированные типы никогда не могут быть опущены (см. ниже).

Модель, реализующая максимально возможное разнообразие типов, называется насыщенной моделью , а сверхмощная конструкция обеспечивает один из способов создания насыщенных моделей.

Примеры типов [ править ]

Рассмотрим язык L бинарного с одним символом отношения , который мы обозначим как $\in$ . Позволять ${\mathcal {M}}$ быть структурой $\langle \omega ,\in _{\omega }\rangle$ для этого языка, который является порядковым $\omega$ со своей стандартной упорядоченностью . Позволять ${\mathcal {T}}$ обозначают первого порядка теорию ${\mathcal {M}}$ .

Рассмотрим множество L (ω)-формул $p(x):=\{n\in _{\omega }x\mid n\in \omega \}$ . Во-первых, мы утверждаем, что это тип. Позволять $p_{0}(x)\subseteq p(x)$ быть конечным подмножеством $p(x)$ . Нам нужно найти $b\in \omega$ удовлетворяющее всем формулам $p_{0}$ . Ну, мы можем просто взять наследника наибольшего порядкового номера, упомянутого в наборе формул $p_{0}(x)$ . Тогда это явно будет содержать все порядковые номера, упомянутые в $p_{0}(x)$ . Таким образом, мы имеем это $p(x)$ это тип. Далее обратите внимание, что $p(x)$ не реализуется в ${\mathcal {M}}$ . Ибо если бы это было так, было бы что-то $n\in \omega$ который содержит каждый элемент $\omega$ . Если бы мы хотели реализовать тип, у нас могло бы возникнуть искушение рассмотреть структуру $\langle \omega +1,\in _{\omega +1}\rangle$ , что на самом деле является расширением ${\mathcal {M}}$ который реализует тип. К сожалению, это расширение не элементарно, например, оно не удовлетворяет ${\mathcal {T}}$ . В частности, приговор $\exists x\forall y(y\in x\lor y=x)$ удовлетворяется этой структурой, а не ${\mathcal {M}}$ .

Итак, мы хотим реализовать тип в элементарном расширении. Мы можем сделать это, определив новую L -структуру, которую мы обозначим ${\mathcal {M}}'$ . Домен структуры будет $\omega \cup \mathbb {Z} '$ где $\mathbb {Z} '$ — это набор целых чисел, оформленный таким образом, что $\mathbb {Z} '\cap \omega =\emptyset$ . Позволять $<$ обозначают обычный порядок $\mathbb {Z} '$ . Мы интерпретируем символ $\in$ в нашей новой структуре $\in _{{\mathcal {M}}'}=\in _{\omega }\cup <\cup \,(\omega \times \mathbb {Z} ')$ . Идея состоит в том, что мы добавляем " $\mathbb {Z}$ -цепочка», или копия целых чисел, прежде всего конечных порядковых номеров. Очевидно, что любой элемент $\mathbb {Z} '$ понимает тип $p(x)$ . Более того, можно проверить, что это расширение элементарно.

Другой пример: полный тип числа 2 над пустым множеством, рассматриваемый как член натуральных чисел, будет набором всех операторов первого порядка (на языке арифметики Пеано ), описывающих переменную x , которые true, когда x = 2. Этот набор будет включать такие формулы, как $\,\!x\neq 1+1+1$ , $x\leq 1+1+1+1+1$ , и $\exists y(y<x)$ . Это пример изолированного типа, так как при работе над теорией натуральных чисел формула $x=1+1$ подразумевает все остальные формулы, верные относительно числа 2.

В качестве еще одного примера можно привести утверждения

\forall y(y^{2}<2\implies y<x)

и

\forall y((y>0\land y^{2}>2)\implies y>x)

описывающие квадратный корень из 2, согласуются с аксиомами упорядоченных полей и могут быть расширены до полного типа. Этот тип не реализуется в упорядоченном поле рациональных чисел, но реализуется в упорядоченном поле действительных чисел. Аналогично бесконечное множество формул (над пустым множеством) {x>1, x>1+1, x>1+1+1, ...} не реализуется в упорядоченном поле действительных чисел, а реализуется в упорядоченном поле гиперреальности . Аналогично мы можем указать тип $\{0<x<1/n\mid n\in \mathbb {N} \}$ это реализуется бесконечно малой гиперреальностью, нарушающей архимедово свойство .

Причина, по которой полезно ограничить параметры определенным подмножеством модели, заключается в том, что это помогает отличить типы, которые могут быть удовлетворены, от тех, которые не могут быть удовлетворены. Например, используя весь набор действительных чисел в качестве параметров, можно сгенерировать неисчисляемый бесконечный набор формул вроде $x\neq 1$ , $x\neq \pi$ , ... это явно исключило бы все возможные действительные значения x и, следовательно, никогда не могло бы быть реализовано в действительных числах.

Каменные пространства [ править ]

полезно рассматривать Множество полных n -типов над A как топологическое пространство . Рассмотрим следующее отношение эквивалентности формул в свободных переменных x ₁ ,..., x _n с параметрами из A :

\psi \equiv \phi \Leftrightarrow {\mathcal {M}}\models \forall x_{1},\ldots ,x_{n}(\psi (x_{1},\ldots ,x_{n})\leftrightarrow \phi (x_{1},\ldots ,x_{n})).

Можно показать, что $\psi \equiv \phi$ тогда и только тогда, когда они содержатся в одних и тех же полных типах.

Множество формул в свободных переменных x ₁ ,..., x _n над A с точностью до этого отношения эквивалентности является булевой алгеброй (и канонически изоморфно множеству A -определимых подмножеств M ^н). Полные n -типы соответствуют ультрафильтрам этой булевой алгебры. Совокупность полных n наборы типов, содержащие данную формулу -типов можно превратить в топологическое пространство, взяв за основу открытых множеств . Это создает пространство Стоуна , связанное с булевой алгеброй, которое является компактным , Хаусдорфовым и полностью несвязным пространством.

Пример . Полная теория алгебраически замкнутых полей характеристики 0 имеет устранение кванторов , что позволяет показать, что возможные полные 1-типы (над пустым множеством) соответствуют:

Корни данного неприводимого непостоянного многочлена над рациональными числами со старшим коэффициентом 1. Например, тип квадратных корней из 2. Каждый из этих типов является изолированной точкой пространства Стоуна.
Трансцендентные элементы , которые не являются корнями какого-либо ненулевого многочлена. Этот тип представляет собой точку в пространстве Стоуна, которая является замкнутой, но не изолированной.

Другими словами, 1-типы в точности соответствуют простым идеалам кольца полиномов Q [ x ] над рациональными числами Q : если r — элемент модели типа p , то идеал, соответствующий p, — это множество многочленов с r в качестве корня (который является нулевым полиномом только в том случае, если r трансцендентный). В более общем смысле, полные n -типы соответствуют простым идеалам кольца полиномов Q [ x ₁ ,..., x _n ], другими словами, точкам простого спектра этого кольца. (Топологию пространства Стоуна на самом деле можно рассматривать как топологию Зариского булевого кольца , естественным образом индуцированную из булевой алгебры. Хотя топология Зариского в общем случае не является хаусдорфовой, она такова в случае булевых колец.) Например, , если q ( x , y ) является неприводимым полиномом от двух переменных, существует 2-тип, реализации которого представляют собой (неформально) пары ( x , y ) элементов с q ( x , y ) = 0.

Теорема типов исключении об

Учитывая полный n -тип p, можно задаться вопросом, существует ли модель теории, которая опускает p нет n , другими словами, в модели -кортежа, который реализует p . Если p — изолированная точка в пространстве Стоуна, т. е. если { p } — открытое множество, легко увидеть, что каждая модель реализует p (по крайней мере, если теория полна). Теорема об исключении типов гласит, что, наоборот, если p не изолирован, то существует счетная модель, опускающая p (при условии, что язык счетен).

Пример : В теории алгебраически замкнутых полей характеристики 0 существует 1-тип, представленный элементами, трансцендентными над полем Q. простым Это неизолированная точка пространства Стоуна (фактически единственная неизолированная точка). Поле алгебраических чисел — это модель, исключающая этот тип, и алгебраическое замыкание любого трансцендентальное расширение рационального является моделью, реализующей этот тип.

Все остальные типы являются «алгебраическими числами» (точнее, наборами утверждений первого порядка, которым удовлетворяет некоторое заданное алгебраическое число), и все такие типы реализуются во всех алгебраически замкнутых полях характеристики 0.

Ссылки [ править ]

Ходжес, Уилфрид (1997). Более короткая модель теории . Издательство Кембриджского университета . ISBN 0-521-58713-1 .
Чанг, CC ; Кейслер, Х. Джером (1989). Теория моделей (3-е изд.). Эльзевир . ISBN 0-7204-0692-7 .
Маркер, Дэвид (2002). Теория моделей: Введение . Тексты для аспирантов по математике . Том. 217. Спрингер. ISBN 0-387-98760-6 .