# On the logical structure of choice and bar induction principles

Nuria Brede, Hugo Herbelin

► To cite this version:

Nuria Brede, Hugo Herbelin. On the logical structure of choice and bar induction principles. LICS 2021 - 36th Annual Symposium on Logic in Computer Science, Jun 2021, Rome / Virtual, Italy. hal-03144849v5

HAL Id: hal-03144849

https://inria.hal.science/hal-03144849v5

Submitted on 5 Jul 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
# On the logical structure of choice and bar induction principles

(includes errata – July 2022)

Nuria Brede

University of Potsdam, Germany

Hugo Herbelin

Inria Paris, Université de Paris, CNRS, IRIF, France

## Abstract—

We develop an approach to choice principles and their contra-positive 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_{ABT}$ of the axiom of dependent choice and dually a generalised bar induction principle $GBI_{ABT}$ such that:

$GDC_{ABT}$ intuitionistically captures the strength of

* 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 × B without introducing further constraints,

* the Boolean Prime Filter Theorem / Ultrafilter Theorem if B is the two-element set $\mathbb{B}$ (for a constructive definition of prime filter),

* the axiom of dependent choice if $A = \mathbb{N}$,

* Weak König's Lemma if $A = \mathbb{N}$ and $B = \mathbb{B}$ (up to weak classical reasoning).

$GBI_{ABT}$ intuitionistically captures the strength of

* Gödel's completeness theorem in the form validity implies provability for entailment relations if $B = \mathbb{B}$ (for a constructive definition of validity),

* bar induction if $A = \mathbb{N}$,

* the Weak Fan Theorem if $A = \mathbb{N}$ and $B = \mathbb{B}$.

Contrastingly, even though $GDC_{ABT}$ and $GBI_{ABT}$ smoothly capture several variants of choice and bar induction, some instances are inconsistent, e.g. when A is $\mathbb{B}^N$ and B is $\mathbb{N}$.

## I. INTRODUCTION

### A. Bar induction, dependent choice and their variants as extensionality principles

For a domain A, there are different ways to define a well-founded tree branching over A. A first possibility is to define it as an inductive object built from leaves and from nodes associating a subtree to each element in A. We will call this definition *intensional*. Using a syntax familiar to functional programming languages or Martin-Löf-style type theory, such intensional trees correspond to inhabitants of an inductive type:

type tree = Leaf | Node of (A → tree)

A second possibility is a definition which we shall call extensional and which is probably more standard in the context of non type-theoretic mathematics. Let $A^*$ denote the set of finite sequences of elements of A, with $\langle\rangle$ denoting the empty sequence and $u \star a$ the extension of the sequence u with a from A. Then an extensional tree T is a downwards-closed predicate over $A^*$. Finite sequences $u \in A^*$ are interpreted as finite paths from the root of a tree and the predicate determines which paths are contained in T. We say that T is extensionally well-founded if for all infinite paths $\alpha$ in $A^N$, the path eventually “leaves” the tree, i.e. there is an initial finite prefix u of $\alpha$ such that u (as path from the root) is not contained in T.

The intensional definition is stronger: to any inductively-defined tree t, we can associate an extensionally well-founded tree $T(t)$ by recursion on t as follows:

$$ 
\begin{align*}
u \in T(\text{Leaf}) &\triangleq \perp \\
u \in T(\text{Node}(f)) &\triangleq \bigvee u = \langle\rangle \\
& \phantom{\triangleq} \exists a \exists u' (u = a@u' \land u' \in T(f(a)))
\end{align*}
$$

where $a@u$, a particular case of concatenation $u'@u$, prefixes $u$ with $a$. We can then prove by induction on $t$ that $\forall \alpha \exists n \neg T(t)(\alpha|_n)$, where $\alpha|_n$ is the restriction of $\alpha$ to its first $n$ values.

To reflect that $T(t)$ is related to $t$, we can define a realisability relation between $t$ and $T$ as follows:

* Leaf realises $T$ if $\langle\rangle \notin T$

* Node($f$) realises $T$ if $\langle\rangle \in T$ and for all $a$, $f(a)$ realises $\lambda u.(a@u \in T)$

Then, we can prove by induction on $t$ that $t$ realises $T(t)$.

Bar induction, introduced by Brouwer and further analysed e.g. by Kleene and Vesley [21] can be seen as the converse property, namely that any extensionally well-founded $T$ can be turned into an inductively-defined tree $t$ that realises $T$, so that, at the end, the intensional and extensional definitions of well-foundedness are equivalent<fnref n="1" />.

At its core, bar induction is the statement “U barred implies U inductively barred” for U a predicate on $A^*$. As studied e.g. in Howard and Kreisel [16], when used on a negated predicate $\neg T$, this reduces to “T extensionally well-founded implies T inductively well-founded”, where $T$ inductively well-founded abbreviates “T inductively well-founded at $\langle\rangle$”, where $T$ inductively well-founded at $u$ is itself defined by the following clauses:

* if $u \notin T$ then $T$ is inductively well-founded at $u$

* if, for all $a$, $T$ is inductively well-founded at $u \star a$, then $T$ is inductively well-founded at $u$

<footnote n="1">¹Kleene and Vesley [21] used respectively the terms “inductive” and “explicit” for what we call intensional and extensional.</footnote>
Then, it can be proved that *T* inductively well-founded at *u* is itself not different from the existence of an intensional tree *t* (hidden in the structure of any proof of inductive well-foundedness) such that *t* realises $\lambda u'.T(u@u')$. This justifies our claim that bar induction is at the end a way to produce an intensionally well-founded tree from an extensionally well-founded one.

Now, if bar induction can be considered as an extensionality principle, it should be the same for its contrapositive which is logically equivalent to the *axiom of dependent choice*. This means that it should eventually be possible to rephrase the axiom of dependent choice as a principle asserting that, if a tree is *coinductively ill-founded*, then it is *extensionally ill-founded* (i.e. an infinite branch can be found). We will investigate this direction in Section II, together with precise relations between these principles and their restriction on finitely-branching trees, namely *Kőnig's Lemma*<fnref n="2" /> and the *Fan Theorem*, introducing a systematic terminology to characterise and compare these different variants.

Note in passing that the approach to consider bar induction and choice principles as extensional principles is consistent with the methodology developed e.g. by Coquand and Lombardi: to avoid the necessity of choice or bar induction axioms, mathematical theorems are restated using the (co-)inductively-defined notions of well- and ill-foundedness rather than the extensional notions [9], [10].

## B. Weak Kőnig's Lemma at the intersection of Boolean Prime Filter Theorem and Dependent Choice

We know from classical reverse mathematics of the subsystems of second order arithmetic [29] that the binary form of Kőnig's lemma, namely *Weak Kőnig's Lemma* (WKL) has the strength of *Gödel's completeness theorem* (for a countable language). Classical reverse mathematics of the axiom of choice and its variants in set theory [14], [27], [20], [11] also tells that Gödel's completeness theorem has the strength of the *Boolean Prime Filter Theorem* (for a language of arbitrary cardinal). This suggests that the Boolean Prime Filter Theorem is the “natural” generalisation of WKL from countable to arbitrary cardinals.

On the other side, Weak Kőnig's Lemma is a consequence<fnref n="3" /> of the axiom of Dependent Choice, the same way as its contrapositive, the Weak Fan Theorem, is an instance of Bar Induction, itself related to the contrapositive of the axiom of Dependent Choice. This suggests that there is common principle which subsumes both the Axiom of Dependent Choice and the Boolean Prime Filter Theorem with Weak Kőnig's Lemma at their intersection.

Such a principle is stated in Section III where it is shown that the ill-founded version indeed generalises the axiom of Dependent Choice and the well-founded version generalises Bar Induction. In the same section, we also show that one of the instance of the ill-founded version captures the general Axiom

<table><caption>TABLE I
SUMMARY OF LOGICAL CORRESPONDENCES</caption><thead><tr><th>ref.</th><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td></td><td colspan="2" style="text-align: center;">T branching from $\mathbb{N}$ over arbitrary B</td></tr><tr><td>Th. 5</td><td>GDC<sub>NBT</sub> = DC<sup>productive</sup><sub>BT</sub></td><td>GBI<sub>NBT</sub> = BI<sup>ind</sup><sub>BT</sub></td></tr><tr><td>Th. 1</td><td>= DC<sup>spread</sup><sub>BT</sub></td><td>= BI<sup>barricaded</sup><sub>BT</sub></td></tr><tr><td>Th. 3</td><td>= DC<sup>serial</sup><sub>BRb<sub>0</sub></sub></td><td></td></tr><tr><td></td><td colspan="2" style="text-align: center;">T branching from $\mathbb{N}$ over non-empty finite B</td></tr><tr><td>Th. 6</td><td>GDC<sub>NBT</sub> = KL<sup>productive</sup><sub>BT</sub></td><td>GBI<sub>NBT</sub> = FT<sup>ind</sup><sub>BT</sub></td></tr><tr><td></td><td>= KL<sup>spread</sup><sub>BT</sub></td><td>= FT<sup>barricaded</sup><sub>BT</sub></td></tr><tr><td></td><td>= co-intuit. KL<sup>unbounded</sup><sub>BT</sub></td><td>= co-intuit. FT<sup>uniform</sup><sub>BT</sub></td></tr><tr><td></td><td>= co-intuit. KL<sup>staged</sup><sub>BT</sub></td><td>= co-intuit. FT<sup>staged</sup><sub>BT</sub></td></tr><tr><td></td><td colspan="2" style="text-align: center;">functions from $\mathbb{N}$ to arbitrary B</td></tr><tr><td>Th. 4</td><td>GDC<sub>NBR<sub>T</sub></sub> = CC<sub>BR</sub></td><td></td></tr><tr><td></td><td colspan="2" style="text-align: center;">functions from arbitrary A to arbitrary B</td></tr><tr><td>Th. 7</td><td>GDC<sub>ABR<sub>T</sub></sub> = AC<sub>ABR</sub></td><td></td></tr><tr><td></td><td colspan="2" style="text-align: center;">binary branching from arbitrary A</td></tr><tr><td>Th. 8</td><td>GDC<sub>A<sup>B</sup>T<sup>C</sup></sub> = Compl<sup>-</sup><sub>A</sub>(T)</td><td>GBI<sub>A<sup>B</sup>T</sub> = Compl<sup>+</sup><sub>A</sub>(T)</td></tr><tr><td>Th. 9</td><td>GDC<sub>A<sup>B</sup>T<sup>C</sup></sub> = BPF<sub>Free(A)</sub>(F<sub>T</sub>)</td><td></td></tr></tbody></table>

of Choice, but that, in its full generality, the new principle is actually inconsistent.

Section IV is devoted to show that the Boolean Prime Filter Theorem is an instance of the generalised axiom of Dependent Choice. In particular, this highlights that the notions of *ideal* and *filter* generalise the notion of a binary tree where the prefix order between paths of the tree is replaced by an inclusion order between non-sequentially-ordered paths now seen as finite approximations of a function from $\mathbb{N}$ to the two-element set $\mathbb{B}$.

## C. Methodology and summary

For our investigations to apply both to classical and to intuitionistic mathematics, we carefully distinguish between the choice axioms (seen as ill-foundedness extensionality schemes) and bar induction schemes (seen as well-foundedness extensionality schemes).

All in all, the correspondences we obtain are summarised in Table I where the definitions of the different notions can be found in the respective sections of the paper.

# II. THE LOGICAL STRUCTURE OF DEPENDENT CHOICE AND BAR INDUCTION PRINCIPLES

## A. Metatheory

We place ourselves in a metatheory capable to express arithmetic statements. In addition to the type $\mathbb{N}$ of natural numbers together with induction and recursion, we assume the following constructions to be available:

* The type $\mathbb{B}$ of Boolean values 0 and 1 together with a mechanism of definition by case analysis. It shall be

<footnote n="2">²The spelling König's Lemma is also common. We respect here the original Hungarian spelling of the author's name.</footnote>

<footnote n="3">³Note that Kőnig's Lemma is a theorem of set theory and that we need to place ourselves in a sufficiently weak metatheory, e.g. $RCA_0$, to state this result.</footnote>
convenient to allow the definition of propositions by case analysis as in if b then P else Q, whose logical meaning shall be equivalent to (b = 1 ∧ P) ∨ (b = 0 ∧ Q).

