Kripke–Platek set theory

Kripke–Platek set theory is a first-order axiomatic set theory that is weaker than Zermelo–Fraenkel set theory.Kripke-Platek, Cantors Attic Wayback Machine. It uses the language of set theory, with infinitely many set variables, denoted by letters, and two set connectives \(=\), \(\in\).
==Axioms==
Under the name there are several axiomatic systems - a system without axiom of infinity (abbreviated KP or KP-), one with axiom of infinity (abbreviated KPωChristoph Duchhardt, Thinning Operators and \(\Pi_4\)-Reflection, Munster university doctral thesis, 2008. or KPI, but some authors use KP), one with axiom schema of \(\in\)-induction (some authors use KP) instead of axiom of foundation, one with axiom of \(\Pi_1\)-foundation instead of axiom of foundation (some authors use KP), and so on. Moreover, KPl (l = lowercase of L), which looks quite similar to KPI (uppercase I), means KP - (\(\Delta_0\)-Coll) asserting "there are unboundedly many admissible ordinals" for other authors, while it meant KP asserting "there are unboundedly many admissible ordinals" in this article.
Therefore one needs to be very careful when they refer to proof-theoretic statements on Kripke-Platek set theory without sources. Unfortunately, several "well-known" results on proof theory of Kripke-Platek set theory are unpublished, and hence many articles available on the internet lack sufficient sources. For example, this wiki included many wrong results based on the confounding of KPi (resp. KPM) with KP asserting the existence of a recursively inaccessible (resp. recursively Mahlo) ordinal, but those are two distinct axiomatic systems.
===Axiom of Extensionality===
\[\forall x\forall y(\forall z(z\in x\leftrightarrow z\in y)\rightarrow x=y)\]
Given sets \(x\), \(y\), if they have exactly the same elements, then they are equal.
===Axiom of Empty Set===
\[\exists x\forall y(y\notin x)\]
where \(y\notin x\) is shorthand for \(\neg y\in x\). There exists some set. In fact, there is a set which contains no members.
===Axiom of Pairing===
\[\forall x\forall y\exists z\forall w(w\in z\leftrightarrow(w=x\lor w=y))\]
Given sets \(x\), \(y\), there exists a set \(z=\{x,y\}\).
===Axiom of Union===
\[\forall x\exists y\forall z(z\in y\leftrightarrow\exists w(z\in w\land w\in x))\]
For every set \(x\), there exists a set \(y\) whose members are exactly all the members of the members of \(x\), denoted \(y=\bigcup x\) or \(y=\bigcup_{z\in x}z\).
===Axiom Schema of Foundation===
For every formula \(\phi(x,p_1,\cdots,p_n)\) or abbreviated \(\phi(x,\vec{p})\), the following is an instance of the axiom schema:
\[\forall\vec{p}(\exists x\phi(x,\vec{p})\rightarrow\exists x(\phi(x,\vec{p})\land\neg\exists y(y\in x\land\phi(y,\vec{p}))))\]
Suppose that a given property \(\phi\) is true for some set \(x\). Then there is a \(\in\)-minimal set for which \(\phi\) is true.
Some authors restrict the axiom shema to \(\Pi_1\)-formulae. On the other hand, some authors call the axiom schema of \(\in\)-induction "axiom schema of foundation".
===Axiom Schema of \(\Sigma_0\)-Separation===
A \(\Sigma_0\) formula is a formula in which every occurrence of quantifier is bounded, namely in the form \(\forall x\in y\phi\) (i.e. \(\forall x(x\in y\rightarrow\phi)\)) or \(\exists x\in y\phi\) (i.e. \(\exists x(x\in y\land\phi)\)). (See for \(\Sigma_n\), \(\Pi_n\) and \(\Delta_n\) formulas)
For every \(\Sigma_0\) formula \(\phi(x,\vec{p})\), the following is an instance of the axiom schema:
\[\forall\vec{p}\forall x\exists y\forall z(z\in y\leftrightarrow(z\in x\land\phi(z,\vec{p})))\]
Given a set \(x\), there exists a set \(y=\{z\in x|\phi(z,\vec{p})\}\).
===Axiom Schema of \(\Sigma_0\)-Collection===
For every \(\Sigma_0\) formula \(\phi(x,y,\vec{p})\), the following is an instance of the axiom schema:
\[\forall\vec{p}\forall a(\forall x\in a\exists y\phi(x,y,\vec{p})\rightarrow\exists b\forall x\in a\exists y\in b\phi(x,y,\vec{p}))\]
Given a set \(a\), if for all its member \(x\) there is some \(y\) such that \((x,y)\) satisfies a given \(\Sigma_0\)-property, then there exists a set \(b\) such that such \(y\) can be found in \(b\).
For example, let \(\phi(x,y,p_1,p_2)\) be a \(\Sigma_0\)-formalization of the property \(\{x,p_1,p_2\}\in y\). This asserts that for any sets \(p_1\) and \(p_2\), if a set \(a\) satisfies that for each \(x\in a\), there exists a set \(y\) such that \(\{x,p_1,p_2\}\in y\), then there must be a set \(b\) that for each \(x\in a\), there exists an element \(y \in b\) such that \(\{x,p_1,p_2\}\in y\).
===Axiom of Infinity===
\[\exists x(\varnothing\in x\land\forall y\in x(y\cup\{y\}\in x))\]
where \(\varnothing\in x\) is shorthand for \(\exists y\in x\forall z(\neg z\in y)\), and \(y\cup\{y\}\in x\) is shorthand for \(\exists z\in x\forall w(w\in z\leftrightarrow(w\in y\lor w=y))\). There exists a set containing infinitely many elements, and it follows from this axiom that the empty set exists.
Some authors use other formulations such as the following:
\[\exists x(\exists z(z\in x) \land(\forall y\in x\exists z\in x(y\in z)))\]
There exists a set containing a finite \(\in\)-chain of elements of any length, and it does not follow from this axiom that the empty set exists.
===Axiom Schema of \(\in\)-induction===
For every formula \(\phi(x)\), the following is an instance of the axiom schema:
\[\forall x(\forall(y\in x)(\phi(y))\rightarrow\phi(x))\rightarrow\forall x(\phi(x))\]
Suppose that a given property \(\phi\) is true for any set \(x\) such that \(\phi\) is true for any \(y\in x\). Then \(\phi\) is true for any set \(x\).
Open-induction, which is the axiom schema of \(\in\)-induction restricted to open formulae, follows from other axiomsDomenico Zambella, "Foundation versus Induction in Kripke-Platek Set Theory", The Journal of Symbolic Logic, Vol. 63, No. 4 (Dec., 1998), pp. 1399-1403..
==Subsystems==
Subsystems of KPω are derived by restricted axiom schema of foundation. Foundation on \(\Pi_n\) formulas (respectively, \(\Sigma_n\) formulas) \(\phi\) is denoted \(\Pi_n\)-Foundation (respectively, \(\Sigma_n\)-Foundation). The weakest system, denoted KPω0, is KPω without foundation and with \(\Delta_0\)-induction along natural numbers.
The proof-theoretic ordinal (abbreviated PTO) of KPω is the Bachmann-Howard ordinal,Jäger, Gerhard. Die konstruktible Hierarchie als Hilfsmittel zur beweistheoretischen Untersuchung von Teilsystemen der Mengenlehre und Analysis. na, 1979.Pohlers, Wolfram. Proof theory: The first step into impredicativity. Springer Science & Business Media, 2008.Ordinal analyses of set theory was first established by Jäger. Jäger defined proof-theoretic ordinal for set theory, and analysed \(\mathsf{KP}\omega\). This history is stated on the Pohlers' book cited above.Michael Rathjen, "Fragments of Kripke–Platek Set Theory with Infinity" (a survey without a proof or a reference to the first source)The reference is not the first source, and the corresponding descriptions in the reference does not include a reference to the first source. Therefore we need the first source. while those subsystems have smaller PTO. The PTO of \(\text{KP}\omega^0+\Sigma_1\text{-Foundation}\) is \(\varphi(\varphi(\omega,0),0)\). For \(n\ge 2\), the PTO of \(\text{KP}\omega^0+\Pi_n\text{-Foundation}\) is \(\psi_\Omega(\delta_n)\) where \(\delta_0=\omega\) and \(\delta_{i+1}=\Omega^{\delta_i}\).
===Axiom of Regularity===
The full foundation implies axiom of regularity. Adding Regularity to KPω0 results a stronger system, denoted KPωr.
===Induction on Natural Numbers===
The full foundation also implies the induction schema of natural numbers (denoted \(\textrm{IND}\)). For every \(\Sigma_n\) formula \(\phi(x)\), the following is an instance of the \(\Sigma_n\)-induction schema (denoted \(\Sigma_n\textrm{-IND}\)):
\[(\phi(0)\land\forall x\in\omega(\phi(x)\rightarrow\phi(x+1)))\rightarrow\forall x\in\omega\phi(x)\]
where \(\omega\) is the first limit ordinal. IND is then the conjunction of \(\Sigma_n\textrm{-IND}\) for all n.
With restricted foundation, \(\textrm{IND}\) improves PTO of the system. \(\text{KP}\omega^0+\Pi_1\text{-Foundation}+\Sigma_1\text{-IND}\) has a PTO of \(\varphi(\omega^\omega,0)\), \(\text{KP}\omega^0+\Pi_1\text{-Foundation}+\text{IND}\) has a PTO of \(\varphi(\varepsilon_0,0)\), and \(\text{KP}\omega^0+\Sigma_1\text{-Foundation}+\text{IND}\) has a PTO of \(\varphi(\varphi(\varepsilon_0,0),0)\). For \(n\ge2\), the PTO of \(\text{KP}\omega^0+\Pi_n\text{-Foundation}+\text{IND}\) is \(\psi_\Omega(\delta_n)\) where \(\delta_0=\varepsilon_0\) and \(\delta_{i+1}=\Omega^{\delta_i}\).
===Rudimentary set theory===
Removing the Σ0-collection axiom schema from KP yields a subsystem sometimes referred to as "rudimentary set theory"P. Aczel, The Type Theoretic Interpretation of Constructive Set Theory (1978).
==Extensions==
Compared with ZFC, KPω lacks axiom of power set and axiom of choice; separation and collection are also restricted to \(\Sigma_0\) formulas. So adding these axioms to KPω is an extension.
===Axiom Schema of Separation===
Let \(\Sigma_n\)-Sep (respectively, \(\Delta_n\)-Sep) denote the axiom schema of separation working on \(\Sigma_n\) formulas (respectively, \(\Delta_n\) formulas), and let \(\textrm{Sep}\) denote the schema \(\bigwedge_{i\in\omega}\Sigma_i\textrm{-Sep}\)D. Madore, (2017) A Zoo of Ordinals (p.6).
\(\text{KP}\omega^r+\text{IND}+\Sigma_1\text{-Sep}\) and \(\Pi^1_2\text{-CA}\) prove the same sentences of second-order arithmetic; \(\text{KP}\omega+\Sigma_1\text{-Sep}\) and \(\Pi^1_2\text{-CA}+\text{BI}\) also prove the same sentences of second-order arithmetic.Michael Rathjen, "Explicit Mathematics With The Monotone Fixed Point Principle. II: Models"
Let \(L\) denote the constructible hierarchy. The least ordinal \(\beta\) satisfying \(L_\beta\models\text{KP}\omega+\Sigma_1\text{-Sep}\) and \(L_\beta\cap\mathcal P(\omega)\models\Pi^1_2\text{-CA}+\text{BI}\) are equal; the least \(\beta\) for \(L_\beta\models\text{KP}\omega+\Delta_2\text{-Sep}\) and \(L_\beta\cap\mathcal P(\omega)\models\Delta^1_3\text{-CA}\) are equal; the least \(\beta\) for \(L_\beta\models\text{KP}\omega+\text{Sep}\), \(L_\beta\models\)ZFC without axiom of power set, and \(L_\beta\cap\mathcal P(\omega)\models \text{Z}_2\) are also equal.David A. Madore, "A zoo of ordinals"
===Axiom Schema of Collection===
Let \(\Sigma_n\)-Coll denote the axiom schema of collection working on \(\Sigma_n\) formulas.
For \(n>0\), \(\text{KP}\omega+\Sigma_n\text{-Sep}+\Sigma_n\text{-Coll}\) and \(\Pi^1_{n+1}\text{-CA}+\Sigma^1_{n+1}\text{-AC}+\text{BI}\) prove the same sentences of second-order arithmetic.Michael Rathjen, "The Higher Infinite in Proof Theory"
===Axiom of Power Set===
KPω with axiom of power set (denoted Pow) is strong enough to dwarf the strength of second-order arithmetic, but it can't prove the existence of \(V_{\omega2}\).Michael Rathjen, "Relativized ordinal analysis: The case of Power Kripke-Platek set theory"
Power Kripke–Platek set theory, denoted \(\text{KP}(\mathcal P)\), is \(\text{KP}\omega+\text{Pow}+\Delta^{\mathcal P}_0\text{-Sep}+\Delta^{\mathcal P}_0\text{-Coll}\), where \(\Delta^{\mathcal P}_0\)-Sep (respectively, \(\Delta^{\mathcal P}_0\)-Coll) is the axiom schema of separation (respectively, axiom schema of collection) only applied on \(\Delta^{\mathcal P}_0\) formulas. A \(\Delta^{\mathcal P}_0\) formula is a formula in which every occurrence of quantifier is in the form \(\forall x\in y\phi\), \(\exists x\in y\phi\), \(\forall x\subseteq y\phi\) (i.e. \(\forall x(\forall z(z\in x\rightarrow z\in y)\rightarrow\phi)\)) or \(\exists x\subseteq y\phi\) (i.e. \(\exists x(\forall z(z\in x\rightarrow z\in y)\land\phi)\)).
\(\text{KP}(\mathcal P)\) enable separation and collection on \(\Delta^{\mathcal P}_0\) properties, and it is much stronger than KPω + Pow. The least ordinal \(\alpha\) for "\(V_\alpha\) is a \(\Pi^{\mathcal P}_2\) model of \(\text{KP}(\mathcal P)\)" is the Bachmann-Howard ordinal.
===Axiom of Choice===
\(\text{KP}(\mathcal P)\) with axiom of choice (denoted AC), however, still have equal PTO to \(\text{KP}(\mathcal P)\).Michael Rathjen, "Power Kripke-Platek set theory and the axiom of choice"
==Large Ordinal Axioms==
Large ordinal axioms on KP usually use definitions in model theory. The first large ordinals are usually countable, and KP with these axioms is weaker than KPω + Pow.
===Admissible Ordinals===
A set \(A\) is admissible if it is a transitive model of KP, denoted \(A\models\text{KP}\). Ordinal \(\alpha\) is called an admissible ordinal if \(L_\alpha\) is an admissible set.
Some authors use another formulation of the admissibility characterised by the following axioms:
# If \(A\) is admissible, then \(A\) is a transitive model of the axioms of pair, union, \(\Delta_0\)-separation, \(\Delta_0\)-collection, and infinity.
# If \(A\) and \(B\) are admissible, then either one of \(A \in B\), \(A = B\), or \(B \in A\) holds.
The least admissible ordinal is oftenChristoph Duchhardt, Thinning Operators and \(\Pi_4\)-Reflection, Munster university doctral thesis, 2008. Accessed 2021-04-16. \(\omega\), followed by \(\omega^\text{CK}_1\). The ordinal \(\omega^\text{CK}_{\alpha+1}\) is defined to be next admissible after \(\omega^\text{CK}_\alpha\), and \(\omega^\text{CK}_\alpha=\sup\{\omega^\text{CK}_\beta|\beta<\alpha\}\) for a limit ordinal \(\alpha\). \(\omega^\text{CK}_\omega\), the first limit of admissible ordinals, is not admissible.
This community believed that KPl is KP asserting "the universe is a limit of admissible sets", with a PTO of Takeuti-Feferman-Buchholz ordinal without sources, but it is wrong. Usually, KPl is defined by BST asserting "the universe is a limit of admissible sets" where BST is KP\(\omega\) without \(\Delta_0\)-collection. A PTO of BST asserting "the universe is a limit of admissible sets" is Takeuti-Feferman-Buchholz ordinal W. Pohlers. 
 Subsystems of Set Theory and Second Order Number Theory, in Handbook of Proof Theory.. KP asserting "the universe is a limit of admissible sets" is known as KPi and its PTO is \(\psi_\Omega(\varepsilon_{I+1})\), where \(\psi\) is Jäger–Buchholz's ψ function.
