The Kripke–Platek set theory with urelements (KPU) is an
axiom system for
set theory
Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
with
urelement
In set theory, a branch of mathematics, an urelement or ur-element (from the German prefix ''ur-'', 'primordial') is an object that is not a set, but that may be an element of a set. It is also referred to as an atom or individual.
Theory
There ...
s, based on the traditional (urelement-free)
Kripke–Platek set theory
The Kripke–Platek set theory (KP), pronounced , is an axiomatic set theory developed by Saul Kripke and Richard Platek.
The theory can be thought of as roughly the predicative part of ZFC and is considerably weaker than it.
Axioms
In its fo ...
. 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
In mathematics, in set theory, the constructible universe (or Gödel's constructible universe), denoted by , is a particular class of sets that can be described entirely in terms of simpler sets. is the union of the constructible hierarchy . It w ...
; KP is so weak that this is hard to do by
traditional means.
Preliminaries
The usual way of stating the axioms presumes a two sorted first order language
with a single binary relation symbol
.
Letters of the sort
designate urelements, of which there may be none, whereas letters of the sort
designate sets. The letters
may denote both sets and urelements.
The letters for sets may appear on both sides of
, while those for urelements may only appear on the left, i.e. the following are examples of valid expressions:
,
.
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.
Axioms
The axioms of KPU are the
universal closure
In mathematical logic, a universal quantification is a type of Quantification (logic), quantifier, a logical constant which is interpretation (logic), interpreted as "given any" or "for all". It expresses that a predicate (mathematical logic), pr ...
s of the following formulae:
*
Extensionality
In logic, extensionality, or extensional equality, refers to principles that judge objects to be equal if they have the same external properties. It stands in contrast to the concept of intensionality, which is concerned with whether the internal ...
:
*
Foundation
Foundation may refer to:
* Foundation (nonprofit), a type of charitable organization
** Foundation (United States law), a type of charitable organization in the U.S.
** Private foundation, a charitable organization that, while serving a good cause ...
: This is an
axiom schema In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.
Formal definition
An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables ap ...
where for every formula
we have
.
*
Pairing
In mathematics, a pairing is an ''R''-bilinear map from the Cartesian product of two ''R''-modules, where the underlying ring ''R'' is commutative.
Definition
Let ''R'' be a commutative ring with unit, and let ''M'', ''N'' and ''L'' be ''R''-modu ...
:
*
Union
Union commonly refers to:
* Trade union, an organization of workers
* Union (set theory), in mathematics, a fundamental operation on sets
Union may also refer to:
Arts and entertainment
Music
* Union (band), an American rock group
** ''Un ...
:
*
Δ0-Separation: This is again an
axiom schema In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.
Formal definition
An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables ap ...
, where for every
-formula
we have the following
.
*
-
Collection
Collection or Collections may refer to:
* Cash collection, the function of an accounts receivable department
* Collection (church), money donated by the congregation during a church service
* Collection agency, agency to collect cash
* Collectio ...
: This is also an
axiom schema In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.
Formal definition
An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables ap ...
, for every
-formula
we have
.
* Set Existence:
Additional assumptions
Technically these are axioms that describe the partition of objects into sets and urelements.
*
*
Applications
KPU can be applied to the model theory of
infinitary language An infinitary logic is a logic that allows infinitely long statements and/or infinitely long proofs. Some infinitary logics may have different properties from those of standard first-order logic. In particular, infinitary logics may fail to be compa ...
s.
Models
A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin ''modulus'', a measure.
Models c ...
of KPU considered as sets inside a maximal universe that are
transitive as such are called
admissible sets.
See also
*
Axiomatic set theory
Set theory is the branch of mathematical logic that studies Set (mathematics), sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, ...
*
Admissible set
*
Admissible ordinal In set theory, an ordinal number ''α'' is an admissible ordinal if L''α'' is an admissible set (that is, a transitive model of Kripke–Platek set theory); in other words, ''α'' is admissible when ''α'' is a limit ordinal and L''α'' ⊧ Σ0- ...
*
Kripke–Platek set theory
The Kripke–Platek set theory (KP), pronounced , is an axiomatic set theory developed by Saul Kripke and Richard Platek.
The theory can be thought of as roughly the predicative part of ZFC and is considerably weaker than it.
Axioms
In its fo ...
References
* .
* .
External links
{{DEFAULTSORT:Kripke-Platek Set Theory With Urelements
Systems of set theory
Urelements