* For any type A, the type $A^*$ of finite sequences over A whose elements shall generally be ranged over by the letters u, v ... We write $\langle\rangle$ for the empty sequence and $u \star a$ for the extension of sequence u with element a. We write $|u|$ for the length of u and $u(n)$ for the n-th element of u when $n < |u|$. We write $v@u$ for the concatenation of v and u. We write $u \leq_s v$ to mean that u is an initial prefix of v. This is inductively defined by:

$$ \frac{u \leq_s v}{u \leq u} \frac{u \leq_s v \star a}{u \leq s} $$

We shall also support case analysis over finite sequences under the form of a case operator.

* For any two types A and B, the type $A \to B$ of functions from A to B. Functions can be built by λ-abstraction as in λx.t for x in A and t in B and used by application as in t(u) for t in A → B and u in A. To get closer to the traditional notations, we shall also abbreviate $t(u_1) \dots (u_n)$ into $t(u_1, \dots, u_n)$.

* A type Prop reifying the propositions as a type. The type $A \to \text{Prop}$ shall then represent the type of predicates over A. We shall allow predicates to be defined inductively (smallest fixpoint) or coinductively (greatest fixpoint), using respectively the μ and ν notations.

* For any type A and predicate P over A, the subset $\{a : A \mid P(a)\}$ of elements of A satisfying P.

This is a language for higher-order arithmetic but in practice, we shall need quantification just over functions and predicates of (apparent) rank 1 (i.e. of the form $A_1 \to \dots \to A_n \to A$ or $A_1 \to \dots \to A_n \to \text{Prop}$ with no arrow types in A and the $A_i$). We however also allow arbitrary type constants to occur, so we can think of our effective metatheory as a second-order arithmetic generic over arbitrary more complex types. In practise, our metatheory could typically be the image of arithmetic in set theory or in an impredicative type theory. We will in any case use the notation $a \in A$ to mean that a has type A when A is a type, which, if in set theory, will become a belongs to the set A.

The metatheory can be thought as classical, i.e. associated to a classical reading of connectives but in practice, unless stated otherwise, most statements will have proofs compatible with a linear, intuitionistic or co-intuitionistic reading of connectives too. Using linear logic as a reference for the semantics of connectives [13], $A \Rightarrow B$, $\forall a Q$, $A \lor B$, $\exists a Q$, $\neg A$ have respectively to be read linearly as $P \dashv Q$, $\&_a Q$, $A \oplus B$, $\oplus_a Q$ and the logical dual $A^\perp$ of A, while $A \land B$ has to be read $A \otimes B$ when used as the dual of $A \Rightarrow B^\perp$ and $A \& B$ when used as the dual of $A^\perp \lor B^\perp$. An intuitionistic reading will add a “!” (of-course connective of linear logic) in front of negative connectives while a co-intuitionistic reading will add a “?” (why-not connective of linear logic) in front of positive connectives.

## B. Infinite sequences

We write $A^N$ for the infinite (countable) sequences of elements of A. There are different ways to represent such an infinite sequence:

* We can represent it as a function, i.e. as a functional object of type $\mathbb{N} \to A$.

* We can represent it as a total functional relation, i.e. as a relation R of type $\mathbb{N} \to A \to \text{Prop}$ such that $\forall n \exists! a R(n, a)$.

* Additionally, when A is $\mathbb{B}$, an extra possible representation is as a predicate P over $\mathbb{N}$ with intended meaning 1 if $P(n)$ holds and 0 if $\neg P(n)$ holds (and unknown meaning otherwise).

The representation as a functional relation is weaker in the sense that a function $\alpha$ induces a functional relation $\lambda n. \lambda a. \alpha(n) = a$ but the converse requires the axiom of unique choice. In the sequel, we will use the notation $\alpha(n) = a$ and $\alpha(n) \triangleq a$ to mean different things depending on the representation chosen for $\mathbb{N} \to B$.

In the first case, $\alpha(n) = a$ means $\alpha(n) =_A a$ where $=_A$ is the equality on A. Similarly, $\alpha(n) \triangleq a$ defines the function $\alpha \triangleq \lambda n. a$.

In the second case, $\alpha(n) = a$ however means $\alpha(n, a)$ and $\alpha(n) \triangleq a$ defines the functional relation $\alpha \triangleq \lambda(n, a')$. ($a' = a$) where n can occur in a.

When A is $\mathbb{B}$, the representation as a predicate P is even weaker in the sense that a functional relation R induces a predicate $\lambda n. R(n, 1)$ but the converse requires classical reasoning. We can easily turn a predicate P into a relation $\lambda n. \lambda b$. (if b then $P(n)$ else $\neg P(n)$) but proving $\forall n \exists! b$ (if b then $P(n)$ else $\neg P(n)$) requires a call to excluded-middle on $P(n)$.

When A is $\mathbb{B}$ and $\alpha$ is a predicate, we define $\alpha(n) = 1$ as $\alpha(n)$ and $\alpha(n) = 0$ as $\neg \alpha(n)$. Technically, this means seeing $\alpha(n) = b$ as a notation for “if b then $\alpha(n)$ else $\neg \alpha(n)$”. Similarly, $\alpha(n) \triangleq b$ defines $\alpha \triangleq \lambda n$. (if b then $\top$ else $\bot$).

In particular, this means that *all choice and bar induction statements of this paper* have two readings of a different logical strength (depending on the validity of the axiom of unique choice in the metatheory), or even three readings (depending on the validity of the axiom of unique choice *and* of classical reasoning) when the codomain of the function mentioned in the theorems is $\mathbb{B}$.

If $\alpha \in A^N$, we write $u \prec_s \alpha$ to mean that $u$ is an initial prefix of $\alpha$. This is defined inductively by the following clauses:

$$ \frac{u \prec_s \alpha}{\langle\rangle \prec_s \alpha} \quad \frac{\alpha(|u|) = a}{u \star a \prec_s \alpha} $$

If $a \in A$ and $\alpha \in A^N$, we write $a@\alpha$ for the sequence $\beta$ defined by $\beta(0) \triangleq a$ and $\beta(n+1) \triangleq \alpha(n)$.

We have the following easy property:

*Proposition 1:* If $u \prec_s \alpha$ then $a@u \prec_s a@\alpha$.
<table><caption>TABLE II
LOGICALLY EQUIVALENT DUAL CONCEPTS ON DUAL PREDICATES</caption><tr><td>T is a tree<br>(closure under restriction)<br>∀u ∀a (u★a ∈ T ⇒ u ∈ T)</td><td>T is monotone<br>(closure under extension)<br>∀u ∀a (u ∈ T ⇒ u★a ∈ T)</td></tr></table>

<table><caption>TABLE III
LOGICALLY OPPOSITE CLOSURE OPERATORS ON DUAL PREDICATES</caption><tr><td>downwards arborification of T<br>(↓−T)<br>λu. ∀u' (u' ≤s u ⇒ u' ∈ T)</td><td>upwards monotonisation of T<br>(↑+T)<br>λu. ∃u' (u' ≤s u ∧ u' ∈ T)</td></tr><tr><td>upwards arborification of T<br>(↑−T)<br>λu. ∃u' (u ≤s u' ∧ u' ∈ T)</td><td>downwards monotonisation of T<br>(↓+T)<br>λu. ∀u' (u ≤s u' ⇒ u' ∈ T)</td></tr></table>

### C. Trees and monotone predicates

Let $B$ be a type and $T$ be a predicate on $B^*$. We overload the notation $u \in T$ to mean that $T$ holds on $u \in B^*$. We say that $T$ is finitely-branching if $B$ is in bijection with a non-empty bounded subset of $\mathbb{N}$ (i.e. to $\{n : \mathbb{N} | n \le p\}$ for some $p$).

We say that $T$ is a tree if it is closed under restriction, and, dually, that $T$ is monotone if it is closed under extension (the formal definitions are given in Table II). Classically, we have $T$ monotone iff $\neg T$ is a tree, and, dually, $\neg T$ monotone iff $T$ is a tree. In particular, another way to describe a tree is as an antimonotone predicate<fnref n="4" />. It is convenient for the underlying intuition to restrict oneself to predicates which are trees, or which are monotone, even if it does not always matter in practice. When it matters, a predicate is turned into a tree either by discarding sequences not connected to the root or by completing it with missing sequences from the root: these are respectively the *downwards arborification* $↓−T$ and *upwards arborification* $↑−T$ of a predicate, as shown in Table III. We dually write $↑+T$ and $↓+T$ for the *upwards monotonisation* and *downwards monotonisation* of $T$. Arborification and monotonisation are idempotent. We shall in general look for minimal definitions of the concept involved in the paper, and thus consider arbitrary predicates as much as possible, turning them into trees or monotone predicates only when needed to give sense to the definitions.

### D. Well-foundedness and ill-foundedness properties

We list properties on predicates which are relevant for stating ill-foundedness axioms (i.e. choice axioms), and their dual well-foundedness axioms (i.e. bar induction axioms). Duality can be understood both under a classical or linear interpretation of the connectives, where the predicate $T$ in one column is supposed to be dual of the predicate $T$ occurring in the other column (dual

predicates if in linear logic, negated predicates if in classical logic). Table IV details properties which differ by contraposition and are thus logically equivalent (in classical and linear logic). On the other side, tables V and VI detail properties which are logically opposite.

<table><caption>TABLE IV
BASIC LOGICALLY EQUIVALENT DUAL PROPERTIES ON DUAL PREDICATES</caption><tr><td>T is progressing at u (*)<br>u ∈ T ⇒ (∃a u★a ∈ T)</td><td>T is hereditary at u<br>(∀a u★a ∈ T) ⇒ u ∈ T</td></tr><tr><td>T is progressing (*)<br>∀u (T is progressing at u)</td><td>T is hereditary<br>∀u (T is hereditary at u)</td></tr></table>

We indicated with (*) concepts for which we did not find an existing terminology in the literature. Thus, the terminology is ours. Also, what we called *staged infinite* is often simply called *infinite*. We used *staged infinite* to make explicit the difference from a definition based on the presence of an infinite number of nodes. Thereby we also obtain a symmetry with the notion of *staged barred*. What we call *having an infinite branch* could alternatively be called *ill-founded*, or *having a choice function*. In particular, the terminology *having an infinite branch* applies here to any predicate and is not restricted to trees. Note that *well-founded* in the standard meaning is the same as *barred* for the dual predicate. In particular, when opposing ill-foundedness and well-foundedness, we adopt a bias towards the tree view, i.e. towards the left column. We have the following:

**Proposition 2:** If $T$ is a tree, then having unbounded paths is equivalent to being staged infinite. Dually, if $T$ is monotone, being a uniform bar is equivalent to being staged barred.

<table><caption>TABLE V
LOGICALLY OPPOSITE DUAL CONCEPTS ON DUAL PREDICATES</caption><tr><td>ill-foundedness properties</td><td>well-foundedness properties</td></tr><tr><td colspan="2">closure operators</td></tr><tr><td>pruning of T<br>νX.λu. (u ∈ T ∧ ∃a u★a ∈ X)</td><td>hereditary closure of T<br>μX.λu. (u ∈ T ∨ ∀a u★a ∈ X)</td></tr><tr><td colspan="2">intensional concepts</td></tr><tr><td>T is a spread<br>⟨⟩ ∈ T ∧ T progressing</td><td>T is barricaded (*)<br>T hereditary ⇒ ⟨⟩ ∈ T</td></tr><tr><td>T is productive<br>⟨⟩ ∈ pruning of T</td><td>T is inductively barred<br>⟨⟩ ∈ hereditary closure of T</td></tr><tr><td colspan="2">intensional concepts relevant for the finite case</td></tr><tr><td>T has unbounded paths<br>∀n ∃u (|u| = n ∧ u ∈ ↓−T)</td><td>T is uniformly barred<br>∃n ∀u (|u| = n ⇒ u ∈ ↑+T)</td></tr><tr><td>T is staged infinite<br>∀n ∃u (|u| = n ∧ u ∈ T)</td><td>T is staged barred (*)<br>∃n ∀u (|u| = n ⇒ u ∈ T)</td></tr><tr><td colspan="2">extensional concepts</td></tr><tr><td>T has an infinite branch<br>∃α ∀u (u &lt;= s α ⇒ u ∈ T)</td><td>T is barred<br>∀α ∃u (u &lt;= s α ∧ u ∈ T)</td></tr></table>

