Kripke-Platek set theory

The Kripke–Platek axioms of set theory (KP), pronounced /ˈkrɪpki ˈplɑːtɛk/, are a system of axiomatic set theory developed by Saul Kripke and Richard Platek.

KP is considerably weaker than Zermelo–Fraenkel set theory (ZFC), and can be thought of as roughly the predicative part of ZFC. The consistency strength of KP with an axiom of infinity is given by the Bachmann–Howard ordinal. Unlike ZFC, KP does not include the power set axiom, and KP includes only limited forms of the axiom of separation and axiom of replacement from ZFC. These restrictions on the axioms of KP lead to close connections between KP, generalized recursion theory, and the theory of admissible ordinals.

Here, a Σ₀, or Π₀, or Δ₀ formula is one all of whose quantifiers are bounded. This means any quantification is the form ${\displaystyle \forall u\in v}$ or ${\displaystyle \exists u\in v.}$ (More generally, we would say that a formula is Σ_n+1 when it is obtained by adding existential quantifiers in front of a Π_n formula, and that it is Π_n+1 when it is obtained by adding universal quantifiers in front of a Σ_n formula: this is related to the arithmetical hierarchy but in the context of set theory.)

...
Wikipedia