В теории моделей и связанных с ними областях математики, тип является объектом, который описывает, как элемент (реальный или возможно) или конечный набор элементов в математической структуре могут вести себя. Точнее, это набор формул первого порядка в языке L со свободными переменными x 1, x 2,…, x n, которые истинны для последовательности элементов L -структуры. В зависимости от контекста типы могут быть полными или частичными, и они могут использовать фиксированный набор констант A из структуры. Вопрос о том, какие типы представляют собой фактические элементы, приводит к идеям насыщенных моделей и опущенных типов.
Рассмотрим структуру для языка L. Пусть M - вселенная структуры. Для каждого A ⊆ M, пусть L () быть языком, полученный из L, добавив константу с для каждого а ∈ A. Другими словами,
1-типа (из) над А представляет собой набор р ( х) формул в L ( A) с не более одной свободной переменной х (следовательно, 1-типа), что для любого конечного подмножества р 0 ( х) ⊆ P ( x) существует некоторый b ∈ M, зависящий от p 0 ( x), с (т.е. все формулы в p 0 ( x) верны, когда x заменяется на b).
Точно так же n -тип (of) над A определяется как набор p ( x 1,…, x n) = p ( x) формул в L ( A), каждая из которых имеет свои свободные переменные, встречающиеся только среди заданных n свободные переменные x 1,…, x n, такие, что для любого конечного подмножества p 0 ( x) ⊆ p ( x) существуют элементы b 1,…, b n ∈ M с.
Полный тип из более чем А, что является одним максимальным по включению. Эквивалентное, для каждого либо или. Любой неполный тип называется частичным типом. Итак, слово тип в целом относится к любому n -типу, частичному или полному, по любому выбранному набору параметров (возможно, пустому набору).
П - типа р ( х) называетсяреализуется в, если существует элемент b ∈ M n такой, что. Существование такой реализации в гарантируются для любого типа по теореме компактности, хотя реализация может иметь место в некотором элементарном расширении из, а не в себе. Если полный тип реализуется с помощью Ь в, то тип обычно обозначается и называется полным типа Ь над А.
Тип p ( x) называется изолированным, если. Поскольку конечные подмножества типа всегда реализуются в, всегда существует элемент b ∈ M n такой, что φ ( b) истинно в ; т.е., таким образом, b реализует весь изолированный тип. Таким образом, изолированные типы будут реализованы в каждой элементарной подструктуре или расширении. Из-за этого нельзя исключать изолированные типы (см. Ниже).
Модель, которая реализует максимально возможное разнообразие типов, называется насыщенной моделью, а сверхмощная конструкция обеспечивает один из способов создания насыщенных моделей.
Рассмотрим язык с одной бинарной связкой, которую мы обозначим как. Позвольте быть структурой для этого языка, который является порядковым с его стандартным хорошим упорядочением. Пусть обозначает теорию.
Рассмотрим набор формул. Во-первых, мы утверждаем, что это тип. Позвольте быть конечным подмножеством. Нам нужно найти, что удовлетворяет всем формулам в. Что ж, мы можем просто взять преемника самого большого порядкового номера, упомянутого в наборе формул. Тогда он явно будет содержать все порядковые номера, упомянутые в. Таким образом, у нас есть тип. Далее обратите внимание, что не реализовано в. Ибо, если бы он был, были бы такие, которые содержали бы каждый элемент. Если бы мы хотели реализовать тип, у нас может возникнуть соблазн рассмотреть модель, которая на самом деле является супермоделью, реализующей тип. К сожалению, это расширение не элементарно, то есть данная модель удовлетворять не должна. В частности, приговору удовлетворяет данная модель, а не компания.
Итак, мы хотим реализовать тип в простейшем расширении. Мы можем сделать это, определив новую структуру на языке, которую мы будем обозначать. Область структуры будет где - набор целых чисел, украшенных таким образом, что. Обозначим через обычный порядок. Мы интерпретируем символ в нашей новой структуре как. Идея состоит в том, что мы добавляем « -цепочку» или копию целых чисел, прежде всего конечных ординалов. Ясно, что любой элемент реализует свой тип. Более того, можно убедиться, что это расширение элементарно.
Другой пример: полный тип числа 2 над пустым набором, рассматриваемым как член натуральных чисел, будет набором всех операторов первого порядка, описывающих переменную x, которые верны, когда x = 2. Этот набор будет включать в себя такие формулы, как,, и. Это пример изолированного типа, поскольку, работая над теорией натуральных чисел, формула подразумевает все другие формулы, которые верны относительно числа 2.
В качестве дальнейшего примера утверждения
и
описание квадратного корня из 2 согласуется с аксиомами упорядоченных полей и может быть расширено до полного типа. Этот тип не реализуется в упорядоченном поле рациональных чисел, но реализуется в упорядоченном поле вещественных чисел. Точно так же бесконечный набор формул (над пустым набором) {xgt; 1, xgt; 1 + 1, xgt; 1 + 1 + 1,...} не реализуется в упорядоченном поле действительных чисел, а реализуется в упорядоченном поле гиперреалов. Если мы разрешаем параметры, например, все вещественные числа, мы можем указать тип, который реализуется бесконечно малым гиперреальным, нарушающим свойство Архимеда.
Причина, по которой полезно ограничить параметры определенным подмножеством модели, заключается в том, что это помогает отличать типы, которые могут быть удовлетворены, от тех, которые не могут. Например, используя весь набор действительных чисел в качестве параметров можно генерировать несчетное бесконечное множество формул, как,... что бы явно исключает все возможные реальные значения для х, и, следовательно, не могут быть реализованы в пределах действительных чисел.
Множество полных n -типов над A полезно рассматривать как топологическое пространство. Рассмотрим следующее отношение эквивалентности формул в свободных переменных x 1,…, x n с параметрами в A:
Это можно показать тогда и только тогда, когда они содержатся в точно таких же полных типах.
Множество формул в свободных переменных x 1,…, x n над A с точностью до этого отношения эквивалентности является булевой алгеброй (и канонически изоморфно множеству A -определяемых подмножеств в M n). Полные n -типы соответствуют ультрафильтрам этой булевой алгебры. Набор полных n -типов можно превратить в топологическое пространство, взяв наборы типов, содержащие данную формулу, в качестве базовых открытых множеств. Это создает пространство Камня, которое является компактным, хаусдорфовым и полностью отключенным.
Пример. Полная теория алгебраически замкнутых полей в характерном 0 имеет квантор элиминации, что позволяет один, чтобы показать, что возможных полных 1-типов (по пустому множеству), соответствуют:
Другими словами, 1-типы в точности соответствуют первичным идеалам кольца многочленов Q [ x ] над рациональными числами Q: если r является элементом модели типа p, то идеал, соответствующий p, является множеством многочленов с корнем r (который является нулевым многочленом, если r трансцендентно). В более общем смысле, полные n -типы соответствуют первичным идеалам кольца многочленов Q [ x 1,..., x n ], другими словами, точкам простого спектра этого кольца. (Камень пространства топология может на самом деле следует рассматривать как Зарискому топологии в виде булева кольца индуцированного естественным образом из булевой алгебры. В то время как топология Зариской в общем случае не Хаусдорф, то в случае булевых колец). Например, если q ( x, y) - неприводимый многочлен от двух переменных, существует 2-тип, реализации которого (неформально) пары ( x, y) элементов с q ( x, y) = 0.
Для полного n -типа p можно спросить, существует ли модель теории, в которой p отсутствует, другими словами, в модели, реализующей p, нет n -набора. Если p - изолированная точка в пространстве Стоуна, т.е. если { p } - открытое множество, легко увидеть, что каждая модель реализует p (по крайней мере, если теория полна). Теорема об исключении типов говорит, что наоборот, если p не изолирован, то существует счетная модель, в которой p не используется (при условии, что язык счетный).
Пример: В теории алгебраически замкнутых полей характеристики 0 существует 1-тип, представленный элементами, трансцендентными над простым полем. Это неизолированная точка пространства Стоуна (фактически единственная неизолированная точка). Поле алгебраических чисел - это модель, в которой этот тип опускается, а алгебраическое замыкание любого трансцендентного расширения рациональных чисел - модель, реализующая этот тип.
Все остальные типы являются «алгебраическими числами» (точнее, они представляют собой наборы утверждений первого порядка, которым удовлетворяет некоторое заданное алгебраическое число), и все такие типы реализуются во всех алгебраически замкнутых полях характеристики 0.