<footnote n="4">⁴From a categorical perspective, a tree is a contravariantly functorial predicate over the preorder generated by $u \le s v$, while a monotone predicate is covariantly functorial.</footnote>
<table><caption>TABLE VI
USEFUL RELATIVISATION OF SOME OF THE CONCEPTS OF TABLE V</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td colspan="2">relativised intensional concepts</td></tr><tr><td>T is productive from <i>u</i><br><i>u</i> &isin; pruning of T</td><td>T is inductively barred from <i>u</i><br><i>u</i> &isin; hereditary closure of T</td></tr><tr><td colspan="2">relativised intensional concepts relevant for the finite case</td></tr><tr><td>T has unbounded paths from <i>u</i><br><i>&forall;n</i> &exist;u' (<i>|u'|</i> = <i>n</i> &and; <i>u</i>@<i>u'</i> &isin; &darr; T)</td><td>T is uniformly barred from <i>u</i><br><i>&exist;n</i> &forall;u' (<i>|u'|</i> = <i>n</i> &rarr; <i>u</i>@<i>u'</i> &isin; &darr; T)</td></tr><tr><td colspan="2">extensional concepts</td></tr><tr><td>T has an infinite branch from <i>u</i><br><i>&exist;&alpha;</i> &forall;u' (<i>u'</i> &lt;_s <i>&alpha;</i> &rarr; <i>u</i>@<i>u'</i> &isin; T)</td><td>T is barred from <i>u</i><br><i>&forall;&alpha;</i> &exist;u' (<i>u'</i> &lt;_s <i>&alpha;</i> &and; <i>u</i>@<i>u'</i> &isin; T)</td></tr></tbody></table>

**PROOF:** Because trees and monotone predicates are invariant under arborification and monotonisation. ■

As a consequence, it is common to use the notion of staged infinite, which is simpler to formulate, when we know that $T$ is a tree. Otherwise, if $T$ is an arbitrary predicate which is not necessarily a tree, there is no particular interest in using the notion of staged infinite. Similarly, staged barred is a simpler way to state uniformly barred when $T$ is monotone, i.e., conversely, uniform bar is the expected refinement of staged barred when $T$ is not known to be monotone.

A progressing $T$ may be productive at $\langle\rangle$ without being productive at all $u \in T$, so we may need to prune $T$ to extract from it a spread. Dually, not all barricaded predicates are inductive bars at all $u$ but we can saturate them into inductive bars, by taking the hereditary closure. We make this formal in the following proposition:

**Proposition 3:** If $T$ is productive then its pruning is a spread. Dually, if $T$ is barricaded then its hereditary closure is an inductive bar.

**PROOF:** That $\langle\rangle$ is in the pruning of $T$ is direct from $T$ productive. That the pruning of $T$ is progressing on all $u$ is also direct by construction of the pruning. The other part of the statement is by duality. ■

Conversely, by coinduction, the pruning of any progressing predicate $T$ contains $T$ and dually, induction shows that the hereditary closure of an hereditary predicate $T$ is included in $T$. Thus, we have:

**Proposition 4:** $T$ spread implies $T$ productive, and, dually, $T$ inductively barred implies $T$ barricaded. □

We can then relate productive and spread, as well as inductive bar and barricaded as follows:

**Proposition 5:** $T$ is productive iff there exists $U \subseteq T$ which is a spread. Dually, $T$ is an inductive bar iff all $U \supseteq T$ is barricaded.

**PROOF:** By duality, it is enough to prove the first equivalence. From left to right, we use Prop. 3, observing that the pruning of $T$ is included in $T$. From right to left, a spread is productive and a coinduction suffices to prove that inclusion preserves productivity. ■

On the other side, having unbounded paths is equivalent to being a spread or to being productive only when $T$ is finitely-branching. Similarly for being uniformly barred compared to being an inductive bar or being barricaded. Moreover, none of the equivalences hold linearly. The second one requires intuitionistic logic, i.e. requires the ability to use an hypothesis several times while the first one, dually, requires a bit of classical reasoning<fnref n="5" />.

For $S$ being a class of formulae and $P$ and $Q$ ranging over $S$, let $D_S$ be the principle $\forall xy(P(x) \lor Q(y)) \Rightarrow (\forall x P(x)) \lor (\forall y Q(y))$. Dually, let $C_S$ be $(\exists x P(x)) \land (\exists y Q(y)) \Rightarrow \exists x \exists y (P(x) \land Q(y))$.

**Proposition 6:** If $B$ is non-empty finite, then productive is equivalent to having unbounded paths and being an inductive bar is equivalent to uniformly barred. The first statement holds in a logic where $D_S$ holds and the second in a logic where $C_S$ holds, for $S$ a class of formulae containing arithmetical existential quantification over $T$.

**PROOF:** Relying on duality, we only prove the first statement. Based on our definition of finite, we also assume without loss of generality that $B$ is $\mathbb{B}$. Our proof relies on an argument found in [3], [18] and proceeds by proving more generally for $u \in \downarrow T$ that $T$ is productive from $u$ iff $T$ has unbounded paths from $u$.

From left to right, we reason by induction on $n$. If $n$ is 0 this is direct from $T$ productive by defining $u' \triangleq \langle\rangle$. Otherwise, by $T$ productive from $u$, we get $a$ such that $T$ is productive from $u \star a$, obtaining by induction $u'$ of length $n-1$ such that $(u \star a)@u' = u@(a@u') \in \downarrow T$, showing that $a@u'$ is the expected sequence of length $n$.

From right to left, we reason coinductively. To prove that $u \in T$, we take a path of length 0. Then, in order to apply the coinduction hypothesis and prove the coinductive part, we prove that there is $b$ such that $T$ has unbounded paths from $u \star b$. By $D_S$, it is enough to prove that for all $n_0$ and $n_1$, there is a path $u_0$ of length $n_0$ and a path $u_1$ of length $n_1$ such that either $(u \star 0)@u_0$ or $(u \star 1)@u_1$ is in $\downarrow T$. So, let $n_0$ and $n_1$ be given lengths. By unbounded paths from $u$, we get a sequence $u''$ of length $\max(n_0, n_1) + 1$ such that $u@u'' \in \downarrow T$. This is a non-empty sequence, hence a sequence of the form $b@u'$ so that we have either $(u \star 0)@u' \in \downarrow T$ or $(u \star 1)@u' \in \downarrow T$ for $u'$ of length $\max(n_0, n_1)$. By closure of $\downarrow T$, prefixes $u_0$ of length $n_0$ and $u_1$ of length $n_1$ of $u'$ can be extracted which both are in $\downarrow T$. ■

**Remark:** Based on the decomposition of WKL for decidable trees into a choice principle and the Lesser Limited Principle of Omniscience (LLPO), we suspect that we actually have the stronger result that the equivalence of unbounded paths and productivity implies $D_S$ for the corresponding underlying class of formulae $S$, and similarly with $C_S$ and the dual statement.

<footnote n="5">⁵or, to be more precise, co-intuitionistic reasoning, that is, using a multi-conclusion sequent calculus to formulate the reasoning, with the contraction rule allowed on conclusions but not on hypotheses</footnote>
## E. Bar induction and tree-based dependent choice

In the first part of Table VII, we reformulate using our definitions the standard statement of bar induction and a tree-based formulation of dependent choice from the literature. The standard form of Bar Induction, as e.g. in [21], corresponds in our classification to $B|_{BT}^{ind}$, apart from the fact that we do not fix in advance the logical complexity of $B$ – such as being countable or not – or the arithmetic strength of $T$ – i.e. whether it is decidable, or recursively enumerable, etc. For dependent choice<fnref n="6" />, we consider here a pruned-tree-based definition $DC_{BT}^{spread}$ corresponding to the instance $DC_{N_0}$ of Levy's family of Dependent Choice indexed on cardinals [23]<fnref n="7" />. A comparison with other logically equivalent definitions of dependent choice will be given in Section II-H.

These formulations of Tree-based Dependent Choice and Bar Induction are not dual<fnref n="8" /> of each other but Prop. 5 gives us a way to connect each one with the dual of the other:

**Theorem 1:** As schemes, generalised over $T$, $DC_{BT}^{spread}$ and $DC_{BT}^{productive}$ are equivalent, and so are $B|_{BT}^{barricaded}$ and $B|_{BT}^{ind}$. □

## F. König's Lemma and the Fan Theorem

The second part of Table VII is about König's Lemma and the Fan Theorem.

The Fan Theorem is sometimes stated over finitely-branching trees, where the definition of finite itself may vary [21], [18], but it is also sometimes considered by default to be on a binary tree [2], [4], [3], [7], [9], [19] in which case the finite version is sometimes called extended. We call here Fan Theorem the finite version, for *finite* defined as being in bijection with a finite prefix of $N$, and for all branchings being on the same finite $B$. The statement of the Fan Theorem sometimes relies on the notion of inductive bar (e.g. [9]), what we call here $FT_{BT}^{ind}$, or on the definition of staged barred for monotone predicates (as a variant in [19]), called here $FT_{BT}^{staged}$, or on the dual notions of finite tree (i.e., technically of staged barred for the negation of a tree) and well-founded tree (i.e., technically of inductively barred for the negation of a tree) in e.g. [5], which respectively corresponds to $FT_{BT}^{staged}$ and $FT_{BT}^{ind}$ for $T^C$ the complement of $T$. But it also often relies on the definition of uniform bar [2], [3], [4], [7], [18], [19], [21] over an arbitrary predicate, what we call here $FT_{BT}^{uniform}$. Note that, as in the case of bar induction, we omit the usual restriction of the statement of the Fan Theorem to decidable predicates.

König's Lemma is generally stated as $T$ infinite tree implies $T$ has an infinite branch, but the definition of $T$ infinite may differ from author to author. The definition in [5], [18] expresses explicitly that the infinity can only be in depth. It does so by requiring arbitrary long branches rather than an infinite number of nodes. The exact definition of arbitrarily long branches also depends on authors. For instance, [30] relies (up to classical reasoning) on having unbounded paths for arbitrary predicates

<table><caption>TABLE VII
TREE-BASED DEPENDENT CHOICE AND BAR INDUCTION DUAL PRINCIPLES</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td colspan="2"><em>T</em> branching over arbitrary <em>B</em></td></tr><tr><td>Tree-based Dependent Choice (DC<sub>BT</sub><sup>spread</sup>)<br><em>T</em> spread ⇒<br><em>T</em> has an infinite branch</td><td>Alternative Bar Induction (B<sub>BT</sub><sup>barricaded</sup>)<br><em>T</em> barred ⇒<br><em>T</em> is barricaded</td></tr><tr><td>Alternative Tree-based Dependent Choice (DC<sub>BT</sub><sup>productive</sup>)<br><em>T</em> productive ⇒<br><em>T</em> has an infinite branch</td><td>Bar Induction (B<sub>BT</sub><sup>ind</sup>)<br><em>T</em> barred ⇒<br><em>T</em> inductively barred</td></tr><tr><td colspan="2"><em>T</em> branching over non-empty finite <em>B</em></td></tr><tr><td>KL<sub>BT</sub><sup>spread</sup> ≜ DC<sub>BT</sub><sup>spread</sup> (finite <em>B</em>)<br>KL<sub>BT</sub><sup>productive</sup> ≜ DC<sub>BT</sub><sup>prod.</sup> (fin. <em>B</em>)</td><td>FT<sub>BT</sub><sup>barricaded</sup> ≜ B<sub>BT</sub><sup>barric.</sup> (fin. <em>B</em>)<br>FT<sub>BT</sub><sup>ind</sup> ≜ B<sub>BT</sub><sup>ind</sup> (finite <em>B</em>)</td></tr><tr><td>Alternative König's Lemma (KL<sub>BT</sub><sup>unbounded</sup>)<br><em>T</em> with unbounded paths ⇒<br><em>T</em> has an infinite branch</td><td>Fan Theorem (FT<sub>BT</sub><sup>uniform</sup>)<br><em>T</em> barred ⇒<br><em>T</em> uniform bar</td></tr><tr><td>König's Lemma (KL<sub>BT</sub><sup>staged</sup>)<br><em>T</em> staged-infinite tree ⇒<br><em>T</em> has an infinite branch</td><td>Staged Fan Theorem (FT<sub>BT</sub><sup>staged</sup>)<br><em>T</em> barred and monotone ⇒<br><em>T</em> staged barred</td></tr></tbody></table>

