Введение
Система математической теории множеств Теория множеств Крипке-Платека с элементами (KPU) - это система аксиом для теории множеств с элементами, основанная на традиционной (без элементов) теории множеств Крипке-Платека. Она значительно слабее (относительно) знакомой системы ZFU. Целью допуска урелементов является возможность включения больших или высокосложных объектов (таких как множество всех действительных) в транзитивные модели теории без нарушения обычных теоретических свойств хорошо упорядоченности и рекурсии конструктивной вселенной; KP настолько слаб, что это трудно сделать традиционными средствами.
The Kripke–Platek set theory with urelements (KPU) is an axiom system for set theory with urelements, based on the traditional (urelement free) Kripke–Platek set theory. It is considerably weaker than the (relatively) familiar system ZFU. The purpose of allowing urelements is to allow large or high complexity objects (such as the set of all reals) to be included in the theory's transitive models without disrupting the usual well ordering and recursion theoretic properties of the constructible universe; KP is so weak that this is hard to do by traditional means.
Предварительные
Обычный способ формулирования аксиомы предполагает два сортированных языка первого порядка с одним символом двоичной связи. Буквы такого рода обозначают элементы, которых может не быть, тогда как буквы такого рода обозначают множества. Буквы могут обозначать как множества, так и элементы. Буквы множеств могут появляться по обе стороны , в то время как буквы элементов могут появляться только слева, т.е. ниже приведены примеры действительных выражений: , Заявление аксиомы также требует ссылки на определенный набор формул, называемых формулами. Коллекция состоит из тех формул, которые могут быть построены с использованием констант, , , , и ограниченного количественного определения. Это количественное определение формы или места данного набора.
The statement of the axioms also requires reference to a certain collection of formulae called formulae. The collection consists of those formulae that can be built using the constants, , , , , and bounded quantification. That is quantification of the form or where is given set.
Дополнительные предположения
Технически это аксиомы, которые описывают разделение объектов на множества и элементы.
Приложения
КПУ может быть применено к теории моделей инфинитарных языков. Модели КПУ, рассматриваемые как множества внутри максимальной вселенной и являющиеся транзитивными по своей природе, называются допустимыми множествами.