The Strength of an Axiom of Finite Choice for Branches in Trees

Journal of Symbolic Logic 88 (4):1367-1386 (2023)
  Copy   BIBTEX

Abstract

In their logical analysis of theorems about disjoint rays in graphs, Barnes, Shore, and the author (hereafter BGS) introduced a weak choice scheme in second-order arithmetic, called the $\Sigma ^1_1$ axiom of finite choice (hereafter finite choice). This is a special case of the $\Sigma ^1_1$ axiom of choice ( $\Sigma ^1_1\text {-}\mathsf {AC}_0$ ) introduced by Kreisel. BGS showed that $\Sigma ^1_1\text {-}\mathsf {AC}_0$ suffices for proving many of the aforementioned theorems in graph theory. While it is not known if these implications reverse, BGS also showed that those theorems imply finite choice (in some cases, with additional induction assumptions). This motivated us to study the proof-theoretic strength of finite choice. Using a variant of Steel forcing with tagged trees, we show that finite choice is not provable from the $\Delta ^1_1$ -comprehension scheme (even over $\omega $ -models). We also show that finite choice is a consequence of the arithmetic Bolzano–Weierstrass theorem (introduced by Friedman and studied by Conidis), assuming $\Sigma ^1_1$ -induction. Our results were used by BGS to show that several theorems in graph theory cannot be proved using $\Delta ^1_1$ -comprehension. Our results also strengthen results of Conidis.

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 103,401

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2023-12-19

Downloads
25 (#921,682)

6 months
7 (#469,699)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Indecomposable linear orderings and hyperarithmetic analysis.Antonio Montalbán - 2006 - Journal of Mathematical Logic 6 (1):89-120.
Necessary use of [image] induction in a reversal.Itay Neeman - 2011 - Journal of Symbolic Logic 76 (2):561 - 574.
On the Π1 1 -separation principle.Antonio Montalbán - 2008 - Mathematical Logic Quarterly 54 (6):563-578.
The strength of Jullien's indecomposability theorem.Itay Neeman - 2008 - Journal of Mathematical Logic 8 (1):93-119.
Forcing with tagged trees.John R. Steel - 1978 - Annals of Mathematical Logic 15 (1):55.

Add more references