On the logical structure of choice and bar induction principles

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$b R(a, b) $\Rightarrow$ $\exists$$\alpha$ $\forall$a R(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 Bool (for a constructive definition of prime filter), $\bullet$ the axiom of dependent choice if A = $\mathbb{N}$, $\bullet$ Weak K\"onig's Lemma if A = $\mathbb{N}$ and B = Bool (up to weak classical reasoning) - GBI(A,B,T) intuitionistically captures the strength of $\bullet$ G\"odel's completeness theorem in the form validity implies provability for entailment relations if B = Bool, $\bullet$ bar induction when A = $\mathbb{N}$, $\bullet$ the Weak Fan Theorem when A = $\mathbb{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^$\mathbb{N}$ and B is $\mathbb{N}$.