rather than trees, what we call here $KL_{BT}^{unbounded}$, but most of the time it is about what we call staged infinite tree [3], [18], [19], leading formally to the definition $KL_{BT}^{staged}$. The versions $KL_{BT}^{staged}$ and $KL_{BT}^{unbounded}$ imply LLPO [17]. Contrastingly, the versions which we call $KL_{BT}^{spread}$ and $KL_{BT}^{productive}$ are “pure choice” versions not implying LLPO (see Prop. 6 for the connection). The binary variant $KL_{BT}^{spread}$ of the former occurs for instance in the literature with name $C_{WKL}$ [3].

There is a standard way to go from arbitrary predicates to trees or monotone predicates by associating to each predicate its (downward or upwards) tree or monotone closure. This allows to show that it is equivalent to state König's Lemma on trees using staged-infinity or on arbitrary predicates using unbounded paths, and, similarly, that it is equivalent to state the Fan Theorem on monotone predicates using staged barred ($FT_{BT}^{staged}$) or on arbitrary predicates using uniformly barred.

**Proposition 7:** As schemes, when generalised over $T$, $KL_{BT}^{staged}$ is equivalent to $KL_{BT}^{unbounded}$ and $FT_{BT}^{staged}$ to $FT_{BT}^{uniform}$.

**PROOF:** We treat the first equivalence. From left to right, if $T$ is a predicate, we apply $KL_{BT}^{staged}$ to $\downarrow^T T$. The resulting infinite branch is an infinite branch in $T$ because $\downarrow^T T \subseteq T$. From right to left, the statement holds by Prop. 2. The second equivalence is by duality. ■

## G. Choice and bar induction as relating intensional and exten-
sional concepts

The intensional definitions are stronger than the extensional ones, which implies that the choice and bar induction axioms can alternatively be seen as stating the logical equivalence of

<footnote n="6">⁶or dependent choices for some authors, e.g. [20]</footnote>

<footnote n="7">⁷Alternatively, it can be seen as the generalisation to arbitrary codomains of the Boolean dependent choice principle $DC^V$ described e.g. in Ishihara [18].</footnote>

<footnote n="8">⁸This might be related to coinductive reasoning historically coming later and being less common than inductive reasoning in mathematics.</footnote>
the intensional and extensional versions of ill-foundedness and well-foundedness properties (of various strengths).

**Theorem 2:** *T* inductively barred implies *T* barred. Dually, *T* has an infinite branch implies *T* is productive.

**PROOF:** We prove by induction on the definition of *T* inductively barred that *T* inductively barred at *u* implies *T* barred from *u* where the latter requires that for all *α*, there is *u'* ≺<sub>*s*</sub> *α* such that *u*@*u'* ∈ *T*.

If $u \in T$, then it is enough to take $\langle\rangle$ for $u'$ to get $u@\langle\rangle \in T$ for any $\alpha$. If $T$ is barred from $u \star b \in T$ for all $b \in B$, this means that there is $u' \prec_s \beta$ such that $(u \star b)@u' \in T$ for any $\beta$. For a given $\alpha$, set $b \triangleq \alpha(0)$ and $\beta(n) \triangleq \alpha(n+1)$ so that we can find $u' \prec_s \beta$, hence $b@u' \prec_s b@\beta$, i.e. $b@u' \prec_s \alpha$ (by Prop. 1) together with $u@(b@u') \in T$.

The dual proof builds *T* productive at *u* from *T* has an infinite branch from *u* by coinduction. From the infinite branch *α* from *u* and $\langle\rangle$ ≺<sub>*s*</sub> *α* we get $u@\langle\rangle \in T$, i.e. $u \in T$. It remains to find *b* such that *T* is productive from $u \star b$ and it suffices to take *α*(0) since *T* has an infinite branch $\beta(n) \triangleq \alpha(n+1)$ from $u \star \alpha(0)$ simply because $v \prec_s \alpha$ implies $\alpha(0)@v \prec_s \alpha(0) \star \beta$ (by Prop. 1) and $(u \star \alpha(0))@v \in T$ from $u@(\alpha(0)@v) \in T$. ■

**H. Relation to other formulations of Dependent Choice and to countable Zorn's Lemma**

For *R* a relation on *B*, it is common to formulate dependent choice as

$$ \forall b^B \exists b'^B R(b, b') \Rightarrow \forall b_0^B \exists f^{\mathbb{N} \to B} (f(0) = b_0 \wedge \forall n R(f(n), f(n+1))). $$

Let us call *serial* a (homogeneous) relation such that $\forall b^B \exists b'^B R(b, b')$ holds. In this section, we formally compare the resulting statement of dependent choice to $\mathcal{D}C_{BT}^{\text{productive}}$, examining also dual statements.

Let *R* be a serial relation, i.e. a relation such that $\forall b^B \exists b'^B R(b, b')$. Using a seed $b_0$, each such relation *R* can be turned into a predicate on $B^*$ under the two following ways:

* The *chaining* $R_{\top}^*(b_0)$ from $b_0$ is probably the most natural one: it says that $u \in R_{\top}^*(b_0)$ if all steps in $u$ from $b_0$ are in *R*.

* The *alignment* $R_{\top}^{\succ}(b_0)$ from $b_0$ artificially uses non-empty sequences to represent pairs of elements. We have $u \in R_{\top}^{\succ}(b_0)$ either when $u$ has at least two elements and the last two elements are related by *R*, or, when the sequence contains exactly one element which is related to $b_0$, or, finally, when the sequence is simply empty.

Reasoning by induction on $v \leq_s u$ in one direction and on $u$ in the other direction, we can show that both are related:

*Proposition 8:* $u \in R_{\top}^*(b_0)$ iff $u \in \downarrow R_{\top}^{\succ}(b_0)$

<figure><img src="image_1.png" /></figure>

Dually, we can define *antichaining* and *blockings* such that:

*Proposition 9:* $u \in R_{\perp}^*(b_0)$ iff $u \in \uparrow R_{\perp}^{\succ}(b_0)$

<figure><img src="image_2.png" /></figure>

The formal definitions are given in Table VIII, where we can notice that the use of $\mu$ vs. $\nu$ does not matter in practice since the structure of the relation is a function of $|u|$.

We are now in position to state in Table IX a relatively standard form of Dependent Choice which we call $\mathcal{D}C_{BRb_0}^{\text{serial}}$ for *R* being a relation on *B* and $b_0$ a seed in *B*. Though to

