Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Games with backtracking options corresponding to the ordinal analysis of $PA$

Eitetsu Ken

Abstract

We give another proof of ordinal analysis of $IΣ_{k}$-fragments of Peano Arithmetic which is free from cut-elimination of $ω$-logic. Our main tool is a direct witnessing argument utilizing game notion, motivated from the realm of proof complexity and bounded arithmetic.

Games with backtracking options corresponding to the ordinal analysis of $PA$

Abstract

We give another proof of ordinal analysis of -fragments of Peano Arithmetic which is free from cut-elimination of -logic. Our main tool is a direct witnessing argument utilizing game notion, motivated from the realm of proof complexity and bounded arithmetic.

Paper Structure

This paper contains 11 sections, 12 theorems, 26 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. A game $\mathcal{G}_1(h)$ for $I\Sigma_1(X)$ v.s. $TI(\prec)$
  4. The game $\mathcal{G}_{1}$ and who wins
  5. Prover's winning strategy extracted from a proof
  6. A game $\mathcal{G}_k(h)$ for $I\Sigma_k(X)$ v.s. $TI(\prec)$
  7. The game $\mathcal{G}_{k}$ and who wins
  8. Prover's winning strategy extracted from a proof
  9. Acknowledgement
  10. Appendix
  11. The observation in Proposition \ref{['DelayerwinsG1']} is tight

Key Result

Lemma 3.4

Let $h \in \omega$. Suppose $(T',\rho')$ is a next position of $(T,\rho)$. Then $T' < T$.

Theorems & Definitions (56)

  • Definition 2.1
  • Remark 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Example 2.6
  • Example 2.7
  • Definition 2.8
  • Definition 2.9
  • Definition 2.10
  • ...and 46 more