On the logical structure of choice and bar induction principles
share
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 ∀ a∃ b R(a, b) ⇒∃α∀α R(α,α(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 𝔹 (for a constructive definition of prime filter), ∙ the axiom of dependent choice if A = ℕ, ∙ Weak König's Lemma if A = ℕ and 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 = 𝔹, ∙ bar induction when A = ℕ, ∙ the Weak Fan Theorem when A = ℕ and 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 𝔹^ℕ and B is ℕ.
READ FULL TEXT