<table><caption>TABLE VIII
LOGICALLY OPPOSITE DUAL CONCEPTS ON DUAL HOMOGENEOUS RELATIONS</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td colspan="2" style="text-align: center;">intensional concepts</td></tr><tr><td><b>R</b> serial<br>∀b ∃b' R(b, b')</td><td><b>R</b> has a “least” element<br>∃b ∀b' R(b, b')</td></tr><tr><td><b>R</b> left-not-full (*)<br>∀b ∃b' ¬R(b, b')</td><td><b>R</b> has a “maximal” element<br>∃b ∀b' ¬R(b, b')</td></tr><tr><td>chaining of <b>R</b> from <i>b</i><sub>0</sub> (<b>R</b><sub>⊥</sub><sup>*</sup>(<i>b</i><sub>0</sub>))<br>μX.λb. λu.<br>case <i>u</i> of<br>$$ \begin{bmatrix} \langle\rangle & \mapsto \top \\ b' \star u & \mapsto R(b, b') \wedge X(b', u) \end{bmatrix} $$</td><td>antichain. of <b>R</b> from <i>b</i><sub>0</sub> (<b>R</b><sub>⊥</sub><sup>*</sup>(<i>b</i><sub>0</sub>))<br>νX.λb. λu.<br>case <i>u</i> of<br>$$ \begin{bmatrix} \langle\rangle & \mapsto \bot \\ b' \star u & \mapsto R(b, b') \vee X(b', u) \end{bmatrix} $$</td></tr><tr><td>alignment of <b>R</b> from <i>b</i><sub>0</sub> (<b>R</b><sub>⊥</sub><sup>≥</sup>(<i>b</i><sub>0</sub>))<br>λu. case <i>u</i> of<br>$$ \begin{bmatrix} \langle\rangle & \mapsto \top \\ b & \mapsto R(b_0, b) \\ u' \star b \star b' & \mapsto R(b, b') \end{bmatrix} $$</td><td>blockings of <b>R</b> from <i>b</i><sub>0</sub> (<b>R</b><sub>⊥</sub><sup>≥</sup>(<i>b</i><sub>0</sub>))<br>λu. case <i>u</i> of<br>$$ \begin{bmatrix} \langle\rangle & \mapsto \bot \\ b & \mapsto R(b_0, b) \\ u' \star b \star b' & \mapsto R(b, b') \end{bmatrix} $$</td></tr></tbody></table>

<table><caption>TABLE IX
DEPENDENT CHOICE AND BAR INDUCTION PRINCIPLES</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td>Dependent Choice ($\mathcal{D}C_{BRb_0}^{\text{serial}}$)</td><td>Dual to Dependent Choice ($\mathcal{B}^{\text{least}}_{BRb_0}$)</td></tr><tr><td><i>R</i> serial ⇒<br>$R_{\top}^{\succ}(b_0)$ has an infinite branch</td><td>$R_{\perp}^{\succ}(b_0)$ barred ⇒<br>$\bar{R}$ has a least element</td></tr></tbody></table>

our knowledge uncommon in the literature, we also mention its dual which we call $\mathcal{B}^{\text{least}}_{BRb_0}$.

We state a few results that allow to show the equivalence of $\mathcal{D}C_{BRb_0}^{\text{serial}}$ and $\mathcal{D}C_{BT}^{\text{productive}}$ as schemes.

We have the following properties.

**Proposition 10:** *R* serial implies $R_{\top}^{\succ}(b_0)$ productive for any $b_0$. Dually, if $R_{\perp}^{\succ}(b_0)$ is inductively barred then *R* has a least element.

**PROOF:** We prove by coinduction that $u \in R_{\top}^{\succ}(b_0)$ implies $R_{\top}^{\succ}(b_0)$ productive from $u$. If $u$ is empty, $R_{\top}^{\succ}(b_0)(\langle\rangle)$ holds by definition and there is by seriality a $b_1$ such that $R_{\top}^{\succ}(b_0)(b_1)$. This allows to conclude by coinduction hypothesis. If $u$ has the form $u' \star b$, there is also by seriality a $b'$ such that $R_{\top}^{\succ}(b_0)(u' \star b \star b')$ and we can again conclude by coinduction hypothesis. The productivity of $R_{\top}^{\succ}(b_0)$ finally follows because $R_{\top}^{\succ}(b_0)(\langle\rangle)$ holds by definition. The dual statement is by dual (inductive) reasoning. ■

Conversely, for *T* a predicate, let $B_T$ be defined by $B_T \triangleq \{u \in B^* | T$ is productive from $u\}$ and let $R_T$ be the relation on $B_T$ defined by $R_T(u, u') \triangleq \exists b (u \star b = u')$. The relation $R_T$ is serial by construction: for $u$ such that $T$ is productive from $u$, there is a such that $T$ is productive from $u \star a$ and $u \star a \in T$. Also, $\langle\rangle \in B_T$ as soon as $T$ is productive.
<table><caption>TABLE X
LOGICALLY OPPOSITE DUAL CONCEPTS ON DUAL RELATIONS</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td>R A-B-left-total</td><td>R A-B-grounded (*)</td></tr><tr><td>∀a ∃b R(a, b)</td><td>∃a ∀b R(a, b)</td></tr><tr><td>R has an A-B-choice function</td><td>R is A-B-barred</td></tr><tr><td>∃α ∀a ∀b (α(a) = b ⇒ R(a, b))</td><td>∀α ∃a ∃b (α(a) = b ∧ R(a, b))</td></tr></tbody></table>

<table><caption>TABLE XI
COUNTABLE CHOICE AND WEAK BAR INDUCTION PRINCIPLES</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td>Countable Choice (CC<sub>BR</sub>)</td><td>Dual to Countable Choice (WBI<sub>BR</sub>)</td></tr><tr><td>R <span style="text-decoration: overline;">N</span>-B-left-total ⇒</td><td>R <span style="text-decoration: overline;">N</span>-B-barred ⇒</td></tr><tr><td>R has an <span style="text-decoration: overline;">N</span>-B-choice function</td><td>R <span style="text-decoration: overline;">N</span>-B-grounded</td></tr></tbody></table>

We can now formally state the correspondence in our language:

**Theorem 3:** As schemes, $DC_{BT}^{productive}$ and $DC_{BRb_0}^{serial}$ are logically equivalent.

**PROOF:** From left to right, we take $R_T^>(b_0)$ and use Prop. 10. From right to left, we take $B_T$ and $R_T$, obtaining $\langle\rangle \in B_T$ from $T$ productive. We get an infinite branch $\beta$ of elements of $B_T$ such that $u \prec_s \beta$ implies $(R_T)^>(\langle\rangle)(u)$, which means first that $R_T(\langle\rangle, \beta(0))$, thus $\beta(0) = b$ for some $b$, then, secondly, that for all $n$, $R_T(\beta(n), \beta(n+1))$, i.e. $\beta(n+1) = \beta(n) \star b$ for some $b$. It is then enough to define $\alpha(n)$ to be the corresponding $b$ to get an infinite branch of elements of $B$. Let us now consider $u \prec_s \alpha$. We already know $\langle\rangle \in T$ from $T$ productive. Otherwise, for $u$ non empty, we get by induction that $u$ coincides with $\beta(|u|-1)$ which is in $T$ because $u \in B_T$ implies $T$ being productive from $u$. ■

As a final remark, let us mention countable Zorn's lemma [31]: *If a partial order $S$ on some set has no countable chain, it has a maximal element.* It corresponds to the instantiation on $\neg S$ of the generalisation of the scheme $R^*_\perp(b_0)$ barred implies $R$ has a least element over all $b_0$, using our definitions up to classical reasoning, and dropping the partial order requirement. This is the case because a least element is a maximal one in the complement of a relation and because, classically, the barring of all antichainings of $\neg S$ is the same as the absence of countable chains in a partial order $S$.

### I. Relation to countable choice

For $R$ heterogeneous relation on $A$ and $B$, we introduce in Table X definitions allowing to state in Table XI the axiom of countable choice, CC, and its dual, which we call weak bar induction. Note that left-total and grounded are respective generalisations of serial and having a least element to non-necessarily homogeneous relations.

We shall prove that CC is derivable from $DC_{BT}^{productive}$ and introduce for that the alignment of a sequential relation over

<table><caption>TABLE XII
LOGICALLY OPPOSITE DUAL CONCEPTS ON DUAL RELATIONS</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td colspan="2" style="text-align: center;">intensional concepts</td></tr><tr><td>seq. pos. alignment of R (R<sub>T</sub><sup>N</sup>)<br>λu. case u of<br>$$ \begin{bmatrix} \langle\rangle & \mapsto \top \\ u \star b & \mapsto R(|u|, b) \end{bmatrix} $$</td><td>seq. neg. alignment of R (R<sub>⊥</sub><sup>N</sup>)<br>λu. case u of<br>$$ \begin{bmatrix} \langle\rangle & \mapsto \bot \\ u \star b & \mapsto R(|u|, b) \end{bmatrix} $$</td></tr></tbody></table>

$\mathbb{N} \times A$ as a predicate over $A^*$ (see Table XII). We have:

**Theorem 4:** For $B$ and $R$ given ($R$ relation over $\mathbb{N}$ and $B$), $CC_{BR}$ is equivalent to $DC_{BRb_0}^{productive}$. Dually, $WBI_{BR}$ is equivalent to $BI_{BRb_0}^{ind}$.

**PROOF:** The correspondence between $R$ left-total and $R_T^N$ productive is obtained by coinduction from left to right and, from right to left, by extracting the $n$th element of the proof of $R_T^N$ to get the image of $n$ by $R$. The function relating $R$ having a choice function (as a relation) and $R_T^N$ having a choice function (as a predicate on $B^*$) is the same. Then, from left to right, for non-empty $u \star b \prec_s \alpha$, we have $\alpha(|u|) = b$, thus $R(|u|, b)$ and $u \in T$. From right to left, for $n$ and $b$ such that $\alpha(n) = b$, the restriction $\alpha|_{n+1}$ of $\alpha$ to its first $n+1$ elements is in $T$, so that $R(|\alpha|_n|, b)$, i.e. $R(n, b)$. Similarly for the dual case. ■

We do not conversely expect to be able in general to express $DC_{BT}^{productive}$ in terms of CC since countable choice is strictly weaker than dependent choice, and similarly for $BI^{ind}$ in terms of WBI. However, if $B$ is countable, it is folklore that the statements of DC and CC become mutually expressible by classical-reasoning-based minimisation: their common strength as choice principle then is not greater than the axiom of unique choice. The latter itself is a tautology if functions are represented as functional relations. It has however the logical effect of reifying functional relations as proper functions if functions are represented as proper objects in a functional type. We conjecture that the equivalence of $BI^{ind}$ and WBI with countable codomain is provable intuitionistically.

### III. NON SEQUENTIAL GENERALISATION OF DEPENDENT CHOICE AND BAR INDUCTION

In the previous section, we considered predicates branching countably many times over a domain $B$. In this section, we investigate how to generalise countable sequences of branches to branching in an arbitrary order over a non-necessarily countable domain $A$.

When $B$ is $\mathbb{B}$, we shall obtain principles equivalent to the Boolean Prime Ideal/Filter Theorem (ill-founded case), or to the Completeness Theorem but we shall recover the strength of dependent choice (ill-founded case) and bar induction (well-founded case) when $A$ is countable, that is when $A$ is in bijection with $\mathbb{N}$. In particular we will obtain the strength of the Weak Fan Theorem (well-founded case) and Weak Kőnig's Lemma (ill-
founded case), up to classical reasoning, when A is countable and B is $\mathbb{B}$.

For a certain instance, we will get the strength of the full axiom of choice. However, the new principle is limited. For instance, for $A \triangleq \mathbb{B}^N$ and $B \triangleq \mathbb{N}$, we end up with an inconsistent axiom.

### A. Finite approximations of functions

Let A be a domain whose elements are ranged over by the letters $a, a', ...$ and B a codomain whose elements are ranged over by the letters $b, b', ...$. Let $T$ be a predicate over $(A \times B)^*$ i.e. over sequences of pairs in A and B, thought as a set of possible finite approximations of a function from A to B. We use $v$ to range over approximations.

We order $(A \times B)^*$ by set inclusion, which we write $\subseteq$. We overload the notations $\downarrow T$, $\uparrow T$, $\uparrow^+ T$ and $\downarrow^+ T$ to now be with respect to $\subseteq$. In particular, since $v \subseteq v'$ for any $v'$ obtained from $v$ by permutation or duplication, all closures are stable by permutation. We write $v \sim v'$ for $v \subseteq v'$ and $v' \subseteq v$, i.e. for the equivalence of $v$ and $v'$ as finite sets.

Note that we do not prevent that a sequence may contain several occurrences of the same pair $(a, b)$. However, such a sequence shall be equivalent to a sequence without redundancies (this design choice is somewhat arbitrary, we just found it more convenient not to enforce the absence of redundancies).

We write $(a, b) \in v$ to mean that $(a, b)$ is one of the elements of the sequence. For $v \in (A \times B)^*$, we write $dom(v)$ for the set of $a$ such that there is some $b$ such that $(a, b) \in v$. For $\alpha \in A \to B$ and $v \in (A \times B)^*$, we define $v \prec \alpha$ to mean $\alpha(a) = b$ for all $(a, b) \in v$, or more formally for the predicate defined by the following clauses:

$$ \frac{v \prec \alpha \qquad \alpha(a) = b}{\langle\rangle \prec \alpha \qquad v \star (a, b) \prec \alpha} $$

We think of $(A \times B)^*$ as finite approximations of functions from A to B and of predicates over finite approximations as constraints generating an ideal or a filter.

In Table XIII, we generalise the notion of productive over (morally) trees into a coinductive notion of A-B-approximable relative to a valid finite set of approximations, and dually, we generalise the notion of inductively barred from holding on a sequence to holding relative to a finite set of approximations.

### B. Generalised Dependent Choice and Generalised Bar Induction

We state the generalisation of dependent choice and bar induction to non-sequential choices over a non-necessarily countable domain in Table XIV. Called $GDC_{ABT}$ (shortly $GDC_{AB}$ or $GDC$ as schemes) and $GBI_{ABT}$ (shortly $GBI_{AB}$ or $GBI$ as schemes), they are generalisations in the sense that they respectively capture $DC^{productive}$ and $BI^{ind}$ for countable A, where by countable is meant the existence of a bijection between A and $\mathbb{N}$.

To prove it, let us assume without loss of generality that A is $\mathbb{N}$ itself. We say that $v \in (\mathbb{N} \times B)^*$ is sequential whenever either

<table><caption>TABLE XIII
LOGICALLY OPPOSITE DUAL CONCEPTS ON DUAL PREDICATES</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td colspan="2">intensional concepts</td></tr><tr><td>$T$ A-B-approximable from $v$<br>$\nu X \cdot \lambda v.$<br>$$ \begin{pmatrix} v \in \downarrow T \land \\ \forall a \notin dom(v) \\ \exists b (v \star (a, b) \in X) \end{pmatrix} $$</td><td>$T$ inductively A-B-barred from $v$<br>$\mu X \cdot \lambda v.$<br>$$ \begin{pmatrix} v \in \uparrow^+ T \lor \\ \exists a \notin dom(v) \\ \forall b (v \star (a, b) \in X) \end{pmatrix} $$</td></tr><tr><td>$T$ A-B-approximable<br>$T$ A-B-approximable from $\langle\rangle$</td><td>$T$ inductively A-B-barred<br>$T$ inductively A-B-barred from $\langle\rangle$</td></tr><tr><td colspan="2">extensional concepts</td></tr><tr><td>$T$ has an A-B-choice function<br>$\exists \alpha \forall u (u \prec \alpha \Rightarrow u \in T)$</td><td>$T$ is A-B-barred<br>$\forall \alpha \exists u (u \prec \alpha \land u \in T)$</td></tr></tbody></table>

<table><caption>TABLE XIV
DUAL AXIOMS ON DUAL PREDICATES</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td>Generalised Dependent Choice<br>($GDC_{ABT}$)<br>$T$ A-B-approximable $\Rightarrow$<br>$T$ has an A-B-choice function</td><td>Generalised Bar Induction<br>($GBI_{ABT}$)<br>$T$ A-B-barred $\Rightarrow$<br>$T$ inductively A-B-barred</td></tr></tbody></table>

$v$ is empty or $v$ has the form $v' \star (|v'|, b)$ with $v'$ itself sequential. To each $u \in B^*$ we can associate a sequential element $ord(u)$ by $ord(\langle\rangle) \triangleq \langle\rangle$ and $ord(u \star b) \triangleq ord(u) \star (|u|, b)$.

To each $T$ over $(\mathbb{N} \times B)^*$, we can associate $||T||$ on $B^*$ by $u \in ||T|| \triangleq ord(u) \in T$. Conversely, to each $T$ over $B^*$, we can associate $\hat{T}$ on $(\mathbb{N} \times B)^*$ defined by $v \in \hat{T} \triangleq \exists u \in T (v = ord(u))$. We have an easy property:

**Proposition 11:** Let $T$ a predicate over $B^*$. If $T$ is closed under restriction, $u \in T$ iff $u \in ||\uparrow^+ \hat{T}||$. If $T$ is closed under extension, $u \in T$ iff $u \in ||\uparrow^+ \hat{T}||$. $\square$

