On the logical structure of choice and bar induction principles

TL;DR

This paper presents a unified extensional framework connecting various choice and bar induction principles, analyzing their logical relations and consistency within constructive and classical settings.

Contribution

It introduces generalized forms of the axiom of dependent choice and bar induction, linking them to classical principles through a unified extensional scheme.

Findings

GDC$_{A,B,T}$ captures multiple choice principles, including dependent choice and ultrafilter theorem.

GBI$_{A,B,T}$ captures bar induction, Gödel's completeness, and weak K{"o}nig's lemma.

Some instances of the generalized principles are inconsistent, highlighting limitations of the framework.

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\beta R(a, b) \Rightarrow\exists\alpha\forall a R(\alpha,(a \alpha (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{\"o}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{\"o}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}$.