Skip to Main content Skip to Navigation
Preprints, Working 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, UP - Université de Paris, 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 "effective" or "intensional" 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 ∀a ∃b R(a, b) ⇒ ∃α ∀a R(a, α(a))) when T is a filter that derives point-wise from a relation R on A × B without introducing further constraints, • the strength of the Boolean Prime Filter Theorem / Ultrafilter Theorem if B is the two-element set Bool, • the strength of the axiom of dependent choice if A = N, and up to weak classical reasoning • the (choice) strength of Weak König’s Lemma if A = N and B = Bool. - GBI(A,B,T) intuitionistically captures • the strength of Gödel’s completeness theorem in the form validity implies provability when B = Bool, • the strength of the Bar Induction when A = N, • the (choice) strength of the Weak Fan Theorem when A = N and B = Bool. 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 Bool^N and B is N.
Document type :
Preprints, Working Papers, ...
Complete list of metadata
Contributor : Hugo Herbelin <>
Submitted on : Monday, March 15, 2021 - 10:46:00 PM
Last modification on : Thursday, April 15, 2021 - 3:08:19 PM


Files produced by the author(s)


  • HAL Id : hal-03144849, version 2



Nuria Brede, Hugo Herbelin. On the logical structure of choice and bar induction principles. 2021. ⟨hal-03144849v2⟩



Record views


Files downloads