# Constructive Substitutes for König's Lemma

Dominique Larchey-Wendling

► To cite this version:

Dominique Larchey-Wendling. Constructive Substitutes for König's Lemma. 30th International Conference on Types for Proofs and Programs TYPES 2024, Rasmus Ejlers Møgelberg; Patrick Bahr, Jun 2024, Copenhagen, Denmark. pp.2:1-2:23, 10.4230/LIPIcs.TYPES.2024.2 . hal-05142852

HAL Id: hal-05142852

https://hal.science/hal-05142852v1

Submitted on 9 Dec 2025

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.

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

Distributed under a Creative Commons Attribution 4.0 International License
# Constructive Substitutes for König's Lemma

Dominique Larchey-Wendling

Université de Lorraine, CNRS, LORIA, F-54000 Nancy, France

## Abstract

We propose weaker but constructively provable variants of the contrapositive of König's lemma. We derive those from a generalization of the FAN theorem for inductive bars to inductive covers, for which we give a concise proof. We compare the positive, negative and sequential characterizations of covers and bars in classical and constructive contexts, giving precise accounts of the role played by the axioms of excluded middle and dependent choice. As an application, we discuss some examples where the use of König's lemma can be replaced by one of our weaker variants to obtain fully constructive accounts of results or proofs that could otherwise appear as inherently classical.

**2012 ACM Subject Classification** Theory of computation → Type theory; Theory of computation → Constructive mathematics

**Keywords and phrases** König's lemma, FAN theorem, constructive mathematics, inductive covers, inductive bars, almost full relations, inductive type theory, Coq

**Digital Object Identifier** 10.4230/LIPIcs.TYPES.2024.2

**Supplementary Material** Software: https://github.com/DmxLarchey/Constructive-Konig [19] archived at swh:1:dir:611c848b0dbc19c9de20744122776440c00e413d

**Funding** Dominique Larchey-Wendling: partially supported by NARCO (ANR-21-CE48-0011).

## 1 Introduction

König's (infinity) lemma, named after Dénes König, was originally published as a theorem of graph theory [18]. Nowadays, it is usually conflated with the following statement:

> Any infinite tree which is finitely branching has an infinite branch.<fnref n="1" />

The restriction to at most binary trees is of particular importance because it can be stated within lightweight foundations like e.g. $RCA_0$ [26], and is usually called weak König's lemma ($WKL$). Notice that König's lemma is also used in its contrapositive form:

> Any finitely branching tree with only finite branches must be finite.

Classical mathematicians would not mind switching between the two formulations but herein, we refrain from using excluded middle at will, and we adopt a constructivist point of view. In this context, that contrapositive form is sometimes referred to as “Brouwer’s FAN theorem” [5, p. 13]. Although there is no universal agreement on what constitutes constructive mathematics, we use the inductive type theory that is the basis of Coq, free of additional axioms, as our constructive foundations.

König's lemma plays critical roles in various fields of mathematics like logic, computability, tiling theory, etc. and has been investigated by reverse mathematics, e.g. as $WKL_0$ in [26], and constructive reverse mathematics [2, 3]. Although some of our investigations might be relevant to the program of reverse mathematicians, we do not follow that approach. We favor a more pragmatic perspective: since the lemma does not belong to the realm of purely constructive mathematics, can we propose weaker alternatives that could be used, not as drop-in, but rather as low cost replacements for König's lemma? Of course, we require that those alternatives are constructively provable.

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

<footnote n="1">¹ the original statement rather talks about paths in a graph.</footnote>
## 2:2 Constructive Substitutes for König's Lemma

Kőnig's lemma can (in particular) be used to establish the termination of algorithms, and typically has been used for the decision procedure of implicational relevance logic [8, 17]. It is instrumental to show the existence of Harvey Friedman's [11] TREE($n$) monster (extremely fast growing) function, in combination with Kruskal's tree theorem, see e.g. [13] where both proofs rely on classical mathematics. These are two example applications of our tools aimed at giving constructive accounts of what could otherwise look inherently classical.

As simple as it sounds, Kőnig's lemma involves the notion of infinite tree. Hence, the trees cannot simply be understood as the inductively defined structure to be found in computer science (these are always finite). Also, the notion of infinite is not as straightforward in the constructive world. In reverse mathematics, where the usage of versatile data structures may be constrained, a tree is often conflated with its set of finite branches (so finite sequences of nodes where the next node is a son of the current node). As such, trees are nonempty, prefix closed, sets of finite sequences, possibly with a computable membership predicate. And infinite branches are sequences for which every finite prefix belongs to the tree, i.e. the upper limit of a growing sequence of finite branches of the tree.

In that context, one can prove Kőnig's lemma using excluded middle and a weak form of the axiom of choice (e.g. dependent choice). If a canonical choice can be made over the sons, typically when there is a total order that can sort the sons at every node of the tree, the infinite construction process in the proof can be determinized (by choosing the least son) and the reliance on the axiom of choice is avoidable in that case. However, excluded middle is more critical, in particular to show that when the union of finitely many sub-trees is infinite, it must be because one of them is infinite. "Being infinite" is not a decidable property so the selection performed by excluded middle cannot be turned into a computable value.

Kleene [16] famously gave a counterexample to a computational interpretation of weak Kőnig's lemma: he builds a computable infinite binary tree, so a decidable set of finite sequences of Booleans<fnref n="2" /> for which there exists no *computable* infinite branch, i.e. no infinite sequence of Booleans of which every finite prefix belongs to the tree. This gives a very strong argument against the constructive acceptability of Kőnig's lemma, at least when one "interprets Bishop's mathematics in a recursive way" [6]<fnref n="3" />.

Not only Kőnig's lemma could be rejected from a constructivist point of view, but some of its consequences suffer similar defects. Consider the compactness result for Wang tilings:

> A finite set of tiles can tile the plane if and only if it can tile any finite square.

Similarly to Kleene's result, Hanf [14] and Myers [24] famously gave examples of finite sets of tiles that can tile the whole plane, but only in a nonrecursive way. This invalidates a computational understanding of the compactness result. Hence no constructive account of the proof of the compactness result can be given, otherwise it would entail the existence of a recursive tiling.<fnref n="4" />

So there is no real hope at a drop-in constructive replacement for Kőnig's lemma because some of its consequences might live outside the realm of constructive or computable mathematics. Nevertheless, we argue that it might be used in contexts where weaker alternatives would also fit. And it is our aim here to explore some of those alternatives.

For instance, there is an interpretation of its contrapositive form, i.e. "any finitely branching tree with only finite branches must be finite", where the notion of infinity is replaced by finitary notions. Notice that the referred statement still relies on arbitrary (finite or infinite) trees: when saying "only finite branches", one must consider the possibility that it contains infinite branches otherwise this hypothesis is vacuous:

<footnote n="2">² choices between the left or the right son.</footnote>

<footnote n="3">³ as said earlier, the notion of what is constructively acceptable is not universally agreed on.</footnote>

<footnote n="4">⁴ Notice that the tileability of a finite square is a decidable property.</footnote>
- one classical way to understand “only finite branches” is by saying that no infinite sequence can have all its finite prefixes in the tree. Hence even though the statement does not refer to infinity, it is uncovered in this unfolding;

- another way is to understand “only finite branches” is to give an inductive characterization of the well-foundedness of branches with the single rule for the $acc F : rel_1 X$ predicate:

$$ \frac{\forall y, F x y \rightarrow acc F y}{acc F x} \quad [acc\_intro] $$