**Proposition 12:** For $T$ over $(\mathbb{N} \times B)^*$ and closed under restriction, $T$ is $\mathbb{N}$-B-approximable iff $||T||$ is productive, and, for $T$ over $B^*$ and closed under restriction, $\uparrow^+ \hat{T}$ is $\mathbb{N}$-B-approximable iff $T$ is productive. Dually, for $T$ closed under extension in both cases, $T$ is inductively $\mathbb{N}$-B-barred iff $||T||$ is inductively barred, and, $\uparrow^+ \hat{T}$ is inductively $\mathbb{N}$-B-barred iff $T$ is inductively barred.

**PROOF:** By duality and Prop. 11, it is enough to prove the first item. The proof is by coinduction in both directions.

From left to right, we prove $T$ $\mathbb{N}$-B-approximable from $ord(u)$ implies $||T||$ productive from $u$. We take $|u|$ for $a$ in the definition of $\mathbb{N}$-B-approximable from $ord(u)$, get some $b$ and pass it to the definition of $||T||$ productive from $u$.

From right to left, we prove more generally that if $||T||$ is productive from $u$ then $T$ is $\mathbb{N}$-B-approximable from $v$ for all $v \subseteq ord(u)$. By definition of $u \in ||T||$, we have $ord(u) \in T$ and thus $v \in \downarrow T$ by closure of $T$. Now, take $n \notin dom(v)$. If $n < |u|$, we set $b$ to be $u(n)$ and apply the coinduction hypothesis with $v$ extended with $b$, which still satisfies $v \star b \subseteq ord(u)$ by
a combinatorial argument. If $n \ge |u|$, we explore the proof of productivity of $||T||$ one step further, getting some $b$ such that $u \star b \in ||T||$ and $||T||$ is productive from $u \star b$. The property $v \subseteq \text{ord}(u \star b)$ continues to hold and we reason by induction on $n - |u|$ until falling into the first case. ■

Similarly, we have:

**Proposition 13:** For $T$ closed under restriction in both cases, $T$ has an $\mathbb{N}$-$B$-choice function iff $||T||$ has an infinite branch, and, $\uparrow \hat{T}$ has a $\mathbb{N}$-$B$-choice function iff $T$ has an infinite branch. Dually, for $T$ closed under extension in both cases, $T$ is $\mathbb{N}$-$B$-barred iff $||T||$ is barred, and, $\uparrow^+ \hat{T}$ is $\mathbb{N}$-$B$-barred iff $T$ is barred. PROOF: By duality and Prop. 11, it is enough to prove the first item. From left to right, if $u \prec_s \alpha$, it is enough to consider $\text{ord}(u) \prec \alpha$. From right to left, if $v \prec \alpha$, we consider $u \triangleq \alpha|_n$, i.e. the initial prefix of length $n$ of $\alpha$, where $n$ is $|v|$. We have $u \prec_s \alpha$ thus $u \in ||T||$ and $\text{ord}(u) \in T$. Since $v \subseteq \text{ord}(u)$, we get $v \in T$ by closure of $T$. ■

Consequently, we have:

**Theorem 5:** $\text{DC}_{\text{BT}}^{\text{productive}}$ iff $\text{GDC}_{\text{NBT}}$ and $\text{BI}_{\text{BT}}^{\text{ind}}$ iff $\text{GBI}_{\text{NBT}}$. PROOF: We mediate by the property that $\text{GDC}_{\text{NBT}}$ is equivalent as a scheme to its restriction to predicates $T$ closed under restriction. Indeed, it is enough to reason with $\downarrow^- T$ knowing that $\downarrow^- T \subseteq T$ and that $\downarrow^- T$ is the identity on predicates closed under restriction. The other equivalence holds by duality. ■

Now, in combination with Prop. 6 and 7 and Th. 1, we get:

**Theorem 6:** As schemes, generalised over $T$, for $B$ non-empty finite, $\text{GDC}_{\text{NBT}}$ is equivalent to $\text{KL}_{\text{BT}}^{\text{spread}}$ and $\text{KL}_{\text{BT}}^{\text{productive}}$, and, in co-intuitionistic and classical logic, equivalent also to $\text{KL}_{\text{BT}}^{\text{unbounded}}$ and $\text{KL}_{\text{BT}}^{\text{staged}}$. Dually, as schemes, $\text{GBI}_{\text{NBT}}$ is equivalent to $\text{FT}_{\text{BT}}^{\text{barricaded}}$ and $\text{FT}_{\text{BT}}^{\text{ind}}$, and, in intuitionistic and classical logic, equivalent also to $\text{FT}_{\text{BT}}^{\text{uniform}}$ and $\text{FT}_{\text{BT}}^{\text{staged}}$. □

### C. Inconsistency of the unconstrained form of Generalised Dependent Choice and Generalised Bar Induction