===Recursively Inaccessible Ordinal===
Although this community believed that KPi is KP asserting the existence of a recursively inaccessible ordinal without sources, it is wrong. We have "\(L_\alpha\models\text{KPi}\) iff ordinal \(\alpha\) is recursively inaccessible". The lack of Foundation results and \(\Delta_0\)-induction along natural numbers is much weaker system, KPi0, with a PTO of Feferman–Schütte ordinal.
===Recursively Mahlo Ordinal===
Although this community referred to KPM as KP asserting "there exists a recursively Mahlo ordinal" or "the universe is recursively Mahlo" without sources, it is wrong. The precise definition of KPM by Rathjen is given as KP asserting "the universe is a limit of sets \(x\) satisfying \(\textrm{Ad}(x)\)" and the schema "if every \(x\) admits some \(y\) satisfying \(H(x,y)\), then there exists some \(z\) satisfying \(\textrm{Ad}(z)\) such that every \(x \in z\) admits some \(y \in z\) satisfying \(H(x,y)\)" for all \(\Delta_0\)-formulae \(H(a,b)\), which appropriately formalises the recursive Mahloness of the universe. Here, \(\textrm{Ad}\) is the predicate defined by the Ad-axiom given as the transitivity, the admissibility, the relativisation of the axiom of infinity, and the trichotomy.Rathjen, Michael. "Proof-theoretic analysis of KPM", Archive for Mathematical Logic 30 (1991) 377--403.
Since it is not convenient to formulate KPM in the way above for the purpose of ordinal analysis, some authors use another formulation given by derivation system with cut-elimination. It has PTO \(\psi_\Omega(\varepsilon_{M+1})\) in Buchholz's ordinal collapsing function using a weakly Mahlo cardinal \(M\)Buchholz, Wilfried. "A note on the ordinal analysis of KPM", while the system without Foundation and with \(\Delta_0\)-induction along natural numbers, KPM0, has PTO \(\varphi(\omega,0,0)\). The proof of the claim on PTO of KPM seems unpublished, but at least, a deeply related comparison to \(\psi_\Omega(\psi_{\chi_{\varepsilon_{M+1}}(0)}(0))\) is published.Michael Rathjen, Collapsing functions based on recursively large ordinals: A well–ordering proof for KPM. Archive for Mathematical Logic 33 (1994) 35–55.
===Reflecting Ordinals===
\(\text{KP}+\Pi_n\text{-Ref}\) is KP with the axiom schema for all \(\Pi_n\) formulas \(\phi(\vec{p})\): \(\forall\vec{p}(\phi(\vec{p})\rightarrow\exists x(x\models\phi(\vec{p})))\). \(\text{KP}+\Pi_3\text{-Ref}\) has PTO \(\Psi_\Omega^0(\varepsilon_{K+1})\), in Rathjen's \(\Psi\). And \(L_\alpha\models\text{KP}+\Pi_n\text{-Ref}\) iff \(\alpha\) is \(\Pi_n\)-reflecting.
\(\text{KP}+\Pi_\omega\text{-Ref}\) is KP with the axiom schema for all first-order formulas \(\phi(\vec{p})\): \(\forall\vec{p}(\phi(\vec{p})\rightarrow\exists x(x\models\phi(\vec{p})))\). It has PTO \(\Psi_{\mathbb X}^{\varepsilon_{\Xi+1}}\) where \(\mathbb X=(\omega^+;\text{P}_0;\epsilon;\epsilon;0)\), in Jan-Carl Stegert's ordinal collapsing function using a \(\Pi_0^2\)-indescribable cardinal \(\Xi\).Jan-Carl Stegert, "Ordinal proof theory of Kripke-Platek set theory augmented by strong reflection principles" And \(L_\alpha\models\text{KP}+\Pi_\omega\text{-Ref}\) iff \(\alpha\) is \(\Pi_0^1\)-reflecting.
===Stable ordinals===
The set theory Stability is KPi with the axiom \(\forall\alpha\exists\beta(\alpha\le\beta\land L_\beta\prec_{\Sigma_1}L_{\beta+\alpha})\). The ordinal \(\vert\textsf{Stability}\vert_{\Sigma_1^{\omega_1^{CK}}}\) related to this system is less than or equal to \(\Psi_{\mathbb X}^{\varepsilon_{\Upsilon+1}}\) where \(\mathbb X=(\omega^+;\text{P}_0;\epsilon;\epsilon;0)\), in Jan-Carl Stegert's ordinal notation using an \(\Upsilon\) so that \(\forall\alpha<\Upsilon\exists\kappa<\Upsilon(\kappa\text{ is }\alpha\text{-indescribable})\land\forall\alpha<\Upsilon\forall\kappa<\Upsilon(\kappa\text{ is }\alpha\text{-indescribable}\rightarrow\alpha<\kappa)\).Jan-Carl Stegert, Ordinal Proof Theory of Kripke-Platek Set Theory Augmented by Strong Reflection Principles (2010) (p.141)
==Sources==
==Footnotes==
==See also==
ja:KP集合論
Category:Set theory