On the logical structure of choice and bar induction principles

• Published in: arXiv.org 2022-07
• Main Authors: Brede, Nuria, Herbelin, Hugo
• Format: Article
• Language: English
• Subjects: Boolean algebra; Principles; Theorems
• ISSN: 2331-8422

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}\).