In its full generality, the generalisation of $\text{GDC}$ and $\text{GBI}$ obtained by allowing non-countable branchings over an arbitrary codomain $B$ is inconsistent: for large enough $A$ and $B$, it may happen that some $T$ is coinductively $A$-$B$-approximable without $T$ having a (full) $A$-$B$-choice function. Indeed, take $A \triangleq \mathbb{B}^N$ and $B \triangleq \mathbb{N}$ and filter the choice function so that it is injective. That is, we define $u \in T$ as follows: if $u$ contains $(f, n)$ and $(f', n)$ then $f$ and $f'$ are extensionally equal.

Then, $T$ is coinductively $\mathbb{B}^N$-$\mathbb{N}$-approximable by successively extending $u$ with $(f, |u|)$ for any $f$ not already in $\text{dom}(u)$. But there is no total choice function $\alpha$ from $\mathbb{B}^N$ to $\mathbb{N}$, since, by Cantor's theorem, such a function is necessarily non-injective. Thus, taking $f$ and $f'$ distinct such that $n \triangleq \alpha(f) = \alpha(f')$, we get that the sequence $(f, n), (f', n) \prec \alpha$ is not in $T$.

Therefore, we have:

**Proposition 14:** As schemes, $\text{GDC}_{\mathbb{B}^N\text{NT}}$ and $\text{GBI}_{\mathbb{B}^N\text{NT}}$ are inconsistent.

### D. Relation to the general axiom of choice

We state the standard axiom of choice in Table XVI and prove that it is equivalent to an instance of the generalised dependent

<table><caption>TABLE XV
LOGICALLY OPPOSITE DUAL CONCEPTS ON DUAL HOMOGENEOUS RELATIONS</caption><thead><tr><th>ill-foundedness style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td colspan="2">intensional concepts</td></tr><tr><td>positive alignment of R (R<sub>⊥</sub>)<br>λv. ∀(a, b) ∈ v (R(a, b))</td><td>negative alignment of R (R<sub>⊥</sub>)<br>λv. ∃(a, b) ∈ v (R(a, b))</td></tr></tbody></table>

<table><caption>TABLE XVI
THE AXIOM OF CHOICE AND ITS DUAL</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td>Standard Axiom of Choice (AC<sub>ABR</sub>)<br>R A-B-left-total ⇒<br>R has an A-B-choice function</td><td>Dual to Standard Axiom of Choice (CO-AC<sub>ABR</sub>)<br>R A-B-barred ⇒<br>R A-B-ground</td></tr></tbody></table>

choice $\text{GDC}$. To do so, we generalise in Table XV the notion of sequential alignment introduced in Section II-I to the notion of (non-sequential) alignment of a relation on $A \times B$ as a predicate over $(A \times B)^*$.

**Theorem 7:** $AC_{ABR}$ is logically equivalent to $\text{GDC}_{ABR_\top}$

PROOF: The proof is a variant of the one of Th. 4. For instance, the correspondence between $R$ A-B-left-total and $R_\top$ A-B-approximable is by coinduction from left to right, calling left-totality at each step, and, from right to left, for any $a$, by using A-B-approximability from $\langle\rangle$ to get $b$ such that $R(a, b)$. ■

## IV. THE BOOLEAN INSTANCES OF GENERALISED DEPENDENT CHOICE AND BAR INDUCTION: RELATION TO THE BOOLEAN PRIME IDEAL/FILTER THEOREM AND COMPLETENESS THEOREMS

### A. Generalised Weak König Lemma and Generalised Weak Fan Theorem

By instantiating the codomain $B$ to $\mathbb{B}$ in $\text{GDC}_{ABT}$ and $\text{GBI}_{ABT}$, we obtain extensions $\text{GBI}_{ABT}$ of the Weak Fan Theorem (precisely of $\text{FT}_{\text{BT}}^{\text{ind}}$, i.e. $\text{GBI}_{\text{NBT}}^{\text{ind}}$ by Th. 6) and $\text{GDC}_{ABT}$ of the Weak König Lemma (precisely of $\text{KL}_{\text{BT}}^{\text{productive}}$, i.e. $\text{GDC}_{\text{NBT}}^{\text{productive}}$ by Th. 6) which replace the countable sequence of branching made on a “tree” (in practise predicates) by a countable sequence of choices in arbitrary order over a non-necessarily countable domain. This will be proved equivalent to a version of the Boolean Prime Ideal/Filter Theorem where primality is formulated positively and to versions of the completeness theorem for entailment relations. This is consistent with the standard reverse mathematics results which show that the completeness theorem is equivalent to the Weak König's Lemma on countable theories [29] but equivalent to the Boolean Prime Filter Theorem on theories of arbitrary cardinality [14], [27], [20], [11].
<table><caption>TABLE XVII
DUAL AXIOMS ON DUAL PREDICATES</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td>Generalised Weak König's Lemma (GDC<sub>ABT</sub>)<br>T A-B-approximable ⇒<br>T has an A-B-choice function</td><td>Generalised Weak Fan Theorem (GBI<sub>ABT</sub>)<br>T A-B-barred ⇒<br>T inductively A-B-barred</td></tr></tbody></table>

## B. Logical reading: relation to completeness theorem

We can give a logical reading to $(A \times \mathbb{B})^*$ as follows. We call *atom* any element of $A$. We interpret pairs in $A \times \mathbb{B}$ as *literals*, i.e. as atoms together with a polarity indicating whether the atom is positive or negative (we adopt the convention that 1 stands for positive and 0 for negative). We call *clause* any unordered sequence of elements in $A \times \mathbb{B}$. We call *context* any unordered sequence of elements of $A$. We range over clauses by the letters $C, D$ and over contexts by the letters $\Gamma, \Delta, ...$

Any clause $C$ can canonically be represented as a pair of two contexts $\Gamma$ and $\Delta$ with $\Gamma$ the subset of positive elements of $A$ in $C$ and $\Delta$ the subset of negative elements. We write $\Gamma \triangleright \Delta$ for such a pair. We call a set of clauses a *theory* and use the letter $\mathcal{T}$ to range over theories. We write $(\Gamma \triangleright \Delta) \in \mathcal{T}$ to mean that there is a clause of $\mathcal{T}$ associated to the pair $\Gamma \triangleright \Delta$. We write $\Gamma \nparallel \Delta$ to mean that $\Gamma$ and $\Delta$ have an atom in common.

We consider (a variant of) Scott's notion of entailment relation [28], i.e. of a preorder relation up to “side contexts”. Let $\mathcal{T}$ be a theory on $A$. We define the *entailment relation* generated by $\mathcal{T}$ to be the smallest relation on sequents, written $\Gamma \vdash_T \Delta$, with $\Gamma$ and $\Delta$ treated as sets, such that the following holds:

$$ \frac{\Gamma \nparallel \Delta}{\Gamma \vdash_T \Delta} \quad \frac{(\Gamma \triangleright \Delta) \in \Gamma^+ \mathcal{T}}{\Gamma \vdash_T \Delta} \quad \frac{\Gamma \vdash_T \Delta, F}{\Gamma \vdash_T \Delta} \quad \frac{F, \Gamma \vdash_T \Delta}{\Gamma \vdash_T \Delta} \quad \text{Cut} $$

It is usual to add an explicit weakening rule to the definition of entailment relation but here we shall consider it as an admissible rule. Formally, the existence of a derivation of $\Gamma \vdash_T \Delta$ using the inferences rules above is the same as

$$ \vdash_T \triangleq \mu X.\lambda(\Gamma \triangleright \Delta). \left( \begin{array}{l} (\Gamma \triangleright \Delta) \in \Gamma^+ \mathcal{T} \\ \lor \exists F \notin (\Gamma \cup \Delta) \left( (\Gamma, F \triangleright \Delta) \in X \\ \land (\Gamma \triangleright \Delta, F) \in X \end{array} \right) \end{array} \right) $$

Thus, $\Gamma \vdash_T \Delta$ exactly says that $\mathcal{T}$ is inductively A-B-barred from $\Gamma \triangleright \Delta$.

Conversely, let us consider $\Gamma \nparallel_T \Delta$. We could define it by negation of $\Gamma \vdash_T \Delta$ but we instead give a direct explicit definition which we call *positive disprovability* and which is equivalent to the negation of $\Gamma \vdash_T \Delta$ when the connectives are read linearly or classically (though not equivalent when read intuitionistically). Let $\mathcal{T}^C$ denote the complement of $\mathcal{T}$, i.e. $(\Gamma \triangleright \Delta) \in \mathcal{T}^C \triangleq \neg((\Gamma \triangleright \Delta) \in \mathcal{T})$. The positive disprovability $\Gamma \nparallel_C \Delta$ can be characterised as the $\mathcal{T}^C$ A-B-approximability from $\Gamma \triangleright \Delta$, that is, formally:

$$ (\Gamma \triangleright \Delta) \in \nu X.\lambda(\Gamma \triangleright \Delta). \left( \begin{array}{l} (\Gamma \triangleright \Delta) \in \Gamma^+ \mathcal{T}^C \\ \lor \forall F \notin (\Gamma \cup \Delta) \left( (\Gamma, F \triangleright \Delta) \in X \\ \lor (\Gamma \triangleright \Delta, F) \in X \end{array} \right) \end{array} \right) $$

<table><caption>TABLE XVIII
LOGICALLY OPPOSITE DUAL CONCEPTS OF LOGIC ON THE SAME PREDICATE</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td colspan="2">intensional concepts</td></tr><tr><td>$\mathcal{T}$ is (positively) consistent</td><td>$\mathcal{T}$ is inconsistent</td></tr><tr><td>$\nparallel_T$</td><td>$\vdash_T$</td></tr><tr><td colspan="2">extensional concepts</td></tr><tr><td>$\mathcal{T}$ is satisfiable<br>$\exists \alpha \alpha \nvDash \mathcal{T}$</td><td>$\mathcal{T}$ is (positively) unsatisfiable<br>$\forall \alpha \alpha \nparallel \mathcal{T}$</td></tr></tbody></table>

<table><caption>TABLE XIX
REFORMULATION OF TABLE XVII AS STATEMENTS ABOUT A GIVEN LOGICAL THEORY</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td>Model-existence-style Completeness<br>Theorem (Compl<sup>-</sup><sub>A</sub>(T))<br>$\mathcal{T}$ consistent ⇒ $\mathcal{T}$ is satisfiable</td><td>Provability-style Completeness<br>Theorem (Compl<sup>+</sup><sub>A</sub>(T))<br>$\mathcal{T}$ unsatisfiable ⇒ $\mathcal{T}$ inconsistent</td></tr></tbody></table>

Let $\alpha$ be a function from $A$ to $\mathbb{B}$. It can be interpreted as a model over $A$ with 1 to indicate that the atom is true in the model and 0 to indicate that the atom is false in the model.

Truth $\alpha \nvDash \mathcal{T}$ of a theory $\mathcal{T}$ in a model $\alpha$ can be defined by

$$ \alpha \nvDash \mathcal{T} \triangleq \forall (\Gamma \triangleright \Delta) \in \mathcal{T} (\Gamma \subset \alpha \Rightarrow \Delta \nparallel \alpha) $$

where we use the notation $\Gamma \subset \alpha$ to mean that $\forall a \in \Gamma \alpha(a) = 1$ and the notation $\Delta \nparallel \alpha$ to mean $\neg \forall a \in \Delta \alpha(a) = 0$. Then, $\mathcal{T}$ is satisfiable (or has a model) if there exists $\alpha$ such that $\alpha \nvDash \mathcal{T}$.

Like for disprovability, the negation of truth can be defined explicitly rather than by negation in a way which is equivalent when the connectives are read linearly or classically (but not intuitionistically). Let us define *positive falsity* of a theory $\mathcal{T}$ in a model $\alpha$, written $\alpha \nparallel \mathcal{T}$, by the following formula:

$$ \alpha \nparallel \mathcal{T} \triangleq \exists (\Gamma \triangleright \Delta) \in \mathcal{T} (\Gamma \subset \alpha \land \Delta \subset \bar{\alpha}) $$

where $\Delta \subset \bar{\alpha}$ stands for $\forall a \in \Delta \alpha(a) = 0$. We say that the theory $\mathcal{T}$ is positively unsatisfiable if, for all $\alpha$, $\alpha \nparallel \mathcal{T}$.

Then, still identifying clauses in $\mathcal{T}$ as sequences in $(A \times \mathbb{B})^*$, we get that $\mathcal{T}$ A-B-barred corresponds to the positive unsatisfiability of $\mathcal{T}$. Also, noticing that $\exists \alpha \forall u (u \prec \alpha \Rightarrow u \in \mathcal{T}^C)$ is isomorphic to $\exists \alpha \forall u (u \in \mathcal{T} \Rightarrow \neg u \prec \alpha)$ and that $\neg u \prec \alpha$ is isomorphic to $\Gamma \subset \alpha \Rightarrow \Delta \nparallel \alpha$, we get that $\mathcal{T}^C$ has an A-B-choice function if and only if there exists a model for $\mathcal{T}$ (see Table XVIII where $\vdash_T$ and $\nparallel_T$ refer to the provability and positive disprovability of the empty clause).

The completeness theorem of logic is conventionally expressed either as the existence of a model for any consistent theory, or contrapositively, that if a theory is unsatisfied in all theories, then it is inconsistent, as shown on Table XIX. For instance, see Rinaldi, Schuster and Wessel [26] for the statement of a completeness theorem such as $\text{Compl}^+(\mathcal{T})$, up to the identification of some $\exists$ with $\neg\neg\exists$. See also e.g. [25] for an algebraic reading. Summing up, we have:
**Theorem 8:** Let $\mathcal{T}$ be a theory of clauses over some set of atoms $A$, with clauses represented as sequences in $(A \times \mathbb{B})^*$. The Generalised Weak König's Lemma over the complement $\mathcal{T}^C$ of $\mathcal{T}$, i.e. $\text{GDC}_{A\mathcal{B}\mathcal{T}^C}$, coincides with the model-existence formulation of completeness for the Scott entailment relation generated by $\mathcal{T}$, i.e. $\text{Compl}_A^-(\mathcal{T})$. Contrapositively, the Generalised Weak Fan Theorem over $\mathcal{T}$, i.e. $\text{GBI}_{A\mathcal{B}\mathcal{T}}$, coincides with the provability-style formulation of completeness for the Scott entailment relation generated by $\mathcal{T}$, i.e. $\text{Compl}_A^+(\mathcal{T})$. Record that, to preserve the duality, $\text{Compl}_A^-(\mathcal{T})$ relies on an explicit definition of $\Gamma \vdash_T \Delta$ which is linearly (and classically) equivalent to but intuitionistically stronger than the negation of $\Gamma \vdash_T \Delta$, and $\text{Compl}_A^+(\mathcal{T})$ relies on an explicit definition of $\alpha \not\vdash_T \mathcal{T}$ which is linearly (and classically) equivalent to but intuitionistically stronger than the negation of $\alpha \vdash_T \mathcal{T}$. $\square$

Note incidentally that entailment relations are connective-free. The usual reliance on Markov's principle to intuitionistically prove completeness as validity implies provability [22] does not apply (see e.g. [15], [12] for recent studies).

### C. Algebraic reading: relation to the Boolean Prime Ideal/Filter Theorem

The previous reasoning based on entailment relations can also be expressed in terms of Boolean algebras, connecting Generalised Weak König's Lemma to the Boolean Prime Ideal/Filter Theorem. There is however a caveat: the standard definition of proper filter and proper ideal is by negation and it will be equivalent to approximability only with a linear or classical, i.e. involutive, reading of the negation.

Let $(\mathcal{B}, \dot{\nu}, \dot{\lambda}, \dot{\perp}, \dot{\tau}, \dot{\wedge})$ be a Boolean algebra and $\dot{\vdash}$ the canonical order relation associated to it: $b \vdash b' \triangleq (b \dot{\wedge} b') = b$. We call filter over $\mathcal{B}$ any non-empty subset $F$ of $\mathcal{B}$ which is closed under $\dot{\lambda}$ and closed under $\dot{\vdash}$ on the right. A filter is proper if it does not contain $\dot{\perp}$. Otherwise, it coincides with $\mathcal{B}$ and we call it full. We call ultrafilter a maximal proper filter. A maximal filter in a Boolean algebra can be described as a map $U$ from $\mathcal{B}$ to $\mathcal{B}$ such that $b_1 \dot{\wedge} b_2 \in U$ iff $b_1 \in U \wedge b_2 \in U$, $b_1 \dot{\vee} b_2 \in U$ iff $b_1 \in U \vee b_2 \in U$, $\dot{\wedge} b \in U$ iff $\neg(b \in U)$, $\dot{\tau} \in U$, and $\dot{\perp} \notin U$. In a Boolean algebra, the notion of maximal filter coincides with the notion of prime filter where a filter $F$ is prime if $(b_1 \dot{\vee} b_2) \in F$ implies $b_1 \in F$ or $b_2 \in F$.

Dually, we call ideal over $\mathcal{B}$ any non-empty subset $I$ of $\mathcal{B}$ which is closed under $\dot{\nu}$ and closed under $\dot{\vdash}$ on the left. An ideal is proper if it does not contain $\dot{\tau}$, and full otherwise. A prime ideal $I$ is such that $(b_1 \dot{\wedge} b_2) \in I$ implies $b_1 \in I$ or $b_2 \in I$ and this coincides with the notion of maximal proper ideal. A prime/maximal proper ideal can be characterised in a dual way to prime/maximal proper filter, i.e. as a map $U$ from $\mathcal{B}$ to $\mathcal{B}$ such that $b_1 \dot{\wedge} b_2 \in U$ iff $b_1 \in U \vee b_2 \in U$, $b_1 \dot{\vee} b_2 \in U$ iff $b_1 \in U \wedge b_2 \in U$, $\dot{\wedge} b \in U$ iff $\neg(b \in U)$, $\dot{\perp} \in U$ and $\dot{\tau} \notin U$.

There is a family of provably equivalent theorems about the existence of maximal/prime ideals/filters in Boolean algebras (see e.g. Jech [20, 2.3]) called Boolean Prime Ideal Theorem in arbitrary Boolean algebras, or Ultrafilter Theorem in the Boolean algebra of subsets of a set. We consider in Table XX

<table><caption>TABLE XX
REFORMULATION OF TABLE XVII AS STATEMENTS ABOUT A GIVEN
BOOLEAN ALGEBRA</caption><thead><tr><th>ill-foundedness-style</th><th>well-foundedness-style</th></tr></thead><tbody><tr><td>Boolean Prime Filter Theorem<br>(BPF<sub>B</sub>(F) for F a filter)</td><td>"Boolean Full Filter Theorem"<br>(co-BPF<sub>B</sub>(F) for F a filter)</td></tr><tr><td>F proper ⇒<br>F extensible into prime filter</td><td>F not extensible into prime filter ⇒<br>F full</td></tr><tr><td>Boolean Prime Ideal Theorem<br>(BPI<sub>B</sub>(I) for I an ideal)</td><td>"Boolean Full Ideal Theorem"<br>(co-BPI<sub>B</sub>(I) for I an ideal)</td></tr><tr><td>I proper ⇒<br>I extensible into prime ideal</td><td>I not extensible into prime ideal ⇒<br>I full</td></tr></tbody></table>

the case of a general Boolean algebra and state the Boolean Prime Ideal Theorem in its two “ideal” and “filter” flavours. We also consider their contrapositives.

