The Kripke–Platek set theory (KP), pronounced , is an
axiomatic 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 concern ...
developed by
Saul Kripke
Saul Aaron Kripke (; November 13, 1940 – September 15, 2022) was an American philosopher and logician in the analytic tradition. He was a Distinguished Professor of Philosophy at the Graduate Center of the City University of New York and e ...
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 formulation, a Δ
0 formula is one all of whose quantifiers are
bounded. This means any quantification is the form
or
(See the
Lévy hierarchy In set theory and mathematical logic, the Lévy hierarchy, introduced by Azriel Lévy in 1965, is a hierarchy of formulas in the formal language of the Zermelo–Fraenkel set theory, which is typically called just the language of set theory. Thi ...
.)
*
Axiom of extensionality: Two sets are the same if and only if they have the same elements.
*
Axiom of induction: φ(''a'') being a
formula
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
, if for all sets ''x'' the assumption that φ(''y'') holds for all elements ''y'' of ''x'' entails that φ(''x'') holds, then φ(''x'') holds for all sets ''x''.
*
Axiom of empty set: There exists a set with no members, called the
empty set
In mathematics, the empty set is the unique set having no elements; its size or cardinality (count of elements in a set) is zero. Some axiomatic set theories ensure that the empty set exists by including an axiom of empty set, while in othe ...
and denoted .
*
Axiom of pairing
In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of pairing is one of the axioms of Zermelo–Fraenkel set theory. It was introduced by as a special case of his axiom of elementary set ...
: If ''x'', ''y'' are sets, then so is , a set containing ''x'' and ''y'' as its only elements.
*
Axiom of union: For any set ''x'', there is a set ''y'' such that the elements of ''y'' are precisely the elements of the elements of ''x''.
*
Axiom of Δ0-separation: Given any set and any Δ
0 formula φ(''x''), there is a
subset
In mathematics, set ''A'' is a subset of a set ''B'' if all elements of ''A'' are also elements of ''B''; ''B'' is then a superset of ''A''. It is possible for ''A'' and ''B'' to be equal; if they are unequal, then ''A'' is a proper subset of ...
of the original set containing precisely those elements ''x'' for which φ(''x'') holds. (This is an
axiom schema.)
*
Axiom of Δ0-collection: Given any Δ
0 formula φ(''x'', ''y''), if for every set ''x'' there exists a set ''y'' such that φ(''x'', ''y'') holds, then for all sets ''X'' there exists a set ''Y'' such that for every ''x'' in ''X'' there is a ''y'' in ''Y'' such that φ(''x'', ''y'') holds.
Some but not all authors include an
*
Axiom of infinity
In axiomatic set theory and the branches of mathematics and philosophy that use it, the axiom of infinity is one of the axioms of Zermelo–Fraenkel set theory. It guarantees the existence of at least one infinite set, namely a set containing th ...
KP with infinity is denoted by KPω. These axioms lead to close connections between KP,
generalized recursion theory
A generalization is a form of abstraction whereby common properties of specific instances are formulated as general concepts or claims. Generalizations posit the existence of a domain or set theory, set of elements, as well as one or more commo ...
, and the theory of
admissible ordinals.
KP can be studied as a
constructive set theory by dropping the
law of excluded middle
In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradi ...
, without changing any axioms.
Empty set
If any set
is postulated to exist, such as in the axiom of infinity, then the axiom of empty set is redundant because it is equal to the subset
. Furthermore, the existence of a member in the universe of discourse, i.e., ∃x(x=x), is implied in certain formulations
[, note at end of §2.3 on page 27: "Those who do not allow relations on an empty universe consider (∃x)x=x and its consequences as theses; we, however, do not share this abhorrence, with so little logical ground, of a vacuum."] of
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
, in which case the axiom of empty set follows from the axiom of Δ
0-separation, and is thus redundant.
Comparison with Zermelo-Fraenkel set theory
As noted, the above are weaker than ZFC as they exclude the
power set axiom, choice, and sometimes infinity. Also the axioms of separation and collection here are weaker than the corresponding axioms in ZFC because the formulas φ used in these are limited to bounded quantifiers only.
The axiom of induction in the context of KP is stronger than the usual
axiom of regularity
In mathematics, the axiom of regularity (also known as the axiom of foundation) is an axiom of Zermelo–Fraenkel set theory that states that every non-empty set ''A'' contains an element that is disjoint from ''A''. In first-order logic, the a ...
, which amounts to applying induction to the complement of a set (the class of all sets not in the given set).
Related definitions
* A set
is called
admissible if it is
transitive and
is a
model of Kripke–Platek set theory.
* An
ordinal number
In set theory, an ordinal number, or ordinal, is a generalization of ordinal numerals (first, second, th, etc.) aimed to extend enumeration to infinite sets.
A finite set can be enumerated by successively labeling each element with the leas ...
''
'' is called an
admissible ordinal if
L'''' is an admissible set.
* L
'''' is called an amenable set if it is a standard model of KP set theory without the axiom of Δ
0-collection.
Theorems
Admissible sets
The ordinal ''α'' is an admissible ordinal if and only if ''α'' is a
limit ordinal and there does not exist a ''γ'' < ''α'' for which there is a Σ
1(L
''α'') mapping from ''γ'' onto ''α''. If ''M'' is a standard model of KP, then the set of ordinals in ''M'' is an admissible ordinal.
Cartesian products exist
Theorem:
If ''A'' and ''B'' are sets, then there is a set ''A''×''B'' which consists of all
ordered pair
In mathematics, an ordered pair (''a'', ''b'') is a pair of objects. The order in which the objects appear in the pair is significant: the ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a'') unless ''a'' = ''b''. (In con ...
s (''a'', ''b'') of elements ''a'' of ''A'' and ''b'' of ''B''.
Proof:
The set (which is the same as by the axiom of extensionality) and the set both exist by the axiom of pairing. Thus
:
exists by the axiom of pairing as well.
A possible Δ
0 formula expressing that ''p'' stands for (''a'', ''b'') is:
:
::
Thus a superset of ''A''× = exists by the axiom of collection.
Denote the formula for ''p'' above by
. Then the following formula is also Δ
0
:
Thus ''A''× itself exists by the axiom of separation.
If ''v'' is intended to stand for ''A''×, then a Δ
0 formula expressing that is:
:
Thus a superset of exists by the axiom of collection.
Putting
in front of that last formula and we get from the axiom of separation that the set itself exists.
Finally,
''A''×''B'' = exists by the axiom of union.
Q.E.D.
Q.E.D. or QED is an initialism of the Latin phrase , meaning "which was to be demonstrated". Literally it states "what was to be shown". Traditionally, the abbreviation is placed at the end of mathematical proofs and philosophical arguments in pri ...
Metalogic
The
consistency strength of KPω is given by the
Bachmann–Howard ordinal
In mathematics, the Bachmann–Howard ordinal (also known as the Howard ordinal, or Howard-Bachmann ordinal) is a large countable ordinal.
It is the proof-theoretic ordinal of several mathematical theories, such as Kripke–Platek set theory (wi ...
.
See also
*
Constructible universe
*
Admissible ordinal
*
Kripke–Platek set theory with urelements
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 ...
References
Bibliography
*
*
*
*
{{DEFAULTSORT:Kripke-Platek set theory
Systems of set theory