Kripke–Platek Set Theory (KP)

Origin. Saul Kripke and Richard Platek, independently around 1964, from the same motivation: a set theory whose models are the right setting for generalized recursion theory. Jon Barwise's Admissible Sets and Structures (1975) is the reference and is where the theory acquired its name and its audience. The abbreviation collides with Kreisel–Putnam logic, which is unrelated.

Models. ZF with the power set gone and separation and collection cut down to Δ₀ formulas — quantifiers bounded by sets. What remains is exactly the theory whose transitive models are the admissible sets, and admissibility is what recursion theory needs: a universe closed under the operations of a computation but not under taking all subsets. KP is where set theory and recursion theory are the same subject.

Formalism.

Axioms: Extensionality, Foundation, Pairing, Union, Δ₀-Separation, Δ₀-Collection. No Power Set. No full Separation. No full Collection. Infinity optional (KP vs KPω).

Δ₀ formulas: All quantifiers bounded: ∀x ∈ y, ∃x ∈ y. Absolute between transitive models — which is why they are the right restriction.

Δ₀-Collection: ∀x ∈ a ∃y φ(x,y) → ∃b ∀x ∈ a ∃y ∈ b φ(x,y), for φ ∈ Δ₀. The set b collects enough witnesses. This is the axiom doing the work.

Admissible sets: A transitive set A is admissible iff (A, ∈) ⊨ KP. L_α ⊨ KP iff α is an admissible ordinal. The least admissible ordinal above ω is ω₁^CK, the Church–Kleene ordinal — the least non-recursive ordinal, arriving here as a set-theoretic object.

Σ recursion: Σ-recursion and Σ-definability are available in KP; they are the generalization of ordinary recursion from ω to an arbitrary admissible set. α-recursion theory is recursion theory over L_α for α admissible.

Barwise compactness: For A countable admissible, any Σ theory in L_A that is A-finitely satisfiable is satisfiable. Compactness for infinitary logic, recovered exactly where the admissibility holds.

Strength: KPω is proof-theoretically far below ZF: its ordinal is the Bachmann–Howard ordinal. Much weaker than second-order arithmetic; comparable to ID₁.

Symbols.

Metatheory. The identification of admissible sets with the models of KP is what the theory exists for: it makes "closed under recursion" a first-order condition, so generalized recursion theory becomes model theory of a set theory. Barwise compactness is the payoff — infinitary logic is non-compact in general and compact over a countable admissible set, and the boundary is exactly admissibility. The proof-theoretic ordinal of KPω being the Bachmann–Howard ordinal places it below Π¹₁-CA₀ and far below ZF, so KP is a weak theory whose interest is entirely in the models it picks out rather than in what it proves.

Applies to. Generalized and higher recursion theory. Admissible sets and α-recursion. Infinitary logic and Barwise compactness. Ordinal analysis, where KPω and its extensions are the standard scale above arithmetic. Constructibility, since the L_α hierarchy is the paradigm family of models.

Limitations. No power set means no real analysis: ℝ is not a set in an admissible universe with only ω, and KP cannot do the mathematics ZF was built for. The theory is chosen for its models rather than for its axioms — nobody accepts KP as a foundation, and Δ₀-Collection is a technical restriction with no independent motivation beyond making admissibility first-order. And the name collides with Kreisel–Putnam logic, which is a fact about the literature and a recurring nuisance in it.

© 2026 Lingenic LLC