On the logical structure of choice and bar induction principles

TL;DR

The paper develops an extensionality-based framework that unifies choice principles and bar induction by linking intensional notions of ill-foundedness and well-foundedness to extensional, filter-driven views. It introduces generalized schemes $GDC_{A,B,T}$ and $GBI_{A,B,T}$ that, under suitable choices of the domain $A$, codomain $B$, and finite-approximation filter $T$, capture classical results such as the Axiom of Choice, the Boolean Prime/Ultrafilter Theorem, Dependent Choice, Weak König's Lemma, Bar Induction, and the Weak Fan Theorem, while also exposing inconsistencies in some broad generalizations. The work establishes a unifying perspective in which ill-founded variants generalize DC/BPF and well-founded variants generalize BI/WFT, with BPF emerging as an instance of generalized DC; it also extends to non-sequential, non-countable branching, connecting to Scott entailment relations and Boolean-algebra formulations. Overall, the paper provides a comprehensive taxonomy and a set of equivalences that illuminate the delicate balance between constructive and classical reasoning in foundational choice principles.

Abstract

We develop an approach to choice principles and their contrapositive bar-induction principles as extensionality schemes connecting an ''intensional'' or ''effective'' view of respectively ill-and well-foundedness properties to an ''extensional'' or ''ideal'' view of these properties. After classifying and analysing the relations between different intensional definitions of ill-foundedness and well-foundedness, we introduce, for a domain $A$, a codomain $B$ and a ''filter'' $T$ on finite approximations of functions from $A$ to $B$, a generalised form GDC$_{A,B,T}$ of the axiom of dependent choice and dually a generalised bar induction principle GBI$_{A,B,T}$ such that: - GDC$_{A,B,T}$ intuitionistically captures the strength of $\bullet$ the general axiom of choice expressed as $\forall a\existsβR(a, b) \Rightarrow\existsα\forall a R(α,(a α(a)))$ when $T$ is a filter that derives point-wise from a relation $R$ on $A x B$ without introducing further constraints, $\bullet$ the Boolean Prime Filter Theorem / Ultrafilter Theorem if $B$ is the two-element set $\mathbb{B}$ (for a constructive definition of prime filter), $\bullet$ the axiom of dependent choice if $A = \mathbb{N}$, $\bullet$ Weak K{ö}nig's Lemma if $A = \mathbb{N}$ and $B = \mathbb{B}$ (up to weak classical reasoning) - GBI$_{A,B,T}$ intuitionistically captures the strength of $\bullet$ G{ö}del's completeness theorem in the form validity implies provability for entailment relations if $B = \mathbb{B}$, $\bullet$ bar induction when $A = \mathbb{N}$, $\bullet$ the Weak Fan Theorem when $A = \mathbb{N}$ and $B = \mathbb{B}$. Contrastingly, even though GDC$_{A,B,T}$ and GBI$_{A,B,T}$ smoothly capture several variants of choice and bar induction, some instances are inconsistent, e.g. when $A$ is $\mathbb{B}^\mathbb{N}$ and $B$ is $\mathbb{N}$.