Skip to Main content Skip to Navigation
Conference papers

On the logical structure of choice and bar induction principles

Nuria Brede 1 Hugo Herbelin 2 
2 PI.R2 - Design, study and implementation of languages for proofs and programs
CNRS - Centre National de la Recherche Scientifique, Inria de Paris, UPC - Université Paris Cité, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
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 • 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 × B$ without introducing further constraints, • the Boolean Prime Filter Theorem / Ultrafilter Theorem if $B$ is the two-element set $\mathbb{B}$ (for a constructive definition of prime filter), • the axiom of dependent choice if $A = \mathbb{N}$, • 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 • Gödel’s completeness theorem in the form validity implies provability for entailment relations if $B = \mathbb{B}$, • bar induction when $A = \mathbb{N}$, • 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}$.
Complete list of metadata
Contributor : Hugo Herbelin Connect in order to contact the contributor
Submitted on : Friday, June 18, 2021 - 8:25:00 PM
Last modification on : Wednesday, June 8, 2022 - 12:50:08 PM


lics (2).pdf
Files produced by the author(s)


  • HAL Id : hal-03144849, version 4
  • ARXIV : 2105.08951



Nuria Brede, Hugo Herbelin. On the logical structure of choice and bar induction principles. LICS 2021 - 36th Annual Symposium on Logic in Computer Science, Jun 2021, Rome / Virtual, Italy. ⟨hal-03144849v4⟩



Record views


Files downloads