where $F : rel_2 X$ is a parameter relation. Intuitively, $F x y$ means that $x$ is the father of $y$ in the tree (or $y$ is a son of $x$). If nodes are conflated with finite branches, then $F x y$ means that $y$ has the shape $x \equiv \_[$, i.e. $x$ followed by a single choice of a son.

In that later case, finiteness of the tree branching along $F$ and rooted at $root$ can be defined by $(acc F root)$, and thus understood as the unavoidable termination of the nondeterministic process of expending branches by adding sons after sons, starting from the $root$. Intuitively, the proof of $(acc F root)$ is a well-founded tree where a leaf is decorated with a proof of $(acc F x)$ such that $x$ is childless (i.e. $\forall y, \neg F x y$). In that inductive understanding of “only finite branches,” the contrapositive of Kőnig’s lemma can be established by well founded induction, see e.g. [1, p. 15]. We will derive it as a corollary in Section 5.3.

In intuitionistic frameworks, Brouwer’s FAN theorem is a consequence of the Bar theorem, originally designed to grasp the full continuum in an approach to real analysis [5]. Its acceptability from a constructive standpoint is a delicate issue. It has a rich track record: see e.g. Troelstra [27, 28] for the context of intuitionistic analysis, but there are more recent results, related to convexity [4] or to the exhaustibility of the Cantor space [9]. Intuitionists have compared Kőnig’s lemma with the FAN theorem in various contexts, e.g. [12, 30].

Remember that our aim is not to study the FAN theorem per se, but to propose workable alternatives to the use of Kőnig’s lemma for the conversion of classical proofs to constructive ones. In this context, we may abuse referring to Kőnig’s lemma even though, from a purely intuitionistic standpoint, the results we discuss are closer to the FAN theorem.

However, in contrast with the above cited work on the FAN theorem, we differ in our approach to quantification over the branches of trees. We follow Coquand’s thesis [6] that bar inductive predicates are the correct expression of universal quantification over choice sequences, be they lawlike or lawless; see our discussion in Section 3.5. Hence, we work directly with inductive bars (on finite sequences), avoiding Brouwer’s thesis [29] completely. Actually, we use the more general notion of inductive cover [25] on (transition) relations.

As for our contributions, in Section 3 we show that the notion of inductive cover generalizes both inductive bars and (inductive) accessibility, w.r.t. its definition as well as w.r.t. the results that it entails. We then give a detailed comparison between the constructive and classical strength of three characterizations of covers: positive, negative and sequential. In particular, for the classical part of the comparison, we separate the role played by excluded middle and dependent choice and show the key role played by the intermediate negative characterization. It will also play an important role in a constructive context, as a substitute to the sequential characterization, when used in combination with the FAN theorem.

In Section 4, we give a type theoretic interpretation of the FAN theorem for inductive covers, with a concise proof. The central argument, the stability of upward closed inductive covers under binary union, differs from that of the proof of Fridlender’s FAN theorem for inductive bars [10] which relies on the stability of monotone inductive bars under binary intersection. However, we derive the FAN for bars as an instance of the FAN for covers, to make the generalization explicit.
## 2:4 Constructive Substitutes for König's Lemma

In Section 5, we exploit the FAN for inductive covers, followed by an application of the negative characterization of covers, to give several weaker versions of (the contrapositive of) König's lemma, showing how relations can be represented by rose trees (hence finitary). This includes an extra covering assumption, or an extra bar assumption, or else an extra almost fullness assumption.

In Section 6, we give two examples where König's lemma can successfully be replaced with one of these weaker variants to give constructive accounts of results of which the former proofs were using the classical form of the lemma.

Additionally, we contribute a mechanization of all the results of the paper in a Coq script that can of course be type checked for correctness, but was especially designed to be read by humans, not only by computers. The script is mostly self contained, largely commented, with concise proofs: the longest is 25 loc but most of them are shorter than 10 loc. It is accessible under a free software license at

https://github.com/DmxLarchey/Constructive-Konig

## 2 Coq preliminaries

We denote by $\mathbb{P}$ the type of propositions and simply by **Type** the Coq hierarchy of types, as usual with this framework. We write $\perp : \mathbb{P}$ for the empty proposition and use the standard notations for logical connectives. Recall that the logic of Coq is intuitionistic hence the negation is defined by $\neg P \equiv P \to \perp$. Following the BHK interpretation, $X \to Y$ more generally denotes the type of maps from $X$ to $Y$, and we write $\forall x : X, P x$ for the dependent product, irrelevant of whether $P : X \to \mathbb{P}$ or $P : X \to \mathbf{Type}$. Whenever it can be guessed, the type annotation in $x : X$ is simply avoided. The dependent sum has several flavors in Coq: for $P : X \to \mathbb{P}$ we have the proposition $\exists x, P x : \mathbb{P}$ and the type $\{x | P x\} : \mathbf{Type}$ which behave somewhat similarly but are however fundamentally different because propositions of sort $\mathbb{P}$ cannot systematically be eliminated to build terms of sort $\mathbf{Type}$.

The type of Peano natural numbers $\mathbb{N}$ is inductively defined in Coq as $\mathbb{N} : n \equiv 0 \mid \mathbb{S}n$ and arithmetic in Coq, which we assume, is built on this type. We manipulate finite sequences as lists, polymorphic<fnref n="5" /> over the carrier type $X$, in the inductive type `list X : l \equiv [] | x::l$ where $x : X$. Additionally, list concatenation (resp. membership) is named `app` (resp. `In`), denoted `infix` by $\cdot \mathbf{+} \cdot : list X \to list X \to list X$ (resp. $\cdot \in \cdot : X \to list X \to \mathbb{P}$), and defined by a guarded fixpoint. Moreover, we use the reverse `rev : list X \to list X` and the length `[.] : list X \to \mathbb{N}` functions as well as the permutation relation $\cdot \sim_p \cdot : list X \to list X \to \mathbb{P}$, as inductively defined in the `Permutation` module of the Coq standard library.

We define finiteness as a property `finite P : \mathbb{P}` of unary relations (viewed as sets):<fnref n="6" />

$$ \mathbf{finite} \{X\} (P : X \to \mathbb{P}) \equiv \exists l, \forall x, P x \leftrightarrow x \in l $$

i.e. there exists a list spanning the relation $P$. This characterization of finiteness as listability is equivalent to Kuratowski finiteness but easier to manipulate formally.

We manipulate relations as functions outputting propositions, hence we denote by $\mathbf{rel}_2 X Y \equiv X \to Y \to \mathbb{P}$ the type of heterogeneous binary relations between $X$ and $Y$. In the homogeneous case, we simply write $\mathbf{rel}_2 X \equiv X \to X \to \mathbb{P}$, and $\mathbf{rel}_1 X \equiv X \to \mathbb{P}$ in the unary case. We use the letters $P, Q : \mathbf{rel}_1$ to denote unary relations and $R, T : \mathbf{rel}_2$ to denote binary relations.

<footnote n="5">⁵ operators on lists are parametric in $X$ and this first argument is nearly always left implicit.</footnote>

<footnote n="6">⁶ Like lists based results, finite is parametric in $X$ and the braces around it specify an implicit argument.</footnote>
to denote binary relations. We write $P \subseteq Q$ or $R \subseteq T$ for the inclusion between relations. Except for commonly found notations like $\in$, $\sim_p$ or $\subseteq$, we generally write related pairs with e.g. a letter for the relation name, in prefix order, like in $Txy$.

For complex inductive predicates, we rather present the constructors using rules with a horizontal line separating the premises from the conclusion. As an example, we below display those of Forall1 $P : rel_1 (list X)$ (denoted $\wedge_1 P$) and Forall2 $R : rel_2 (list X) (list Y)$ (denoted $\wedge_2 R$) which are finitary conjunctions defined in the List module of the standard library, for $P : rel_1 X$ and $R : rel_2 XY$:

$$ \frac{\begin{array}{c} P x \\ \wedge_1 P \end{array}}{\begin{array}{c} \wedge_1 P \end{array}} \frac{\begin{array}{c} \wedge_1 P l \\ (x :: l) \end{array}}{\begin{array}{c} \wedge_2 R \end{array}} \frac{\begin{array}{c} R x y \\ \wedge_2 R l m \end{array}}{\begin{array}{c} \wedge_2 R \end{array}} \frac{\begin{array}{c} (y :: m) \end{array}}{\begin{array}{c} \wedge_2 R \end{array}} $$

The free symbols $x, y : X$ and $l, m : list X$ can be instantiated by any value in their respective types. In the corresponding Coq constructors, they are universally quantified over.

## 3 Inductive covers

We recall the notion of inductive cover [25] which subsumes both accessibility and bar inductive predicates; see Sections 3.2 and 3.3. We discuss three characterizations of covers, the positive, the negative and the sequential, from the strongest to the weakest (constructively), but also explain in some details how to get their classical equivalence, separating the roles played by the axioms of excluded middle and dependent choice. We discuss these characterizations in the context Brouwer's intuitionistic understanding of infinite sequences.

Before we switch to covers, we import the standard order theoretic notion of being upward closed, however not requiring partial orders but any binary relation instead.

**Definition 1 (Upward closed).** Given a type $X$ and a binary relation $T : rel_2 X$, we say that a unary relation $P : rel_1 X$ is $T$-upward closed if $P$ is stable under direct $T$-images. We define: upclosed $T P \equiv \forall x y, T x y \to P x \to P y$.

For instance, the finitary conjunction $\wedge_1 P$ is upward closed for permutations, formally stated as upclosed $(\cdot, \sim_p) \wedge_1 P$. Upward closed unary relations will be preserved by covers, and some results about covers (including the FAN theorem) assume upward closed relations.

### 3.1 Inductive covers definition, basic results

As in [25], we work with the class of singleton inductively generated formal topologies, as opposed to the more general (e.g. indexed) presentation of [7]. They are defined by the notion of inductive cover of a set (i.e. unary relation) along a (transition) binary relation.

**Definition 2 (Inductive cover [25]).** Given a type $X$, a binary relation $T : rel_2 X$ and a unary relation $P : rel_1 X$, we define the inductive $T$-cover of $P$, denoted cover $T P : rel_1 X$ by the two following inductive rules:

$$ \frac{P x}{\text{cover } T P x} \text{ [cover_stop]} \qquad \frac{\forall y, T x y \to \text{cover } T P y}{\text{cover } T P x} \text{ [cover_next]} $$

Notice that $P x$ (resp. $T x y$ and $\text{cover } T P x$) is denoted by $x \in P$ (resp. $y \in T(x)$ and $x \triangleleft P$) in [25] but we favor prefix notations. Remark that the transition relation $T$ is hidden in the infix notation $x \triangleleft P$ used for the cover whereas we keep it in $\text{cover } T P x$. Also in [25], the constructor $[\text{cover\_stop}]$ (resp. $[\text{cover\_next}]$) is called *reflexivity* (resp. *infinity*).
## 2:6 Constructive Substitutes for König's Lemma

The non-dependent induction principle (or eliminator, depending on your preferred terminology) generated for the `cover T P` predicate has the following type:

$$ \mathit{cover\_ind} T P : \forall Q', P \subseteq Q' \to (\forall x, T x \subseteq Q' \to Q' x) \to (\forall x, \mathit{cover} T P x \to Q' x). $$

Informally, it states that `cover T P` is included in any unary relation `Q'` closed under the constructors/rules `[cover_stop]` and `[cover_next]`. Coq auto-generates a slight variant<fnref n="7" /> of `cover_ind` but they are equivalent as non-dependent eliminators. We choose to present the above one because of its direct link with the positive, negative and sequential characterizations of the cover that we discuss in Section 3.4. In our Coq code, we give a straightforward implementation of `cover_ind` as a guarded Fixpoint, similar to the auto-generated one.

Using the `cover_ind` induction principle in combination with the constructors, we show how a morphism can be used to transfer covers between different types and relations.

**Proposition 3 (cover_morphism).** Let X, Y be two types, R : `rel₂ X` and T : `rel₂ Y` be binary relations, and P : `rel₁ X` and Q : `rel₁ Y` be unary relations. We further assume a map `f : Y → X` which is supposed to be a morphism w.r.t. P/Q and R/T, i.e. satisfying

$$ \forall y, P(fy) \to Qy \quad \text{and} \quad \forall y_1 y_2, Ty_1 y_2 \to R(fy_1)(fy_2). $$

Then we have $\forall x y, x = fy \to \mathit{cover} R P x \to \mathit{cover} T Q y$.

As they are made available as Coq code, we generally do not give detailed proofs herein. To illustrate how we reason by induction using `cover_ind`, we exceptionally give a detailed account of the proof for the `cover_morphism` statement.

**Proof.** We first reorder the hypotheses and the goal becomes $\forall x, \mathit{cover} R P x \to \forall y, x = fy \to \mathit{cover} T Q y$, which we prove by induction on $\mathit{cover} R P x$: we factor out `Q'` in the goal as $\forall x, \mathit{cover} R P x \to Q' x$ with $Q' = \lambda x, \forall y, x = fy \to \mathit{cover} T Q y$. Reasoning backwards, we apply the instance $\mathit{cover\_ind} R P Q'$ to the goal, replacing it with two sub-goals:<fnref n="8" />

- $P \subseteq Q'$: unfolding $Q'$, we assume `x` s.t. `P x` and `y` s.t. `x = fy` and we have to show $\mathit{cover} T Q y$. We derive $P(fy)$ by substitution and then $Q y$ using the left morphism hypothesis. We then derive $\mathit{cover} T Q y$ using the constructor `[cover_stop]`;

- $\forall x, (Rx \subseteq Q') \to Q'x$: we assume `x` s.t. $IH_x : \forall z, Rxz \to \forall y', z = fy' \to \mathit{cover} T Q y'$ (corresponding to the induction hypothesis) and `y` s.t. $x = fy$, and we have to show $\mathit{cover} T Q y$. We substitute `x` with $fy$ in $IH_x$ and get $IH_y : \forall z, R(fy)z \to \forall y', z = fy' \to \mathit{cover} T Q y'$. Applying the second constructor `[cover_next]`, we replace the goal $\mathit{cover} T Q y$ with $\forall z, Tyz \to \mathit{cover} T Q z$. Hence we assume `z` s.t. $H_{yz} : T yz$ and we now have to show $\mathit{cover} T Q z$. Using the right morphism hypothesis, we derive $H'_{yz} : R(fy)(fz)$. We instantiate the induction hypothesis as $IH_y(fz) H'_{yz} z \mathit{eq\_refl}$ and get $\mathit{cover} T Q z$ as desired. Notice that we use the reflexive identity for $\mathit{eq\_refl}$: $fz = fz$. This concludes the proof. Using standard automation for backward proof-search (the `eauto` tactic), the Coq proof script however consists in only two lines of code, one for reordering the hypotheses in the initial statement, the second telling which hypothesis to perform induction on, and then launching automation after substituting `fy` for `x`.

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

<footnote n="7">⁷ namely of type $\forall Q', P \subseteq Q' \to (\forall x, T x \subseteq \mathit{cover} T P \to T x \subseteq Q' \to Q' x) \to (\forall x, \mathit{cover} T P x \to Q' x)$.</footnote>

<footnote n="8">⁸ factoring out $Q'$ and applying `cover_ind` are automated for us by the Coq induction tactic.</footnote>
For the rest of the section, we assume a fixed type $X$ to be used as carrier for binary relations $R, T : \mathbf{rel}_2 X$ and unary relations $P, Q : \mathbf{rel}_1 X$. The monotonicity of $\mathbf{cover}$ can be obtained as a particular case, using the identity morphism $f = \lambda x, x$. More precisely, $\mathbf{cover}(\cdot)(\cdot)$ is antitonic in its first argument and monotonic in its second argument:

$$ \mathbf{cover\_mono} R T P Q : T \subseteq R \to P \subseteq Q \to \mathbf{cover} RP \subseteq \mathbf{cover} T Q. $$

Additionally to be increasing (by $[\mathbf{cover\_stop}]$) and monotonic (by $\mathbf{cover\_mono}$), $\mathbf{cover} T$ is also an idempotent operator making it a closure operator:

$$ \mathbf{cover\_idempotent} T P : \mathbf{cover} T (\mathbf{cover} T P) \subseteq \mathbf{cover} T P. $$

**Proof.** Assuming an arbitrary $x$, the proof of $\mathbf{cover} T (\mathbf{cover} T P) x \to \mathbf{cover} T P x$ proceeds by induction on $\mathbf{cover} T (\mathbf{cover} T P) x$. $\quad$

Then we get that the $\mathbf{cover} T$ operator preserves $T$-upward closed unary relations:

$$ \mathbf{cover\_upclosed} T P : \mathbf{upclosed} T P \to \mathbf{upclosed} T (\mathbf{cover} T P). $$

**Proof.** We assume $\mathbf{upclosed} T P$ and an arbitrary $x$ and show $\mathbf{cover} T P x \to \forall y, T x y \to \mathbf{cover} T P y$ by induction on $\mathbf{cover} T P x$. $\quad$

## 3.2 Inductive cover and accessibility

In this section, we fix a type $X$ to serve as carrier for relations below. We recall that the $\mathbf{cover}$ predicate is a generalization of the accessibility predicate, also called $R$-founded in [25].

**► Definition 4 (acc(essibility), $R$-founded).** Given a binary relation $R : \mathbf{rel}_2 X$, the $\mathbf{acc}(\mathbf{essibility})$ predicate<fnref n="9" /> for $R$ and the $R$-founded predicate<fnref n="10" /> are defined inductively, each with one single rule:

$$ \frac{\forall y, R x y \to \mathbf{acc} R y \qquad [\mathbf{acc\_intro}]}{\mathbf{acc} R x} \qquad \frac{\neg R x x \qquad \forall y, R x y \to \mathbf{founded} R y \qquad \mathbf{founded} R x}{\mathbf{founded} R x} $$

A simple observation shows that the shape of the constructor $[\mathbf{acc\_intro}]$ is the same as the second constructor $[\mathbf{cover\_next}]$ of the $\mathbf{cover}$ predicate. Furthermore, the first constructor $[\mathbf{cover\_stop}]$ can be neutralized by setting $P$ as the empty relation $\emptyset = \lambda$, $\perp$. Hence we immediately derive the equivalence:

**► Proposition 5.** The $\mathbf{acc}(\mathbf{essibility})$ predicate is an instance of the $\mathbf{cover}$ predicate.

$$ \mathbf{acc\_iff\_cover\_empty} R x : \mathbf{acc} R x \leftrightarrow \mathbf{cover} R \emptyset x. $$

Moreover, accessible elements are necessarily irreflexive. Indeed, we show $\forall x, \mathbf{acc} R x \to R x x \to \perp$ by induction on $\mathbf{acc} R x$. Hence it follows that the left premise $\neg R x x$ of the constructor of $R$-founded is superfluous:

**► Proposition 6.** $R$-founded and accessibility define equivalent notions:

$$ \mathbf{founded\_iff\_acc} R x : \mathbf{founded} R x \leftrightarrow \mathbf{acc} R x. $$

As a corollary we get $\mathbf{founded} R x \leftrightarrow \mathbf{cover} R \emptyset x$, a result already established in [25, Theorem 3.2] but, seemingly, the authors did not observe that the left premise ($\neg R x x$ i.e. irreflexivity) of the introduction rule for $R$-founded was superfluous.

<footnote n="9">⁹ The variant $\mathbf{Acc}$ as defined in the Coq standard library module `Prelude`, simply uses the reversed relation $R^{-1}$ instead of $R$ for $\mathbf{acc}$. So we have $\mathbf{Acc} R \simeq \mathbf{acc} R^{-1}$ and $\mathbf{Acc} R^{-1} \simeq \mathbf{acc} R$.</footnote>

<footnote n="10">¹⁰ $R$-founded is defined in [25, Definition 3.1].</footnote>
## 3.3 Inductive cover and inductive bars

Let $X$ be a carrier type for lists. We consider unary relations on the type `list X` that we use to represent finite sequences. We show that inductive covers, in addition to generalizing accessibility predicates (see Section 3.2), also generalize inductive bar predicates [6, 10].

**Definition 7 (Inductive bar).** Let $P: rel_1(list X)$ be a unary relation on lists. We define the inductive bar $P: rel_1(list X)$ unary relation with the two following inductive rules:

$$ \frac{P l}{\mathbf{bar} P l} [\mathbf{bar\_stop}] \qquad \frac{\forall x, \mathbf{bar} P (x :: l)}{\mathbf{bar} P l} [\mathbf{bar\_next}] $$

Compared to [10, Definition 6], there are two slight differences. First our lists expand from the left, whereas often in the literature [6, 10, 29], finite sequences expand from the right. Hence rule $[\mathbf{bar\_next}]$ would be written

$$ \frac{\forall x, \mathbf{bar} P (l \dot{=} [x])}{\mathbf{bar} P l} $$

with such a reversed convention. However, this difference can be viewed as just of matter of ordering the display of the arguments of the list constructor `::`. Another more important difference compared to [10, Definition 6] or else [29], is the absence of the inductive rule

$$ \frac{\mathbf{bar} P l}{\mathbf{bar} P (x :: l)} [\mathbf{bar\_monotone}] $$

in Definition 7. We discard rule $[\mathbf{bar\_monotone}]$ because it is admissible for monotone unary relations on finite sequences.

**Definition 8 (Monotone unary relation).** A unary relation $P: rel_1(list X)$ is monotone if it satisfies monotone $P \coloneqq \forall x l, P l \to P(x :: l)$.

The (discarded) $[\mathbf{bar\_monotone}]$ rule/constructor would ensure that $\mathbf{bar} P$ is a monotone predicate even when $P$ is not monotone. However, as an instance of `cover_upclosed`, if $P$ is monotone then so is $\mathbf{bar} P$; see `bar_monotone` after Proposition 10 below. We observe that monotone unary relations are those which are upward closed under list extension:

**Definition 9 (list extension).** The extends: $rel_2(list X)$ binary relation on lists is defined by the single inductive rule: $\frac{\text{ extends } l (x :: l)}{}$

We could have used the first order characterization ` extends l m` $\leftrightarrow$ $\exists x, m = x :: l$ to give an alternate definition of ` extends`. With this notion, we get the equivalence

$$ \mathit{upclosed\_extends\_iff\_monotone} P : \mathit{upclosed extends} P \leftrightarrow \mathit{monotone} P $$

as an immediate consequence, but the specialization goes further:

**Proposition 10 (bar\_iff\_cover\_extends).** Given a unary relation $P: rel_1(list X)$ and a list $l: list X$, we have the equivalence $\mathbf{bar} P l \leftrightarrow \mathbf{cover extends} P l$.

Thanks to Proposition 10 and `upclosed_extendsviff_monotone`, the two below results are specializations of respectively `cover_upclosed` and `cover_monotone`.

$$ \mathbf{bar\_monotone} P : \mathit{monotone} P \to \mathit{monotone} (\mathbf{bar} P); $$

$$ \mathbf{bar\_mono} P Q : P \subseteq Q \to \mathbf{bar} P \subseteq \mathbf{bar} Q. $$

More generally, the analysis that we are going to present for inductive covers in the next section can be specialized to either accessibility predicates and inductive bar predicates.
## 3.4 Positive, negative and sequential characterizations

We now discuss other characterizations of covers, which are not constructively equivalent to the inductive one, but however are classically equivalent, hence the abusive use of the word “characterization.” We present a detailed analysis of those characterizations and which classical axioms their equivalence depends on.

The results of this section that assume classical axioms are not used elsewhere in this paper: these axioms are (propositional) excluded middle (XM), giving us De Morgan laws for logical connectives and quantifiers, and dependent choice (DC):

$$xm: \forall A: \mathbb{P}, A \lor \neg A;$$

$$dc: \forall (A: \text{Type}) (R: \text{rel}_2 A), (\forall a \exists b, R a b) \rightarrow \forall a \exists \rho: \mathbb{N} \rightarrow A, \rho_0 = a \land \forall n, R \rho_n \rho_{1+n}.$$

The names of the results that depend on these added axioms are suffixed with _XM or _DC or both for an unambiguous exposition.

We start with the following definitions of the positive characterization cover_pos , the negative characterization coverpronot , and the sequential characterization cover_seq .

**► Definition 11 (Nonequivalent characterizations of cover).**

$$\text{cover\_pos} \ T P \ x := \lambda Q : \text{rel}_1 X, P \subseteq Q \rightarrow (\forall y, T y \subseteq Q \rightarrow Q y) \rightarrow Q x;$$

$$\text{cover\_neg} \ T P \ x := \lambda Q : \text{rel}_1 X, Q x \rightarrow (\forall y, Q y \rightarrow \exists z, Q z \land T y z) \rightarrow \exists y, P y \land Q y;$$

$$\text{cover\_seq} \ T P \ x := \lambda \rho : \mathbb{N} \rightarrow X, \rho_0 = x \rightarrow (\forall n, T \rho_n \rho_{1+n}) \rightarrow \exists n, P \rho_n.$$

Although not equivalent, the constructive strength of these characterizations can be compared: they are displayed from the strongest ( cover_pos ) to the weakest ( cover_seq ). Beware that both Q and ρ are universally quantified over in the characterizations below.

The positive characterization cover_pos is really just a reordering of the implications in the induction principle cover_ind , so we get the following equivalence purely constructively:

$$\text{cover\_iff\_cover\_pos} \ T P \ x : \text{cover} \ T P \ x \leftrightarrow \forall Q, \text{cover\_pos} \ T P \ x \ Q.$$

The positive characterization is constructively stronger than the negative one:

$$\text{cover\_pos\_cover\_neg} \ T P \ x : (\forall Q, \text{cover\_pos} \ T P \ x \ Q) \rightarrow (\forall Q, \text{cover\_neg} \ T P \ x \ Q).$$

**Proof.** We use ∀ Q , cover_pos T P x Q as the formulation of an induction principle.

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

The negative characterization is constructively stronger than the sequential one. The below proof argument anticipates the intuition behind the definition of the negative characterization.

$$\text{cover\_neg\_cover\_seq} \ T P \ x : (\forall Q, \text{cover\_neg} \ T P \ x \ Q) \rightarrow (\forall \rho, \text{cover\_seq} \ T P \ x \ \rho).$$

**Proof.** Assuming a T -sequence ρ : N → X , we instantiate Q with the direct image ρ ( N ) = λ y, ∃ n, ρ$_{n}$ = y . We show coverpronot T P x ρ ( N ) → cover_seq T P x ρ and conclude.

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

We now explain the intuition behind those definitions by turning to a classical interpreta- tion where all those characterizations are equivalent, discussing the precise roles played by XM and DC. The negative characterization coverpronot is central to our analysis and can be understood in two ways, either as deriving from cover_pos or generalizing cover_seq :

■ The first understanding of coverpronot is as contrapositive form of cover_pos :

$$\text{cover\_pos\_iff\_neg\_XM} \ T P \ x \ Q : \text{cover\_pos} \ T P \ x \ Q \leftrightarrow \text{cover\_neg} \ T P \ x \ (\neg Q).$$
## 2:10 Constructive Substitutes for König's Lemma

The proof involves excluded middle but first-order De Morgan transformations are enough to get the equivalence!<fnref n="11" /> The converse implication of `cover_pos__cover谓neg` above is unlikely to be constructively provable (see Section 3.5), but it is a direct corollary to `cover_pos__iff__cover谓neg_XM`,<fnref n="12" /> however assuming XM as an added axiom;

The second way to understand the negative characterization `cover谓neg` is to view it as a generalization of the sequential characterization `cover_seq`. Notice that the statement $\forall\rho$, `cover_seq` T P x $\rho$ is the usual intuitive definition of being a T-cover for P:

Any infinite T-sequence starting at $x$ meets $P$.<fnref n="13" />

However this interpretation depends on what are the inhabitants of the type $\mathbb{N} \to X$ of which $\rho$ is a member; see Section 3.5. In the proof of `cover谓neg__cover_seq`, we used the direct image $\rho(\mathbb{N})$ as a particular instance of $Q$ in `cover谓neg`. $Q$ represents a set of values containing $x$ and over which $T$ is a total binary relation, which generalizes $T$-sequences by removing the requirement of determinism. The quantification over $T$-sequences $\rho: \mathbb{N} \to X$ is replaced by quantification over $Q$ which is an $T$-unstoppable nondeterministic process: indeed any point in $Q$ has at least one $T$-image in $Q$. This property of unstoppability $\forall y, Qy \to \exists z, Qz \land Tyz$ is shared also by Brouwer's notion of spread.

As a consequence of the above discussion, constructively already, the positive characterization is equivalent to the inductive one, and stronger than the negative one, which is itself stronger than the sequential one. Hence we derive:

$$ \begin{align*} \mathit{cover\_negative} \ T P x & : \mathit{cover} \ T P x \to \forall Q, Qx \to (\forall y, Qy \to \exists z, Qz \land Tyz) \to \exists y, Py \land Qy \\ \mathit{cover\_sequences} \ T P x & : \mathit{cover} \ T P x \to \forall \rho, \rho_0 = x \to (\forall n, T \rho_n \rho_{1+n}) \to \exists n, P \rho_n \end{align*} $$

If one is interested in the converse implications, then, on the one hand, XM would be used to prove that $\forall Q$, `cover谓neg` T P x Q implies `cover` T P x. On the other hand, to recover $\forall Q$, `cover谓neg` T P x Q from $\forall \rho$, `cover_seq` T P x $\rho$, one uses DC {$x \mid Qx$} which is dependent choice specialized on the $\Sigma$-type {$x \mid Qx$} where $Q: \mathit{rel}_1 X$. Indeed, the statement of DC $X$, i.e. dependent choice specialized on type $X$ is:

$$ \mathbf{DC} \ X := \forall R : \mathit{rel}_2 X, (\forall x \exists y, R x y) \to \forall x \exists \rho : \mathbb{N} \to X, \rho_0 = x \land \forall n, R \rho_n \rho_{1+n}. $$

When $Q: \mathit{rel}_1 X$, we reformulate the instance DC {$x \mid Qx$} as<fnref n="14" />

$$ \forall R, (\forall x, Qx \to \exists y, Qy \land R x y) \to \forall x, Qx \to \exists \rho, \rho_0 = x \land \forall n, Q \rho_n \land R \rho_n \rho_{1+n} $$

which is exactly what is needed to extract a sequence $\rho: \mathbb{N} \to X$ out of the $T$-unstoppable process $Q$ starting at $x$.

$$ \mathit{cover\_seq\_cover\_neg\_DC} \ T P x : (\forall \rho, \mathit{cover\_seq} \ T P x \rho) \to (\forall Q, \mathit{cover\_neg} \ T P x Q). $$

**► Theorem 12** (in the spirit of Brouwer's bar theorem). Assuming $xm$ and $dc$, the inductive and the sequential characterizations of covering are equivalent:

$$ \mathit{cover} \ T P x \leftrightarrow \forall \rho, \rho_0 = x \to (\forall n, T \rho_n \rho_{1+n}) \to \exists n, P \rho_n. $$

<footnote n="11">¹¹ In the Coq script, we insist on obtaining that equivalence via De Morgan rewriting and congruence only.</footnote>

<footnote n="12">¹² see `cover谓neg__cover谓pos_XM`.</footnote>

<footnote n="13">¹³ Such formulation are more commonly found for the “intuitive” (read sequential) definition of “being a bar for P” [6]. See `bar_sequences` in Section 3.5 for the corresponding specialization.</footnote>

<footnote n="14">¹⁴ see `DC_sig__DC_Σ` in the Coq code.</footnote>
Hence under XM+DC, any cover is an inductive cover while Brouwer’s “bar theorem” states that “any bar is inductive bar,” or, quoting [6], for sequences of natural numbers:

$$ \forall P : \mathit{rel}_1 (\mathit{list} \mathbb{N}), \mathit{bar} P [] \leftrightarrow \forall \alpha : \mathbb{N} \to \mathbb{N}, \exists n, P [\alpha_{n-1}; \dots; \alpha_0]. $$

The bar theorem statement is an instance of Theorem 12 where $T = \mathit{extends}$. Indeed, an $\mathit{extends}$-sequence of lists in $\mathbb{N} \to \mathit{list} X$ corresponds to the $n$-prefixes of a sequence $\mathbb{N} \to X$; see Brouwer\_bar\_XM\_DC in the Coq code.

## 3.5 Discussion

We have explained how the inductive predicates **bar** and **acc** are just specializations of the notion of inductive **cover** so the remarks below also apply to those restricted notions. For instance we get the following specializations for $R : \mathit{rel}_2 X$ and $P : \mathit{rel}_1 (\mathit{list} X)$:

$$ \mathit{acc\_negative} x : \quad \mathit{acc} R x \to \forall Q, Q x \to (\forall y, Q y \to \exists z, Q z \land R y z) \to \perp; $$

$$ \mathit{acc\_sequences} x : \quad \mathit{acc} R x \to \forall \rho, \rho_0 = x \to (\forall n, R \rho_n \rho_{1+n}) \to \perp; $$

$$ \mathit{bar\_negative} : \quad \mathit{bar} P [] \to \forall Q, Q [] \to (\forall l, Q l \to \exists x, Q (x :: l)) \to \exists l, P l \land Q l; $$

$$ \mathit{bar\_sequences} : \quad \mathit{bar} P [] \to \forall \alpha, \exists n, P [\alpha_{n-1}; \dots; \alpha_0]. $$

The negative characterization is intermediate between the inductive/positive characterization (strongest) and the sequential characterization (weakest). We isolate the role played by XM (in fact De Morgan laws) and DC. While it avoids DC, the negative characterization, using unstoppable nondeterministic processes instead of sequences, still likely requires XM to be equivalent with the positive characterization. Indeed, were the negative characterization be constructively equivalent to positive/inductive characterization, such a result would instantly give us Theorem 12 (and Brouwer’s bar theorem) using DC alone, hence avoiding XM.

The discussion on what is nature of (infinite) sequences is central to the sequential characterization of bars, and of course, as the infinite itself, is very much debated in constructive mathematics. Clearly, adjoining XM and DC populates the type $\mathbb{N} \to X$ with enough *lawless sequences*. Brouwer however rejected XM and DC and instead justifies his bar theorem using “Brouwer’s thesis” [29] which is not as strong as an axiom as XM+DC. In [6], Coquand criticizes the use of the type $\mathbb{N} \to X$ to cover “all” sequences in the sequential characterization of bars:

> “This example is paradigmatic: by replacing systematically the intuitive notion of bar by the notion of inductive bar, we can now prove Brouwer’s fan theorem. More generally, we can think of **bar P** [] as the *correct format expression of a universal quantification over all sequences*, not necessarily given by a law.” (emphasis added)

To be more specific, absent of extra axioms, the type $\mathbb{N} \to X$ of *lawlike sequence* (on which the sequential characterization is based) cannot account for sequences that do not evolve according to a predetermined law, see e.g. Veldman [29]:

> “the intuitionistic mathematician [...] admits the possibility of sequences $\alpha_0, \alpha_1, \alpha_2, \dots$ that are created step-by-step and thus, in some sense, are given by a black box. He is very much aware that *he is unable to make any kind of survey of the totality of all infinite sequences of natural numbers*.” (emphasis added)

In a way, we follow and extend to covers the program proposed by Coquand [6] to systematically replace the intuitive (understand sequential) notion of cover by the inductive version, avoiding axioms altogether. But we can still use the sequential or negative versions, in a limited way, at the end of a constructive deduction, e.g. following the FAN theorem.
4 The FAN theorem for inductive covers

In this section, we present another interpretation of the FAN theorem in type theory, generalizing the FAN theorem for inductive covers [10] to inductive covers [7, 25] instead. We give a concise proof for this result, which differs significantly from that of [10, Theorem 6]. Hence, as an specialization, we get an alternate proof of that former result as well.

In this section, let us fix a type X and a binary relation T : rel₂ X. We extend the binary relation T to lists (viewed as finite sets), as T† : rel₂ (list X) using the direct image and this way, we can view FANs over T as T†-sequences over finite sets.

4.1 Lifting a relation to finite sets

We define the finitary image relation on list X viewed as finite sets, i.e. permutations and contractions are admissible for lists used in that context.

► **Definition 13 (Finitary image).** We define the finitary image binary relation on lists, denoted $T^\dagger : \text{rel}_2(\text{list} X)$, by $T^\dagger := \lambda l m, \forall y, y \in m \rightarrow \exists x, x \in l \wedge T x y$, i.e. $T^\dagger lm$ holds when $m$ is included in the direct image of $l$.

The finitary image relation $T^\dagger$ is monotonic in its first argument and antitonic in its second argument, i.e. $l_1 \subseteq l_2 \rightarrow m_2 \subseteq m_1 \rightarrow T^\dagger l_1 m_1 \rightarrow T^\dagger l_2 m_2$ holds.

One critical observation for the proof of the FAN theorem below is how $T^\dagger$ behaves when splitting its first/source argument in two halves. Then there is a corresponding splitting of the second/image argument, but since $T^\dagger$ ignores the order on the elements of lists, this splitting only holds up to a permutation of the image list:

$$ \mathit{fimage\_split\_inv} \ l_1 \ l_2 \ m : \ T^\dagger \ (l_1 \ \& \ l_2) \ m \rightarrow \exists m_1 m_2, m \sim_p m_1 \ \& \ m_2 \wedge T^\dagger \ l_1 \ m_1 \wedge T^\dagger \ l_2 \ m_2 $$

which we show by induction on $m$. Additionally, we show that $T^\dagger (\cdot) k$ is upward closed for permutations for any $k$, which can be written as $\mathit{upclosed} (\cdot \sim_p \cdot) (T^\dagger \cdot k)$. And to conclude this section, if $P$ is upward closed for $T$ then the finitary conjunction $\wedge_1 P$ of $P$ (over lists) is upward closed for $T^\dagger$, i.e. $\mathit{upclosed} T P \rightarrow \mathit{upclosed} T^\dagger \wedge_1 P$.

4.2 Proof of the FAN theorem for inductive covers

We give a proof of the statement of the FAN theorem for inductive covers, using the finitary image relation $T^\dagger$ to represent FANs over the relation $T$.

► **Theorem 14 (FAN for inductive covers).** Let $P : \text{rel}_1 X$ be $T$-upward closed. If $x$ is in the $T$-cover of $P$ then the singleton list $[x]$ is in the $T^\dagger$-cover of $\wedge_1 P$, i.e.

$$ \mathit{FAN\_cover} : \mathit{upclosed} T P \rightarrow \forall x, \mathit{cover} T P x \rightarrow \mathit{cover} T^\dagger \wedge_1 P [x]. $$

Using a sequential understanding of covers, the statement could be read as: if any $T$-sequence starting at $x$ meets $P$ then any $T^\dagger$-sequence starting at $[x]$ meets $\wedge_1 P$, hence “any finitary FAN rooted at $x$ meets a monotone $P$ uniformly,” which is a commonly found informal statement of the FAN theorem.

While this sequential understanding cannot be established in our constructive framework (for reasons discussed in Section 3.5), we below give a quite compact inductive proof of the positive/inductive understanding of the statement of the FAN theorem for inductive covers.
**Proof.** Let us assume $P$ with upclosed $TP$. We first show that $\text{cover} T^\dagger \wedge_1 P$ is upward closed for permutations, stated as upclosed $(\cdot \sim_p \cdot)(\text{cover} T^\dagger \wedge_1 P)$. For this, we prove $\text{cover} T^\dagger \wedge_1 P l \to \forall m, l \sim_p m \to \text{cover} T^\dagger \wedge_1 P m$ by induction on $\text{cover} T^\dagger \wedge_1 P l$.

Now, we establish the key result that $\text{cover} T^\dagger \wedge_1 P$ is stable under (binary) union, herein represented by the append operation on lists:

$$ \text{cover\_fimage\_union} l m : \text{cover} T^\dagger \wedge_1 P l \to \text{cover} T^\dagger \wedge_1 P m \to \text{cover} T^\dagger \wedge_1 P (l \dashv m). $$

The proof proceeds by nested induction, first on $\text{cover} T^\dagger \wedge_1 P l$ and then on $\text{cover} T^\dagger \wedge_1 P m$, with a critical use of fimage_split_inv to invert two statements of shape $T^\dagger (\cdot \dashv \cdot) (\cdot)$ where the first argument of $T^\dagger$ is a union of lists. As a corollary of cover_fimage_union, we get the specialization where $l = [x]$ is a singleton as

$$ \forall x m, \text{cover} T^\dagger \wedge_1 P [x] \to \text{cover} T^\dagger \wedge_1 P m \to \text{cover} T^\dagger \wedge_1 P (x :: m) $$

and then, as a direct consequence

$$ \text{cover\_fimage\_Forall} l : (\forall x, x \in l \to \text{cover} T^\dagger \wedge_1 P [x]) \to \text{cover} T^\dagger \wedge_1 P l $$

for which we proceed by induction on $l$.

We can conclude with the proof of the FAN theorem for inductive covers. We establish $\text{cover} T^\dagger \wedge_1 P [x]$, reasoning by induction on $\text{cover} T P x$:

- the base case where $P x$ holds is trivially solved by giving a proof of $\wedge_1 P [x]$ and then deriving $\text{cover} T^\dagger \wedge_1 P [x]$ with an instance of first constructor $[\text{cover\_stop}]$;

- in the recursive case where $\forall y, T x y \to \text{cover} T^\dagger \wedge_1 P [y]$ is the induction hypothesis, we show $\forall l, T^\dagger [x] l \to \forall y, y \in l \to \text{cover} T^\dagger \wedge_1 P [y]$ and then combine this with $\text{cover\_fimage\_Forall}$ and an instance of the second constructor $[\text{cover\_next}]$.

This concludes our proof of the FAN theorem for inductive covers.

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

We can immediately derive $\wedge_1 (\text{cover} T P) l \to \text{cover} T^\dagger \wedge_1 P l$ by induction on $l$ and then the following characterization of covering for the finitary image:

$$ \text{cover\_fimage\_iff} : \text{upclosed} T P \to \forall l, \text{cover} T^\dagger \wedge_1 P l \leftrightarrow (\forall x, x \in l \to \text{cover} T P x). $$

i.e. the list $l$ is $T^\dagger$-covered for $\wedge_1 P$ if and only if all the members of $l$ are $T$-covered for $P$.

## 4.3 The FAN theorem for inductive bars

We recall the interpretation of the FAN theorem in type theory [10] and derive an alternate proof of that result as an instance of Theorem 14, which illustrates our claim of generalization. We fix a carrier type $X$ for lists and consider relations over list $X$ and list(list $X$). For $lc: list(list X)$, let us first define the

$$ \text{FAN } lc \equiv \lambda l, \wedge_2 (\cdot \in \cdot) l lc $$

i.e. if written as $l = [x_1; \dots; x_n]$ and $lc = [c_1; \dots; c_p]$, FAN $lc$ $l$ means $n = p$ and $x_1 \in c_1, x_2 \in c_2, \dots, x_n \in c_n$. Stated in plain english, $l$ is a list of one-to-one choices for the choice list $lc$; see the inductive definition of $\wedge_2 R$ in Section 2. Using generic tools designed for the finite abstraction, we can show that FAN $lc$ is a finite, i.e.

$$ \text{FAN\_finite } lc : \text{finite}(\text{FAN } lc). $$
## 2:14 Constructive Substitutes for König's Lemma

However in [10, page 102], the author gives a specific construction of a list which collects the lists of choices $l$ s.t. $\mathbf{FAN} \mathbf{l}c \mathbf{l}$, that we denote $\mathbf{list\_fan} \mathbf{l}c$ herein, satisfying:

$$ \mathbf{list\_fan\_spec} \mathbf{l}c : \forall l, \mathbf{FAN} \mathbf{l}c \mathbf{l} \leftrightarrow l \in \mathbf{list\_fan} \mathbf{l}c. $$

Thus the dependent pair $(\mathbf{list\_fan} \mathbf{l}c, \mathbf{list\_fan\_spec} \mathbf{l}c)$ is an (explicitly given) proof of the proposition finite($\mathbf{FAN} \mathbf{l}c$). The value of $\mathbf{list\_fan} \mathbf{l}c$ can be viewed as a generalization of the exponential function to lists, computing the list of choice sequences for $\mathbf{l}c$.

The FAN theorem as stated and proved in [10] relies on the particular implementation of the exponential $\mathbf{list\_fan}$ given there, but the result itself only depends on the fact that $\mathbf{list\_fan}$ satisfies $\mathbf{list\_fan\_spec}$. Theorem 6 of [10] also assumes the added rule $[\mathbf{bar\_monotone}]$ in the inductive definition of the $\mathbf{bar}$ predicate but it is admissible for monotone relations.

**Theorem 15 (reminder of Theorem 6 of [10]).** Let $P: \mathbf{rel}_1(\mathbf{list} X)$ be unary relation. The following statement holds: $\mathbf{monotone} P \rightarrow \mathbf{bar} P [] \rightarrow \mathbf{bar} (\lambda lc, \wedge_1 P(\mathbf{list\_fan} lc)) []$.

*Proof.* We first reformulate the result as

$$ \mathbf{FAN\_bar} P : \mathbf{monotone} P \rightarrow \mathbf{bar} P [] \rightarrow \mathbf{bar} (\lambda lc, \mathbf{FAN} lc \subseteq P) [] $$

which is an equivalent statement thanks to the monotonicity $\mathbf{bar\_mono}$ of the $\mathbf{bar}$ predicate. Indeed, using $\mathbf{list\_fan\_spec}$, we get the equivalence $\wedge_1 P(\mathbf{list\_fan} lc) \leftrightarrow \mathbf{FAN} lc \subseteq P$ for any $lc$. Now the statement $\mathbf{FAN\_bar} P$ is independent of the implementation of $\mathbf{list\_fan}$.

Using the results of Section 3.3, we replace the hypotheses $\mathbf{monotone} P$ and $\mathbf{bar} P []$ by $\mathbf{upclosed} \mathbf{extends} P$ and $\mathbf{cover} \mathbf{extends} P []$, and the goal $\mathbf{bar} (\lambda lc, \mathbf{FAN} lc \subseteq P) []$ becomes $\mathbf{cover} \mathbf{extends} (\lambda lc, \mathbf{FAN} lc \subseteq P) []$. Hence, by Theorem 14 we get $\mathbf{cover extends}^\dagger \wedge_1 P []$. Then we transfer the inductive cover using $\mathbf{list\_fan}$ as a morphism (Proposition 3):

$$ \mathbf{cover\ extends}^\dagger \wedge_1 P [] \rightarrow \mathbf{cover\ extends} (\lambda lc, \mathbf{FAN} lc \subseteq P) [] $$

after having checked that the following statements hold: $[] = \mathbf{list\_fan} []$, $\mathbf{extends} l m \rightarrow \mathbf{extends}^\dagger (\mathbf{list\_fan} l) (\mathbf{list\_fan} m)$ and $\wedge_1 P (\mathbf{list\_fan} lc) \rightarrow \mathbf{FAN} lc \subseteq P$. $\quad$

Theorem 6 of [10] (cf. Theorem 15), and its original proof, even though it uses one particular implementation of $\mathbf{list\_fan}$ both in the proved statement and inside the arguments, can be adapted to work for any implementation of $\mathbf{list\_fan}$ as soon as it satisfies $\mathbf{list\_fan\_spec}$. The reason is that we pass through $\mathbf{FAN\_bar}$ which is independent of the actual implementation of $\mathbf{list\_fan}$. This is how the proof is implemented our Coq code.

Besides the previous remark and the detour via inductive covers, the proof we give differs from that of [10] in an important way. Indeed, the core argument of the later proof is the closure of monotone inductive bars under binary intersection [10, Proposition 3]:

$$ \mathbf{monotone} P \rightarrow \mathbf{monotone} Q \rightarrow \mathbf{bar} P l \rightarrow \mathbf{bar} Q l \rightarrow \mathbf{bar} (P \cap Q) l $$

which is there established by nested inductions on $\mathbf{bar} P l$, and then on $\mathbf{bar} Q l$. On the contrary, the core argument in the proof of Theorem 14 lies in $\mathbf{cover\_fimage\_union}$, i.e. the closure of $\mathbf{cover} T^\dagger \wedge_1 P$ under binary union (the append operator on lists). In a way, it generalizes to upward closed inductive covers the stability under binary unions of finiteness.
# 5 Weaker variants of the contrapositive of König's lemma

Recall the contrapositive form of König's lemma: any finitely branching tree without infinite branches is finite. We introduce (inductive) rose trees, i.e. finite trees with arbitrary (finite) branching at each node, and we give a type theoretic variant which has stronger assumptions (e.g. the covering assumption below), and which replaces the notion of possibly infinite tree that is implicit in formulation “any ... tree without infinite branches” with that of a relation:

Assume a finitely branching relation $T : rel_2 X$ and $P : rel_1 X$ which is $T$-upward closed. If $x$ belongs to the $T$-cover of $P$ then the finite paths along $T$ starting at $x$ and avoiding $P$ are the branches of a rose tree rooted at $x$.

Notice that we use equivalence between paths and branches to express that (part of) a relation is “the same” as a rose tree. Because we only view the relation via its paths, the acyclicity assumption, as used when (infinite) trees are viewed as graphs, can be dropped. But before we formalize this statement, we must define paths, rose trees and their branches.

## 5.1 Path, rose trees and their branches

Let us fix a type $X$ as carrier for relations and indices of rose trees below.

**► Definition 16 (Inductive path).** For a relation $T : rel_2 X$, the paths in $T$ are described by a ternary relation $path_T : X \to list_X \to X \to \mathbb{P}$ defined by two inductive rules:

$$ \frac{\text{path } T \ x \ [] \ x}{T \ x \ y \quad \text{path } T \ y \ p \ z} $$

Intuitively, $path_T x p y$ means that $p$ is the sequence of values encountered on a path from $x$ to $y$, following the relation $T$, including the endpoint $y$ but excluding starting point $x$. The existence of a $T$-path from $x$ to $y$ is equivalent to the reflexive-transitive closure of $T$ (we do not use this characterization however), and hence we have:

$$ \text{upclosed\_path } T P : \text{upclosed } T P \to \text{upclosed} (\lambda x y, \exists p, \text{path } T x p y) P. $$

**► Definition 17 (Inductive rose tree).** The type of $X$-indexed rose trees denoted $\text{tree}_X : \text{Type}$ is inductively defined by a single rule:

$$ \frac{x : X \quad l : \text{list}(\text{tree}_X)}{\langle x | l \rangle : \text{tree}_X \quad [\text{node}]} $$

where we denote $\langle x | l \rangle$ as a shortcut for $(\text{node } x \ l)$. The root of $t = \langle x | l \rangle$ is indexed by $x$ and we write $\text{root}_t = x$, and $l$ is the list of the sons of $t$. We define the height of a rose tree, denoted $\text{tree}\_\text{ht} : \text{tree}_X \to \mathbb{N}$, using the fixpoint equation $\text{tree}\_\text{ht} \langle x | [t_1; \dots; t_n] \rangle = 1 + \text{list\_max}[\text{tree}\_\text{ht} t_1; \dots; \text{tree}\_\text{ht} t_n]$.

The branches of a rose tree (the paths starting at the root) are characterized using a ternary relation $\text{branch} : \text{tree}_X \to \text{list}_X \to X \to \mathbb{P}$ inductively defined by two rules:

$$ \frac{\langle y | m \rangle \in l \quad \text{branch} \langle y | m \rangle \ p \ z}{\text{branch} \langle x | l \rangle [] \ x} $$

Hence a branch is either empty, stopping at the root, or the choice of a son (i.e. sub-tree) and of a branch in that son. The predicate $\text{branch } t \ p \ y$ relates a tree $t$, a list of visited indices $p$ up to the index $y$ of the root of a sub-tree of $t$.
## 5.2 Representing binary relations using rose trees

We give a formal definition for the statement “a binary relation is a finite tree.” This is required indeed because the type of binary relations and the type of rose trees are very different. We use paths in relations and branches in rose trees as a means to define the notion of *representation* by a rose tree, for the part of a relation $T: rel_2 X$ rooted at $x$ of which the paths from $x$ satisfy the property $P: \text{list}X \to X \to \mathbb{P}$.

**► Definition 18 (Representation).** Assume a binary relation $T: rel_2 X$, a property for paths $P: \text{list}X \to X \to \mathbb{P}$ and a point $x: X$. We say that $P$ in $T$ at $x$ is strongly represented by $t: \text{tree}X$ and write $\text{strongly\_represents} T P x t$ if:

$$ \text{strongly\_represents} T P x t := \text{root} t = x \wedge \forall p y, \text{branch} t p y \leftrightarrow \text{path} T x p y \wedge P p y. $$

We say that $P$ in $T$ at $x: X$ is represented by $t: \text{tree} X$ and write $\text{represents} T P x t$ if:

$$ \text{represents} T P x t := \text{root} t = x \wedge \forall p y, P p y \rightarrow (\text{branch} t p y \leftrightarrow \text{path} T x p y). $$

The property $P$ for paths is applied only to those originating at $x$ but can depend on the destination as well as on the sequence of visited nodes on the path to the destination.

We observe that $\text{strongly\_represents} T P x t \rightarrow \text{represents} T P x t$. While the strong notion would be a first/natural choice to formalize the idea that the relation $T$ starting at $x$ and restricted by $P$ “is a tree,” this choice can however be questioned in the light of decidability issues. Indeed, when $X$ is equipped with a (propositionally) decidable equality,<fnref n="15" /> e.g. when $X = \mathbb{N}$, then both `branch t p y` and `path T x p y` become decidable predicates. In that case, `strongly\_represents T P x t` implies that $P$ is decidable as well, an assumption we want to avoid for building representations. In the case of `represents`, $P$ does not need to be decidable but the representing tree may contain branches which do not satisfy $P$.

We assume a fixed $T: rel_2 X$ which is furthermore *finitely branching*, i.e. $\forall x, \text{finite}(Tx)$. We show that paths of bounded length can be strongly represented.

**► Theorem 19.** When $T: rel_2 X$ is *finitely branching*, for any $n: \mathbb{N}$ and any $x: X$, the property $(\lambda p y, \lfloor p \rfloor \le n)$ in $T$ at $x$ has a strong representation.

*Proof.* We build the tree $t$ s.t. $\text{strongly\_represents} T (\lambda p y, \lfloor p \rfloor \le n) x t$ by induction on $n$, after generalizing on $x$. ◀

Now we characterize the properties of paths that have representations as those which hold only for small paths.

**► Theorem 20.** When $T: rel_2 X$ is *finitely branching*, for any property $P: \text{list} X \to X \to \mathbb{P}$ and any point $x: X$, the two following statements are equivalent:

- $\exists t, \text{represents} T P x t$;

- $\exists n, \forall p y, \text{path} T x p y \rightarrow P p y \rightarrow \lfloor p \rfloor < n$.

*Proof.* In the forward direction, the bound $n$ can be chosen to be the height $\text{tree\_ht} t$ of the representation of $P$ in $T$ at $x$. In the reverse direction, given a bound $n$ for the length of paths satisfying $P$, we first obtain a tree $t$ s.t. $\text{strongly\_represents} T (\lambda p y, \lfloor p \rfloor \le n) x t$. We then check that this tree $t$ represents $P$ in $T$ at $x$. ◀

<footnote n="15">¹⁵ i.e. $\forall x y: X, x = y \lor x \ne y$.</footnote>
Theorem 20 states that, in the finitely branching case, a relation is represented by a (finite) rose tree if and only if there is a global bound on the length of its paths. In the context of the FAN theorem (the contrapositive of Kőnig's lemma), it relates the finiteness of a tree to the boundedness of its height, the length of its longest branch. It can be compared to the characterization of binary trees<fnref n="16" /> which are finite as those for which there is a uniform bound on the length of their branches, see e.g. [15].

## 5.3 Kőnig's lemma for inductive covers, accessibility and inductive bars

We establish statements of weakened variants of (the contrapositive of) Kőnig's lemma, assuming e.g. the existence of a cover for the root of the "tree".

**▶ Theorem 21 (Kőnig's lemma for inductive covers).** Let us assume a finitely branching binary relation $T : rel_2 X$, i.e. $\forall x, finite(Tx)$, a T-upward closed unary relation $P : rel_1 X$, a root $x : X$ which is T-covered by $P$. Then the paths which refute $P$ at their tail are represented in $T$ at $x$, i.e. $\exists t, \text{represents } T(\lambda p y, \neg P y) x t$.

**Proof.** Using the length of paths, we define $circlen$, the circle (centered at $x$) of radius $n$, and the collection of $Q : rel_1 (list X)$ of finite supports of some circle as

$$circlen := \lambda y, \exists p, \text{path } T x p y \wedge n = [p] \quad Ql := \exists n, \forall x, circlen x \leftrightarrow x \in l.$$

Because $T$ has finite direct images, we deduce that circles are finite, by induction on $n$. Hence we get $\forall n, \text{finite}(circlen)$.

Let us show that $Q$ meets $\wedge_1 P$. Indeed, as we assume $\text{cover } T P x$, using the FAN Theorem 14 for covers we get $\text{cover } T^\dagger \wedge_1 P [x]$. Then we use $\text{cover\_negative}$ with $Q$. We only need to show that $Q$ holds at $[x]$ and is $T^\dagger$-unstoppable i.e. $\forall l, Ql \to \exists m, Qm \wedge T^\dagger lm$:

- $Q[x]$ holds because $[x]$ is a support for the circle of radius 0;

- $Q$ is $T^\dagger$-unstoppable because the circle of radius $1+n$ is a $T^\dagger$-image of that of radius $n$.

As $Q$ meets $\wedge_1 P$, then $P$ contains some circle, i.e. there is $n$ such that $circlen \subseteq P$. As a consequence, since $T$-paths from $x$ of length greater than $n$ cross $circlen$ hence meet $P$ at that crossing point, their tail must belong to $P$ as well, because $P$ is $T$-upward closed. Hence $\forall p y, \text{path } T x p y \to n \le [p] \to P y$ holds and we conclude using Theorem 20. ◀

This proof uses the FAN Theorem 14 for inductive covers, and then combines it with the $\text{cover\_negative}$ characterization. The finiteness of circles $\forall n, \text{finite}(circlen)$, which lives $\mathbb{P}$ (and not in Type), is not strong enough to be able to define circle as a map $\mathbb{N} \to list X$, which would be needed if the $\text{cover\_sequences}$ characterization were to be used instead of $\text{cover\_negative}$.

As the instance of Theorem 21 where $P = \emptyset$, we recover a finitary form of Kőnig's lemma similar to [1, p. 15]. A direct proof by induction on (the proof of) $\text{acc } T x$ would probably be shorter but we here illustrate the generality of Kőnig's lemma for inductive covers.

**▶ Corollary 22 (Kőnig's lemma for accessibility [1]).** Let $T : rel_2 X$ be a binary relation s.t. $\forall x, \text{finite}(Tx)$ and let $x : X$ be a $T$-accessible point of $X$, i.e. $\text{acc } T x$. Then there is a rose tree $t : \text{tree } X$ with root $x$ such that the $T$-paths from $x$ are exactly the branches of $t$.

We present a variant of Kőnig's lemma for inductive covers. It is not exactly an instance of Theorem 21 because the properties of paths are not limited to those of their endpoint.

<footnote n="16">¹⁶ as sets of finite sequences of Booleans representing their finite branches.</footnote>
We finish our tour of weakened forms of Kőnig's lemma with a slightly different form where the outcome is not a representing rose tree but just its height, hence a bound on the length of its branches. In light of Theorem 20, these are equivalent conditions for finitely branching relations. While we insisted so far on getting tree representations in the spirit of Kőnig's lemma, in its applications on e.g. termination, a bound on the height of this tree is often sufficient to conclude.

Given a sequence of relations $P: \mathbb{N} \to \text{rel}_1 X$, we define a predicate $\text{choice_list } P: \text{rel}_1 (\text{list } X)$ such that $\text{choice_list } P[x_0; \dots; x_{n-1}] \leftrightarrow P_0 x_0 \wedge \dots \wedge P_{n-1} x_{n-1}$, i.e. $\text{choice_list } P l$ holds exactly when the members of $l$ are successive choices in $P_0, P_1, \dots$

**Theorem 25.** Given an almost full relation, i.e. $R: \text{rel}_2 X$ s.t. $\text{af } R$, and a sequence of finite unary relations, i.e. $P: \mathbb{N} \to \text{rel}_1 X$ s.t. $\forall n, \text{finite } P_n$. Then the length of irredundant choice lists for $P$ is (uniformly) bounded. Formally, we get:

$$ \text{af } R \to (\forall n, \text{finite } P_n) \to \exists n, \forall l, \text{choice_list } P l \to \text{irred } R l \to [l] < n. $$

*Proof.* From $\text{af\_bar\_good\_nil}$, we know that $\text{bar}(\text{good } R)$ [] holds and we apply the $\text{FAN\_bar}$ form of Theorem 15 and derive $\text{bar}(\lambda lc, \text{FAN } lc \subseteq \text{good } R)$ [].

We define $\text{support } n l := \forall x, P_n x \leftrightarrow x \in l$, meaning that $l$ is a supporting list for the (finite) unary relation $P_n$. We use the $\text{bar\_negative}$ characterization of inductive bars applied to $\text{bar}(\lambda lc, \text{FAN } lc \subseteq \text{good } R)$ [] with $Q := \lambda lc, \text{choice_list support } (\text{rev } lc)$. We get $lc$ such that $\text{FAN } lc \subseteq \text{good } R$ and $\text{choice_list support } (\text{rev } lc)$.

Then we check that $n = [lc]$ satisfies the property $\forall l, \text{choice_list } P l \to [l] = n \to \text{good } R (\text{rev } l)$. The same value then bounds the length of irredundant choice lists for $P$. ◀

Again, we use a combination of a FAN theorem and the negative characterization of inductive bars. The assumption of finiteness $\forall n, \text{finite } P_n: \mathbb{P}$ is not strong enough to be able to build a sequence $\mathbb{N} \to \text{list } X$ that enumerates the respective supports for $P_0, P_1, \dots$ but the negative characterization allows us to reason without escaping from the $\mathbb{P}$ sort.

## 5.5 Type-bounded variants and the FAN functional

To answer a question of one of the reviewers, we briefly discuss how the FAN theorem for covers and its consequences can be lifted to Type-bounded variants allowing for the computation of FAN functionals, which output bounds on the length of branches of finite trees. For this, the types of the cover, bar or af predicates are lifted as:

$$ \text{cover}_t \{X\} (T: X \to X \to \text{Type}) (P: \text{rel}_1 X) : X \to \text{Type} $$

$$ \text{bar}_t \{X\} (P: \text{rel}_1 (\text{list } X)) : \text{list } X \to \text{Type} $$

$$ \text{af}_t \{X\} (R: \text{rel}_2 X) : \text{Type} $$

and, as a consequence, parts of the List and Permutation library results need to be given Type-bounded variants as well. Noticeably, the transition relation argument $T$ in $\text{cover}_t$ is lifted, and not only its output sort.

In Coq jargon, we say that those predicates become informative, meaning that their inductive structure can be used to compute values of sort Type, typically bounds on the length of branches in $\mathbb{N}$. As an illustration here, these variants include the following FAN functional, lifting Theorem 25 above to an output of sort Type:

$$ \text{af}_t R \to (\forall n, \text{finite}_t P_n) \to \{n: \mathbb{N} | \forall l, \text{choice\_list } P l \to \text{irred } R l \to [l] < n\} $$

where $\text{finite}_t \{X\} (P: X \to \mathbb{P}) = \{l | \forall x, P x \leftrightarrow x \in l\}$ is the lifting of finiteness.

We delegate to the distributed Coq code, specifically file `constructive_konig_type.v`, the explanations on how such liftings are performed.
# 6 Two examples of replacements of König's lemma

In this section, we discuss two applications of our constructive variants of König's lemma that allow to transfer some "classical" proofs into the realm of constructive mathematics.

## 6.1 The decidability from implicational relevance logic

In [20], we use a variant of König's lemma for almost full relations, corresponding here to Theorem 25, to show the termination of an exhaustive proof search procedure for implicational relevance logic (IR), based on a sequent system designed by Curry [8]. The termination of this system was established by Kripke [17], building on Curry's work, rediscovering Dickson's lemma, and concluding with König's lemma.

The idea of the proof is the following. Curry's sequent proof system is proved sound and complete for IR. It has three essential properties:

- each sequent rule has finitely many premises, in fact less than two;

- for any conclusion, there are only finitely many rule instances having that conclusion;

- there is a notion of redundancy for sequents such that, if a sequent $S_2$ is redundant over $S_1$, then any proof of $S_2$ can be contracted into a proof of $S_1$ of lesser height. This property is called *Curry's lemma*.

Kripke proved that the notion of redundancy, derived from the natural inclusion ordering on multisets, forms a well quasi order (WQO), and thus any sequence of sequents contains a redundant pair. Notice that the WQO terminology and Dickson's lemma, the key ingredient in the result, were only popularized later on. Then, using Curry's lemma, Kripke argued that any proof search branch must contain a redundant pair, and by König's lemma, the proof search tree for irredundant proofs is finite.

Replacing the classical approach to WQOs by inductive almost full relations, in [20] we prove that the notion of redundancy is almost full, the constructive form of Dickson's lemma been derived from Coquand's constructive form of Ramsey's theorem [31]. Then we use the Type-bounded variant of Theorem 25 called *Constructive_Koenigs lemma* and outlined in Section 5.5 to show that the irredundant part of the proof search tree has a computable bound on its height, so the search process can be safely pruned above that height.

## 6.2 Building Harvey Friedman's TREE(n) monster

In [23], we build on a Coq constructive proof of Kruskal's tree theorem [22] to implement TREE(n) function (that we specify below), invented and studied by Harvey Friedman [11] in his groundbreaking work on reverse mathematics.

The (homeomorphic) embedding on rose trees is a WQO as soon as the comparison between decorations of the nodes is itself a WQO: this is the statement of Kruskal's theorem in a classical setting. In [22], we implement a constructively provable form by replacing WQOs with (inductive) *af* relations (see Definition 24). Notice that this constructive form of Kruskal's theorem has a quite involved proof that we do not discuss here.

Using Kruskal's theorem, the homeomorphic embedding between roses trees decorated with elements of the finite set {1, ..., *n*} is *af* and we use this relation as our redundancy relation. This means, using the sequential characterization *af_sequences* of Section 5.4, that any sequence $T_1, T_2, ...$ of rose trees contains a redundant pair. Now Friedman bounds the number of possible choice for $T_i$ by requiring that its size (number of nodes) is less than *i*: we say that *T_i* is *sized*. Hence, considering the set of all such sized sequences ($T_i$)$_{0<i}$, they form a finitely branching tree and all infinite branches contain a redundant pair. Following
the argumentation of e.g. [13], by Kőnig's lemma, the irredundant part of that tree is finite
and thus sized sequences have maximal length, which is by definition TREE(n).

We circumvent this classical argumentation by applying Theorem 25, hence, according
to its proof, first applying the FAN theorem for inductive bars and then the negative
characterization of inductive bars. We obtain, constructively, the existence of a uniform
bound on the length of irredundant sequences of sized trees ($T_i$)$_{0<i}$. The exact value of the
bound, i.e. TREE(n), can then be computed by unbounded linear search [23]<fnref n="19" />

7 Conclusion

Besides the Coq script that supports the results presented herein, we can summarize our
contributions as following. We show that the notion of inductive cover generalizes both
accessibility and bar inductive predicates, hence we can discuss concepts and results at the
level of covers and they instantiate on these restricted notions as well. We follow Coquand's
program [6] and replace characterizations based on sequences with inductive ones, that
constructively do not fall short on lawless sequences.

We compare the strength of the positive, negative and sequential characterizations of
covers, or (as an instance) of “being a bar;” both in constructive and classical contexts. We
analyze the precise roles played by the axioms of excluded middle and dependent choice.

The negative characterization is a remarkable intermediate notion: a) it is a De Morgan
dual of the positive characterization; b) it expels determinism from the sequential character-
ization, and shares properties with Brouwer’s notion of spread; c) it is relevant in practice,
for instance when dealing with **Prop**-bounded Coq definitions.

We give a concise constructive proof of a FAN theorem for inductive covers that generalizes
the type theoretic interpretation of the FAN theorem for inductive bars [10]. We notice that
the respective core argument of these two proofs differ significantly.

The negative or sequential characterizations of covers (or bars) are weaker than the posit-
ive/inductive characterization. They fail when trying to constructively establish important
closure properties, such as the FAN theorem. However, they can still be used constructively,
after the inductive FAN theorem, to obtain uniform bounds on the length of branches of
trees. This is the core argumentation behind several weaker variants of Kőnig's lemma that
we derive and present, herein insisting on representations by inductive rose trees.

To conclude, we discuss two applications of those constructive variants of Kőnig's lemma
that allow the transport of classical results in the constructive realm.

Almost full relations give a satisfactory constructive account for the notion of well quasi
order, i.e., finitary closure properties such as Dickson's lemma, Higman's lemma and Kruskal's
tree theorem can be constructively established with this notion. However, as far as we are
aware, the stronger notion of better quasi order (BQO) has not yet been given a suitable
inductive account, and it would be quite a challenge to lean towards an inductive definition
of BQOs, hopefully satisfying additional infinitary closure properties.

References

1 F. Baader and T. Nipkow. *Term Rewriting and All That*. Cambridge University Press, 1998.

2 J. Berger. Brouwer's fan theorem, 2021. doi:10.48550/arXiv.2001.00064.

3 J. Berger and H. Ishihara. Brouwer's fan theorem and unique existence in constructive analysis. *Mathematical Logic Quarterly*, 51(4):360-364, 2005. doi:10.1002/malq.200410038.

<footnote n="19">¹⁹ Using a *Type*-bounded variant of Theorem 25, one can use bounded linear search instead of unbounded linear search. However, there is little to gain in obtaining an efficient algorithm for computing TREE(n) since writing TREE(3) in decimal would already exhaust all atoms of the known universe.</footnote>
4 J. Berger and G. Svindland. Brouwer's fan theorem and convexity. *The Journal of Symbolic Logic*, 83(4):1363-1375, 2018. doi:10.1017/jsl.2018.49.

5 C. Cheung. Brouwer's Fan Theorem: An Overview. Master's thesis, Cornell University, 2015. URL: https://api.semanticscholar.org/CorpusID:203584866.

6 T. Coquand. About Brouwer's Fan Theorem. *Revue internationale de philosophie*, 230:483-489, September 2004. URL: http://www.jstor.org/stable/23955601.

7 T. Coquand, G. Sambin, J. Smith, and S. Valentini. Inductively generated formal topologies. *Annals of Pure and Applied Logic*, 124(1):71-106, 2003. doi:10.1016/S0168-0072(03)00052-6.

8 H. B. Curry. *A Theory of Formal Deductibility*. Notre Dame mathematical lectures. University of Notre Dame, 1957.

9 M. Escardo. Infinite sets that admit fast exhaustive search. In *22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)*, pages 443-452, 2007. doi:10.1109/LICS.2007.25.

10 D. Fridlender. An Interpretation of the Fan Theorem in Type Theory. In *Types for Proofs and Programs*, pages 93-105. Springer Berlin Heidelberg, 1999. doi:10.1007/3-540-48167-2_7.

11 H. M. Friedman. Internal finite tree embeddings. In *Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman*, Lecture Notes in Logic, pages 60-91. Cambridge University Press, 2002.

12 M. Fujiwara. König's lemma, weak König's lemma, and the decidable fan theorem. *Mathematical Logic Quarterly*, 67(2):241-257, 2021. doi:10.1002/malq.202000020.

13 J. H. Gallier. What's so special about Kruskal's theorem and the ordinal $\Gamma_0$? A survey of some results in proof theory. *Annals of Pure and Applied Logic*, 53(3):199-260, 1991. doi:10.1016/0168-0072(91)90022-E.

14 W. Hanf. Nonrecursive Tilings of the Plane. I. *The Journal of Symbolic Logic*, 39(2):283-285, 1974. doi:10.2307/2272640.

15 H. Ishihara. Weak König's Lemma Implies Brouwer's Fan Theorem: A Direct Proof. *Notre Dame Journal of Formal Logic*, 47(2):249-252, 2006. doi:10.1305/ndjfl/1153858649.

16 S. C. Kleene and R. E. Vesley. *The Foundations of Intuitionistic Mathematics: Especially in Relation to Recursive Functions*. North-Holland Publishing Co., 1965.

17 S. Kripke. The Problem of Entailment (abstract). *Journal of Symbolic Logic*, 24:324, 1959.

18 D. König. Über eine Schlussweise aus dem Endlichen ins Unendliche. *Acta Sci. Math. (Szeged)*, 3(2-3):121-130, 1927.

19 D. Larchey-Wendling. Constructive substitutes for König's lemma ( artifact ). Software, NARCO (ANR-21-CE48-0011), swhId: **swh:1:dir:611c848b0dbc19c9de20744122776440c00e413d** (visited on 2025-05-25). URL: https://github.com/DmxLarchey/Constructive-Konig, doi:10.4230/artifacts.23151.

20 D. Larchey-Wendling. Constructive Decision via Redundancy-Free Proof-Search. *Journal of Automated Reasoning*, 64:1197-1219, 2020. doi:10.1007/s10817-020-09555-y.

21 D. Larchey-Wendling. Quasi Morphisms for Almost Full Relations. In *30th International Conference on Types for Proofs and Programs, TYPES*, 2024. URL: https://easychair.org/publications/preprint/M3Km.

22 D. Larchey-Wendling. The Coq-Kruskal project, April 2024. URL: https://github.com/DmxLarchey/Coq-Kruskal.

23 D. Larchey-Wendling. The Friedman-TREE project, November 2024. URL: https://github.com/DmxLarchey/Friedman-TREE.

24 D. Myers. Nonrecursive Tilings of the Plane. II. *The Journal of Symbolic Logic*, 39(2):286-294, 1974. doi:10.2307/2272641.

25 C. Sacerdoti Coen and S. Valentini. General Recursion and Formal Topology. In *PAR-10. Partiality and Recursion in Interactive Theorem Provers*, volume 5 of *EPiC Series in Computing*, pages 72-83. EasyChair, 2012. doi:10.29007/hl175.

26 S. G. Simpson. *Subsystems of Second Order Arithmetic*. Perspectives in Logic. Cambridge University Press, 2 edition, 2009.
27 A. S. Troelstra. Note on the Fan Theorem. *The Journal of Symbolic Logic*, 39(3):584–596, 1974. doi:10.2307/2272902.

28 A. S. Troelstra. Some Models for Intuitionistic Finite Type Arithmetic with Fan Functional. *The Journal of Symbolic Logic*, 42(2):194–202, 1977. doi:10.2307/2272120.

29 W. Veldman. Brouwer's Real Thesis on Bars. *Philosophia Scientiæ*, pages 21–42, 2006. doi:10.4000/philosophiascientiae.404.

30 W. Veldman. Brouwer's Fan Theorem as an axiom and as a contrast to Kleene's alternative. *Arch. Math. Logic*, 53:621–693, 2014. doi:10.1007/s00153-014-0384-9.

31 D. Vytiniotis, T. Coquand, and D. Wahlstedt. Stop When You Are Almost-Full. In *Intercative Theorem Proving*, pages 250–265. Springer Berlin Heidelberg, 2012. doi:10.1007/978-3-642-32347-8_17.