We now compare the Boolean Prime Ideal/Filter Theorems to Generalised Weak König's Lemma, i.e. $\text{GDC}_{A\mathcal{B}\mathcal{T}}$, showing first that the Generalised Weak König's Lemma is an instance of the Boolean Prime Ideal and Boolean Prime Filter Theorems.

To any domain $A$ we can associate a freely generated Boolean algebra (Free$(A)$, $\dot{\nu}$, $\dot{\lambda}$, $\dot{\perp}$, $\dot{\tau}$, $\dot{\wedge}$) by considering the set of algebraic expressions built from $\dot{\nu}$, $\dot{\lambda}$, $\dot{\perp}$, $\dot{\tau}$ and $\dot{\wedge}$, all quotiented by the axioms of a Boolean algebra.

As in the previous section, any $v$ in $(A \times \mathbb{B})^*$, can be written under the form $\Gamma \triangleright \Delta$ and a predicate over $(A \times \mathbb{B})^*$ can be seen as a theory $\mathcal{T}$ of clauses. Let $\vdash_T$ be the associated entailment relation and $F_T$ be the (equivalence classes of) Boolean expressions of the form $\dot{\lambda}_i ((\dot{\nu} \dot{\wedge} \Gamma_i) \dot{\nu} (\dot{\nu} \Delta_i))$ such that $\Gamma_i \vdash_T \Delta_i$ holds for all $i$ (this can be shown independent of the exact choice of conjunctive normal form). It is relatively standard to show that $F_T$ is a filter. This filter is proper if $\perp \notin F_T$, that is if $\neg(\vdash_T)$, that is if $\mathcal{T}$ is not inconsistent, that is, by Section IV-B, if $\mathcal{T}^C$ is $A$-B-approximable, where the connectives are interpreted either linearly or classically.

We can dually define $I_T$ to be the (equivalence classes of) Boolean expressions of the form $\dot{\nu}_i ((\dot{\lambda} \Gamma_i) \dot{\lambda} (\dot{\lambda} \Delta_i))$ such that $\Gamma_i \vdash_T \Delta_i$ holds for all $i$. This is an ideal which is proper if $\tau \notin I_T$, that is if $\neg(\vdash_T)$, that is if $\mathcal{T}^C$ is A-B-approximable where, again, the connectives are interpreted either linearly or classically.

Reasoning by induction on the definition of $\vdash_T$ and relying on the definition of $(\Gamma \triangleright \Delta) \prec \alpha$, we have the general result that prime filters and prime ideals on a free Boolean algebra, here Free$(A)$, are characterised by their intersection with generators, here $A$. Whether other elements of Free$(A)$ belong or not to a prime filter or prime ideal is canonically determined<fnref n="9" /> by:

$$ \begin{align*} \alpha(a \dot{\nu} a') &= b'' &\triangleq \quad (\alpha(a) &= b) \wedge (\alpha(a') &= b') \wedge (b'' &= b + b') \\ \alpha(a \dot{\wedge} a') &= b'' &\triangleq \quad (\alpha(a) &= b) \wedge (\alpha(a') &= b') \wedge (b'' &= b \cdot b') \\ \alpha(\dot{\perp}) &= b &\triangleq \quad b &= 0 \\ \alpha(\dot{\tau}) &= b &\triangleq \quad b &= 1 \\ \alpha(\dot{\wedge} a) &= b' &\triangleq \quad (\alpha(a) &= b) \wedge (b' &= 1 - b) \end{align*} $$

<footnote n="9">⁹We define the value of $\alpha$ as equations to remain agnostic on the representation of a function to $\mathbb{B}$, see II-B.</footnote>
where + , -, are the corresponding operations on $\mathbb{B}$, and where the prime filter case is characterised by $\alpha(b) = 1$ and the prime ideal case by $\alpha(b) = 0$.

In particular, the existence of a function from $A$ to $\mathbb{B}$ characterising a prime filter that extends the filter $F_\tau$ on $\text{Free}(A)$ is the same, by Section IV-B, as a model of $\mathcal{T}$ and as an $A$-$\mathbb{B}$-choice function for $\mathcal{T}^C$. By focusing on $\alpha(b) = 0$ rather than $\alpha(b) = 1$, this very same function also characterises the prime ideal that extends the ideal $I_\tau$, so, we get:

**Theorem 9:** $\mathbf{GDC}_{\mathbb{A}\mathbb{B}\mathcal{T}^C}$, where the connectives are interpreted linearly or classically, is equivalent to $\mathbf{BPF}_{\text{Free}(A)}(F_\tau)$ and $\mathbf{BPI}_{\text{Free}(A)}(I_\tau)$. $\square$

Conversely, if $F$ is a filter on a Boolean algebra $\mathcal{B}$, we can define $\mathcal{T}_F$ on $(\mathcal{B} \times \mathcal{B})^*$ by $(\Gamma \triangleright \Delta) \in \mathcal{T}_F \triangleq (\mathcal{V}^{\frown} \Gamma) \mathcal{V}^{\frown} (\mathcal{V} \Delta) \in F$. By induction on a proof of $\Gamma \vdash_\tau \Delta$ we can show that it implies $(\mathcal{V}^{\frown} \Gamma) \mathcal{V}^{\frown} (\mathcal{V} \Delta) \in F$ thus $\Gamma \vdash_\tau \Delta$ iff $(\mathcal{V}^{\frown} \Gamma) \mathcal{V}^{\frown} (\mathcal{V} \Delta) \in F$. Therefore, $F$ proper becomes equivalent to $\mathcal{T}_F$ $A$-$\mathbb{B}$-approximable where the connectives are interpreted either linearly or classically. Reasoning as above, this eventually allow to reduce $\mathbf{BPF}_B(F)$ to $\mathbf{GDC}_{\mathbb{B}\mathbb{B}\mathcal{T}_F}$ and to show the equivalence of $\mathbf{GDC}_{\mathbb{A}\mathbb{B}\mathcal{T}}$ and $\mathbf{BPF}_B(F)$ as schemes. Then, a similar analysis can put $\mathbf{GBI}_{\mathbb{A}\mathbb{B}\mathcal{T}}$ into correspondence with co-$\mathbf{BPF}_B(F)$ and co-$\mathbf{BPI}_B(I)$.

More generally, we also believe that, like in the countable case, $\mathbf{GDC}_{ABT}$ and $\mathbf{GDC}_{ABT}$ over any finite, non-necessarily two-element, codomain $B$ can be reduced to $\mathbf{GDC}_{ABT}$ and $\mathbf{GDC}_{ABT}$.

V. FURTHER QUESTIONS

The duality revealed that when a proof requires classical reasoning and its dual does not, it is that it requires co-intuitionistic reasoning and its dual intuitionistic reasoning. As a conclusion, to the notable exception of Proposition 6, we believe that all proofs could be carried out in a linear variant of higher-order arithmetic.

There is a rich literature on choice axioms and on principles equivalent to choice axioms. Not all of them can be classified as either ill- or barred/well-foundedness-style, though. For instance, open induction and update induction [24], [8], [6], are classically equivalent to bar induction and dependent choice but are formulated as well-foundedness of some order on functions. The study could also for instance be extended to choice principles such as Zorn's lemma, the ordinal variants of the axiom of dependent choices by Lévy [23] and the ordinal variants of Zorn's lemma [31] by Wolk.

ACKNOWLEDGMENTS

We thank the communities of researchers who contributed to develop the material we built on, and in particular Camille Noûs, from the Cogitamus Lab, who embodies the collective and collaborative nature of scientific research.

The ideas in Section IV-C derived from investigations led by Charlotte Barot [1]. The second author thanks Valentin Blot and Étienne Miquey for numerous fruitful discussions on the axiom of dependent choice and bar induction. Special thanks also to the reviewers for their corrections and insightful suggestions.

REFERENCES

[1] Charlotte Barot. *Two [choice] principles involved in the intuitionistic completeness theorem*. Master thesis, University Paris-Diderot, 2017.

[2] Josef Berger. The Fan Theorem and Uniform Continuity. In *Proceedings CiE 2005*, page 18–22. Springer-Verlag, 2005.

[3] Josef Berger. A decomposition of Brouwer's fan theorem. *J. Logic & Analysis*, 1, 2009.

[4] Josef Berger and Hajime Ishihara. Brouwer's fan theorem and unique existence in constructive analysis. *Mathematical Logic Quarterly*, 51(4):360–364, 2005.

[5] Josef Berger, Hajime Ishihara, and Peter Schuster. The Weak König Lemma, Brouwer's Fan Theorem, De Morgan's Law, and Dependent Choice. *Reports on Mathematical Logic*, 47, 2012.

[6] Ulrich Berger. A computational interpretation of open induction. In *LICS 2004, Proceedings*, page 326. IEEE Computer Society, 2004.

[7] Crystal Cheung. *Brouwer's Fan Theorem: An Overview*. Master thesis, Cornell University, 2015.

[8] Thierry Coquand. A note on the open induction principle. *Chalmers University*, 1997.

[9] Thierry Coquand. About Brouwer's Fan Theorem. *Revue Internationale de Philosophie*, 230:483–489, 2004.

[10] Thierry Coquand and Henri Lombardi. A logical approach to abstract algebra. *Mathematical Structures in Computer Science*, 16(5):885–900, 2006.

[11] Christian Espíndola. Semantic completeness of first-order theories in constructive reverse mathematics. *Notre Dame J. Formal Logic*, 57(2):281–286, 2016.

[12] Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness theorems for first-order logic analysed in constructive type theory: Extended version. *Journal of Logic and Computation*, 31(1):112–151, 01 2021.

[13] Jean-Yves Girard. Linear logic. *Theor. Comput. Sci.*, 50:1–102, 1987.

[14] Leon Henkin. The completeness of the first-order functional calculus. *J. Symb. Log.*, 14(3):159–166, 1949.

[15] Hugo Herbelin and Danko Ilik. An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem. *Manuscript available online*, 2016.

[16] William A. Howard and Georg Kreisel. Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. *J. Symb. Log.*, 31(3):325–358, 1966.

[17] Hajime Ishihara. An omniscience principle, the König lemma and the Hahn-Banach theorem. *Mathematical Logic Quarterly*, 36(3):237–240, 1990.

[18] Hajime Ishihara. Constructive reverse mathematics: Compactness properties. *From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics*, 48, 10 2005.

[19] Hajime Ishihara. Weak König's Lemma Implies Brouwer's Fan Theorem: A Direct Proof. *Notre Dame J. Formal Logic*, 47(2):249–252, 04 2006.

[20] Thomas J. Jech. *The Axiom of Choice*. Dover Books on Mathematics Series. Courier corporation, 1973.

[21] Stephen Kleene and Richard E. Vesley. *The foundations of intuitionistic mathematics*. North-Holland, 1965.

[22] Georg Kreisel. Elementary completeness properties of intuitionistic logic with a note on negations of prenex formulae. *Journal of Symbolic Logic*, 23(3):317–330, 1958.

[23] Azriel Lévy. The interdependence of certain consequences of the axiom of choice. *Fundamenta Mathematicae*, 54(2):135–157, 1964.

[24] Jean-Claude Raoult. Proving open properties by induction. *Information Processing Letters*, 29(1):19–23, 1988.

[25] Davide Rinaldi and Peter Schuster. A universal Krull-Lindenbaum theorem. *Journal of Pure and Applied Algebra*, 220(9):3207–3232, 2016.

[26] Davide Rinaldi, Peter Schuster, and Daniel Wessel. Eliminating disjunctions by disjunction elimination. *The Bulletin of Symbolic Logic*, 23(2):181–200, 2017.

[27] Herman Rubin and Jean E. Rubin. *Equivalents of the Axiom of Choice*. Elsevier, 1963.

[28] Dana Scott. Completeness and axiomatizability. In *Proceedings of the Tarski symposium*, pages 411–435, 1974.

[29] Stephen G. Simpson. *Subsystems of Second Order Arithmetic*. Perspectives in Logic. Cambridge University Press, 2nd edition, 2009.

[30] Wim Veldman. Brouwer's Fan Theorem as an axiom and as a contrast to Kleene's alternative. *Arch. Math. Log.*, 53(5-6):621–693, August 2014.

[31] Elliot S. Wolk. On the principle of dependent choices and some forms of Zorn's lemma. *Canad. Math. Bull.*, 26(3), 1983.