Типы в теории моделей

Введение

В теории моделей и смежных областях математики тип — это объект, описывающий возможное поведение (реального или потенциального) элемента или конечного множества элементов в математической структуре. Более точно, это множество формул первого порядка на языке L со свободными переменными x1, x2, …, xn, которые выполняются для некоторого набора n-кортежей в L-структуре. В зависимости от контекста, типы могут быть полными или частичными, и они могут использовать фиксированное множество констант A из структуры. Вопрос о том, какие типы соответствуют существующим элементам, приводит к понятиям насыщенных моделей и опущению типов.

Формальное определение

Рассмотрим структуру для языка L. Пусть M – вселенная структуры. Для каждого A ⊆ M, пусть L(A) будет языком, полученным из L путем добавления константы ca для каждого a ∈ A. Другими словами,

Consider a structure for a language L. Let M be the universe of the structure. For every A ⊆ M, let L(A) be the language obtained from L by adding a constant ca for every a ∈ A. In other words,

A 1 type (of ) over A is a set p(x) of formulas in L(A) with at most one free variable x (therefore 1 type) such that for every finite subset p0(x) ⊆ p(x) there is some b ∈ M, depending on p0(x), with (i. e. all formulas in p0(x) are true in when x is replaced by b). Similarly an n type (of ) over A is defined to be a set p(x1, ,xn) = p(x) of formulas in L(A), each having its free variables occurring only among the given n free variables x1, ,xn, such that for every finite subset p0(x) ⊆ p(x) there are some elements b1, ,bn ∈ M with
A complete type of over A is one that is maximal with respect to inclusion. Equivalently, for every either or Any non complete type is called a partial type. So, the word type in general refers to any n type, partial or complete, over any chosen set of parameters (possibly the empty set). An n type p(x) is said to be realized in if there is an element b ∈ Mn such that The existence of such a realization is guaranteed for any type by the compactness theorem, although the realization might take place in some elementary extension of , rather than in itself. If a complete type is realized by b in , then the type is typically denoted and referred to as the complete type of b over A. A type p(x) is said to be isolated by , for , if for all we have Since finite subsets of a type are always realized in , there is always an element b ∈ Mn such that φ(b) is true in ; i. e. , thus b realizes the entire isolated type. So isolated types will be realized in every elementary substructure or extension. Because of this, isolated types can never be omitted (see below). A model that realizes the maximum possible variety of types is called a saturated model, and the ultrapower construction provides one way of producing saturated models.

1-тип (над A) – это множество p(x) формул в L(A) с не более чем одной свободной переменной x (следовательно, 1-тип), такое что для каждого конечного подмножества p0(x) ⊆ p(x) существует некоторое b ∈ M, зависящее от p0(x), при котором (т.е. все формулы в p0(x) истинны, когда x заменено на b). Аналогично, n-тип (над A) определяется как множество p(x1, …, xn) = p(x) формул в L(A), каждая из которых имеет свои свободные переменные, встречающиеся только среди данных n свободных переменных x1, …, xn, такое что для каждого конечного подмножества p0(x) ⊆ p(x) существуют элементы b1, …, bn ∈ M, с

Полный тип (над A) – это тип, максимальный по включению. Эквивалентно, для каждого p либо либо . Любой неполный тип называется частичным типом. Таким образом, слово "тип" в общем случае относится к любому n-типу, частичному или полному, по любому выбранному набору параметров (возможно, пустому множеству). Говорят, что n-тип p(x) реализуется в M, если существует элемент b ∈ Mn, такой что . Существование такой реализации гарантируется для любого типа теоремой о компактности, хотя реализация может иметь место в некотором элементарном расширении M, а не в самом M. Если полный тип реализован в b в M, то этот тип обычно обозначается и называется полным типом b над A. Говорят, что тип p(x) изолирован M, если для всех у нас есть , поскольку конечные подмножества типа всегда реализуются в M, всегда существует элемент b ∈ Mn, такой что φ(b) истинно в M, т.е. , таким образом b реализует весь изолированный тип. Следовательно, изолированные типы будут реализованы в каждой элементарной подструктуре или расширении. Из-за этого изолированные типы никогда не могут быть опущены (см. ниже). Модель, которая реализует максимально возможное разнообразие типов, называется насыщенной моделью, а построение ультрастепени предоставляет один из способов получения насыщенных моделей.

Каменные пространства

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

It is useful to consider the set of complete n types over A as a topological space. Consider the following equivalence relation on formulas in the free variables x1, , xn with parameters in A:

One can show that if and only if they are contained in exactly the same complete types. The set of formulas in free variables x1, ,xn over A up to this equivalence relation is a Boolean algebra (and is canonically isomorphic to the set of A definable subsets of Mn). The complete n types correspond to ultrafilters of this Boolean algebra. The set of complete n types can be made into a topological space by taking the sets of types containing a given formula as a basis of open sets. This constructs the Stone space associated to the Boolean algebra, which is a compact, Hausdorff, and totally disconnected space. Example. The complete theory of algebraically closed fields of characteristic 0 has quantifier elimination, which allows one to show that the possible complete 1 types (over the empty set) correspond to:
Roots of a given irreducible non constant polynomial over the rationals with leading coefficient 1. For example, the type of square roots of 2. Each of these types is an isolated point of the Stone space. Transcendental elements, which are not roots of any non zero polynomial. This type is a point in the Stone space that is closed but not isolated. In other words, the 1 types correspond exactly to the prime ideals of the polynomial ring Q[x] over the rationals Q: if r is an element of the model of type p, then the ideal corresponding to p is the set of polynomials with r as a root (which is only the zero polynomial if r is transcendental). More generally, the complete n types correspond to the prime ideals of the polynomial ring Q[x1, ,xn], in other words to the points of the prime spectrum of this ring. (The Stone space topology can in fact be viewed as the Zariski topology of a Boolean ring induced in a natural way from the Boolean algebra. While the Zariski topology is not in general Hausdorff, it is in the case of Boolean rings.) For example, if q(x,y) is an irreducible polynomial in two variables, there is a 2 type whose realizations are (informally) pairs (x,y) of elements with q(x,y)=0.

Теорема опускания типов

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