Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On sequential theorems in Reverse Mathematics

Dag Normann, Sam Sanders

Abstract

Many theorems of mathematics have the form that for a certain problem, e.g. a differential equation or polynomial (in)equality, there exists a solution. The sequential version then states that for a sequence of problems, there is a sequence of solutions. The original and sequential theorem can often be proved via the same (or similar) proof and often have the same (or similar) logical properties, esp. if everything is formulated in the language of second-order arithmetic. In this paper, we identify basic theorems of third-order arithmetic, e.g. concerning semi-continuous functions, such that the sequential versions have very different logical properties. In particular, depending on the constructive status of the original theorem, very different and independent choice principles are needed. Despite these differences, the associated Reverse Mathematics, working in Kohlenbach's higher-order framework, is rather elegant and is still based at the core on weak König's lemma.

On sequential theorems in Reverse Mathematics

Abstract

Many theorems of mathematics have the form that for a certain problem, e.g. a differential equation or polynomial (in)equality, there exists a solution. The sequential version then states that for a sequence of problems, there is a sequence of solutions. The original and sequential theorem can often be proved via the same (or similar) proof and often have the same (or similar) logical properties, esp. if everything is formulated in the language of second-order arithmetic. In this paper, we identify basic theorems of third-order arithmetic, e.g. concerning semi-continuous functions, such that the sequential versions have very different logical properties. In particular, depending on the constructive status of the original theorem, very different and independent choice principles are needed. Despite these differences, the associated Reverse Mathematics, working in Kohlenbach's higher-order framework, is rather elegant and is still based at the core on weak König's lemma.
Paper Structure (12 sections, 9 theorems, 21 equations)

This paper contains 12 sections, 9 theorems, 21 equations.

Table of Contents

  1. Introduction and preliminares
  2. Main results
  3. Introduction
  4. Preliminaries
  5. Some equivalences involving weak König's lemma
  6. Sequential theorems and weak König's lemma
  7. Sequential Cantor intersection theorem
  8. Sequential Heine-Borel theorem
  9. Variations
  10. Weak weak König's lemma
  11. Cousin's lemma
  12. The Lebesgue number lemma

Key Result

Theorem 2.5

Over $\textup{RCA}_{0}^{\omega}$, the following are equivalent: Over $\textup{RCA}_{0}^{\omega}+\textup{QF-AC}^{0,1}$, items itema-itemdz are equivalent to $\textup{WKL}_{0}$ and to The system ${\textsf{Z}}_{2}^{\omega}$ cannot prove items itema-itemf while ${\textsf{Z}}_{2}^{\Omega}$ proves items itema-iteme.

Theorems & Definitions (38)

  • Definition 2.1
  • Definition 2.2
  • Remark 2.3: Sequential theorems and the law of excluded middle
  • Theorem 2.5
  • proof
  • Theorem 2.7
  • proof
  • Theorem 2.8
  • proof
  • Theorem 2.9: $\textup{ACA}_{0}^{\omega}+\textup{ClC}$
  • ...and 28 more