On the logical structure of choice and bar induction principles
Nuria Brede, Hugo Herbelin · 2021
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 GDCABT of the axiom of dependent choice and dually a generalised bar induction principle GBIABT such that:GDCABTintuitionistically captures the strength of·the general axiom of choice expressed as ∀a∃bR(a,b) ⇒ ∃α∀aR(a,α(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 \mathbbB (for a constructive definition of prime filter),·the axiom of dependent choice if A = \mathbbN,·Weak Knig's Lemma if A = \mathbbN and B = \mathbbB (up to weak classical reasoning).GBIABTintuitionistically captures the strength ofGödel's completeness theorem in the form validity implies provability for entailment relations if B = \mathbbB (for a constructive definition of validity),·bar induction if A = \mathbbN,·the Weak Fan Theorem if A = \mathbbN and B = \mathbbB.Contrastingly, even though GDCABT and GBIABTsmoothly capture several variants of choice and bar induction, some instances are inconsistent, e.g. when A is \mathbbB\mathbbNand B is \mathbbN.