Kripke–Platek set theory

Kripke–Platek set theory is a first-order axiomatic set theory that is weaker than Zermelo–Fraenkel set theory.^[1] 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ω^[2] 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 (lowercase 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 Lévy hierarchy 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 axioms^[3].

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ω⁰, 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,^[4]^[5]^{[footnote 1]}^[6]^{[footnote 2]} while those subsystems have smaller PTO.^[6]^{[footnote 2]} 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}\).^[6]^{[footnote 2]}

Axiom of Regularity

The full foundation implies axiom of regularity. Adding Regularity to KPω⁰ 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}\).^{[citation needed]}

Rudimentary set theory

Removing the Σ₀-collection axiom schema from KP yields a subsystem sometimes referred to as "rudimentary set theory"^[7].

Extensions

Compared with ZFC, KPω lacks axiom of power set and axiom of choice; separation and collection are also restricted on \(\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}\)^[8].

\(\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.^[9]

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.^[10]

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.^[11]

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}\).^[12]

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)\).^[13]

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 \(\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 ^[14]. 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

Main article: 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".^{[citation needed]} The lack of Foundation results and \(\Delta_0\)-induction along natural numbers is much weaker system, KPi⁰, with a PTO of Feferman–Schütte ordinal.^{[citation needed]}

Recursively Mahlo Ordinal

Main article: 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.^[15]

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.^[15] It has PTO \(\psi_\Omega(\varepsilon_{M+1})\) (in an ordinal collapsing function using a weakly Mahlo cardinal \(M\)), while the system without Foundation and with \(\Delta_0\)-induction along natural numbers, KPM⁰, 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.^[16]

Reflecting Ordinals

Main article: Reflecting ordinal

\(\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(\varepsilon_{K+1})\), in an ordinal notation using a weakly compact cardinal \(K\). And \(L_\alpha\models\text{KP}+\Pi_n\text{-Ref}\) iff \(\alpha\) is \(\Pi_n\)-reflecting.^{[citation needed]}

\(\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 Jean Carl Stegert's ordinal collapsing function using a \(\Pi_0^2\)-indescribable cardinal \(\Xi\).^[17] And \(L_\alpha\models\text{KP}+\Pi_\omega\text{-Ref}\) iff \(\alpha\) is \(\Pi_0^1\)-reflecting.

Stable ordinals

Main article: Stable ordinal

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 Jean Carl Stegert's ordinal notation using such \(\Upsilon\) 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)\).^[18]

Sources

↑ Kripke-Platek, Cantors Attic Wayback Machine.
↑ Christoph Duchhardt, Thinning Operators and \(\Pi_4\)-Reflection, Munster university doctral thesis, 2008.
↑ Domenico Zambella, "Foundation versus Induction in Kripke-Platek Set Theory", The Journal of Symbolic Logic, Vol. 63, No. 4 (Dec., 1998), pp. 1399-1403.
↑ 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.
↑ ^6.0 ^6.1 ^6.2 Michael Rathjen, "Fragments of Kripke–Platek Set Theory with Infinity" (a survey without a proof or a reference to the first source)
↑ P. Aczel, The Type Theoretic Interpretation of Constructive Set Theory (1978)
↑ D. Madore, (2017) A Zoo of Ordinals (p.6)
↑ Michael Rathjen, "Explicit Mathematics With The Monotone Fixed Point Principle. II: Models"
↑ David A. Madore, "A zoo of ordinals"
↑ Michael Rathjen, "The Higher Infinite in Proof Theory"
↑ Michael Rathjen, "Relativized ordinal analysis: The case of Power Kripke-Platek set theory"
↑ Michael Rathjen, "Power Kripke-Platek set theory and the axiom of choice"
↑ W. Pohlers. Subsystems of Set Theory and Second Order Number Theory, in Handbook of Proof Theory.
↑ ^15.0 ^15.1 Rathjen, Michael. "Proof-theoretic analysis of KPM", Archive for Mathematical Logic 30 (1991) 377--403.
↑ Michael Rathjen, Collapsing functions based on recursively large ordinals: A well–ordering proof for KPM. Archive for Mathematical Logic 33 (1994) 35–55.
↑ Jan-Carl Stegert, "Ordinal proof theory of Kripke-Platek set theory augmented by strong reflection principles"
↑ Jan-Carl Stegert, Ordinal Proof Theory of Kripke-Platek Set Theory Augmented by Strong Reflection Principles (2010) (p.141)

Footnotes

↑ 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.
↑ ^2.0 ^2.1 ^2.2 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.