Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Provably Total Set-Recursive Functions of KPl

Juan Pablo Aguilera, Anton Fernández, Joost J. Joosten

TL;DR

This work develops a relativized ordinal-analysis framework for Kripke-Platek set theories, notably $KPl$, $KPl^r$, and $W$-KPl, to classify provably total set-recursive-from-$\omega$ functions. It introduces a relativized ordinal notation system ${\sf RS}_l(X)$ built atop Veblen functions, collapsing functions, and a cut-elimination/collapsing machinery, and establishes an embedding of the theories into this infinitary system with explicit ordinal bounds. The main technical achievement is a uniform bound: any $f$ provably total from $\omega$-recursion in $KPl$ satisfies $f(x)\in L_{\psi_0(e_n)}(x)$ for some $n$, with $e_0=\Omega_\omega+1$ and $e_{m+1}=\omega^{e_m}$, and analogous bounds hold for $KPl^r$ and $W$-$KPl$ via $\hat G_n$ and $\check G_\alpha$. The results extend Cook-Rathjen-style analyses to weaker set theories, provide well-ordering proofs for the relativized notations, and yield optimality insights about the growth and necessity of the ordinal machinery in these classifications.

Abstract

Using relativized ordinal analysis, we give a proof-theoretic characterization of the provably total set-recursive-from-$ω$ functions of KPl and related theories.

The Provably Total Set-Recursive Functions of KPl

TL;DR

This work develops a relativized ordinal-analysis framework for Kripke-Platek set theories, notably , , and -KPl, to classify provably total set-recursive-from- functions. It introduces a relativized ordinal notation system built atop Veblen functions, collapsing functions, and a cut-elimination/collapsing machinery, and establishes an embedding of the theories into this infinitary system with explicit ordinal bounds. The main technical achievement is a uniform bound: any provably total from -recursion in satisfies for some , with and , and analogous bounds hold for and - via and . The results extend Cook-Rathjen-style analyses to weaker set theories, provide well-ordering proofs for the relativized notations, and yield optimality insights about the growth and necessity of the ordinal machinery in these classifications.

Abstract

Using relativized ordinal analysis, we give a proof-theoretic characterization of the provably total set-recursive-from- functions of KPl and related theories.
Paper Structure (26 sections, 63 theorems, 307 equations)

This paper contains 26 sections, 63 theorems, 307 equations.

Table of Contents

  1. Introduction
  2. Preliminaries on Set Theory
  3. Our Ordinal Notation System
  4. An overview on Veblen functions
  5. Our relativized ordinal notation system
  6. The infinitary proof system RSl(X)
  7. The terms and formulas of RSl(X)
  8. Operator-controlled derivations
  9. Cut-elimination for RSl(X)
  10. The rank of a formula
  11. Predicative results of RSl(X)
  12. The Collapsing Theorem
  13. Embedding KPl into RSl(X)
  14. The forces relation
  15. Embedding the axioms of KPl
  16. ...and 11 more sections

Key Result

Lemma 3.5

Let $\alpha_1,\alpha_2,\beta_1,\beta_2$ be ordinals. Then $$$\varphi\alpha_1\beta_1=\varphi\alpha_2\beta_2\Leftrightarrow $ Moreover, $\varphi\alpha_1\beta_1<\varphi\alpha_2\beta_2\Leftrightarrow $

Theorems & Definitions (177)

  • Definition 2.1: Formulas of the language $\mathcal{L'}$ of KPl
  • Definition 2.2: KPl-formulas
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • Definition 3.1: Constructible hierarchy relativized to $X$
  • Definition 3.3: Veblen functions
  • Definition 3.4
  • Lemma 3.5
  • ...and 167 more