Constructive Substitutes for Kőnig’s Lemma

Larchey-Wendling, Dominique

doi:10.4230/LIPIcs.TYPES.2024.2

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.

Keywords and phrases:

Kőnig’s lemma, FAN theorem, constructive mathematics, inductive covers, inductive bars, almost full relations, inductive type theory, Coq

Funding:

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

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Type theory ; Theory of computation

\rightarrow

Constructive mathematics

Editors:

Rasmus Ejlers Møgelberg and Benno van den Berg

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

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.¹¹1the original statement rather talks about paths in a graph.

The restriction to at most binary trees is of particular importance because it can be stated within lightweight foundations like e.g. $\mathit{RCA}_{0}$ [26], and is usually called weak Kőnig’s lemma ( $\mathit{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 $\mathit{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.

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] $\mathrm{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,²²2choices between the left or the right son. 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].³³3as said earlier, the notion of what is constructively acceptable is not universally agreed on.

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.⁴⁴4Notice that the tileability of a finite square is a decidable property.

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:

$\blacksquare$

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;
$\blacksquare$

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 $\mathtt{acc}\>{F}:\mathtt{rel}_{1}\>X$ predicate:

where $F:\mathtt{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\mathbin{{+\mskip-10.0mu+}}{[\_]}$ , 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 $\mathit{root}$ can be defined by $(\mathtt{acc}\>{F}\,\mathit{root})$ , and thus understood as the unavoidable termination of the nondeterministic process of expending branches by adding sons after sons, starting from the $\mathit{root}$ . Intuitively, the proof of $(\mathtt{acc}\>{F}\,\mathit{root})$ is a well-founded tree where a leaf is decorated with a proof of $(\mathtt{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.

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 $\mathtt{Type}$ the Coq hierarchy of types, as usual with this framework. We write $\bot:\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 $\lnot P\mathrel{{:}\!{=}}P\mathrel{\rightarrow}\bot$ . Following the BHK interpretation, $X\mathrel{\rightarrow}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\mathrel{\rightarrow}\mathbb{P}$ or $P:X\mathrel{\rightarrow}\mathtt{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\mathrel{\rightarrow}\mathbb{P}$ we have the proposition $\exists x,\,P\,x:\mathbb{P}$ and the type $\{x\mid P\,x\}:\mathtt{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 $\mathtt{Type}$ .

The type of Peano natural numbers $\mathbb{N}$ is inductively defined in Coq as $\mathbb{N}:n\mathrel{{:}\!{:}\!{=}}0\mid\mathtt{S}\,n$ and arithmetic in Coq, which we assume, is built on this type. We manipulate finite sequences as lists, polymorphic⁵⁵5operators on lists are parametric in $X$ and this first argument is nearly always left implicit. over the carrier type $X$ , in the inductive type $\mathtt{list}\,X:\leavevmode\nobreak\ l\mathrel{{:}\!{:}\!{=}}{[\mskip 1.0mu]}% \mid x\mathbin{::}l$ where $x : X$ . Additionally, list concatenation (resp. membership) is named $\mathtt{app}$ (resp. $\mathtt{In}$ ), denoted infix by $\cdot\mathbin{{+\mskip-10.0mu+}}\cdot:\mathtt{list}\,X\mathrel{\rightarrow}% \mathtt{list}\,X\mathrel{\rightarrow}\mathtt{list}\,X$ (resp. $\cdot\in\cdot:X\mathrel{\rightarrow}\mathtt{list}\,X\mathrel{\rightarrow}% \mathbb{P}$ ), and defined by a guarded fixpoint. Moreover, we use the reverse $\mathtt{rev}:\mathtt{list}\,X\mathrel{\rightarrow}\mathtt{list}\,X$ and the length ${\lfloor{\cdot}\rfloor}:\mathtt{list}\,X\mathrel{\rightarrow}\mathbb{N}$ functions as well as the permutation relation $\cdot\mathrel{\sim_{p}}\cdot:\mathtt{list}\,X\mathrel{\rightarrow}\mathtt{list% }\,X\mathrel{\rightarrow}\mathbb{P}$ , as inductively defined in the $\mathtt{Permutation}$ module of the Coq standard library.

We define finiteness as a property $\mathtt{finite}\,P:\mathbb{P}$ of unary relations (viewed as sets):⁶⁶6Like lists based results, $\mathtt{finite}$ is parametric in $X$ and the braces around it specify an implicit argument.

\mathtt{finite}\leavevmode\nobreak\ \{X\}\leavevmode\nobreak\ (P:X\mathrel{% \rightarrow}\mathbb{P})\mathrel{{:}\!{=}}\exists l,\,\forall x,\,P\,x\mathrel{% \,\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 $\mathtt{rel}_{2}\>{X\>Y}\mathrel{{:}\!{=}}X\mathrel{\rightarrow}Y\mathrel{% \rightarrow}\mathbb{P}$ the type of heterogeneous binary relations between $X$ and $Y$ . In the homogeneous case, we simply write $\mathtt{rel}_{2}\>X\mathrel{{:}\!{=}}X\mathrel{\rightarrow}X\mathrel{% \rightarrow}\mathbb{P}$ , and $\mathtt{rel}_{1}\>X\mathrel{{:}\!{=}}X\mathrel{\rightarrow}\mathbb{P}$ in the unary case. We use the letters $P,Q:\mathtt{rel}_{1}\>\_$ to denote unary relations and $R,T:\mathtt{rel}_{2}\>{\_\>\_}$ 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$ , $\mathrel{\sim_{p}}$ or $\subseteq$ , we generally write related pairs with e.g. a letter for the relation name, in prefix order, like in $T\,x\,y$ .

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 $\mathtt{Forall}\,P:\mathtt{rel}_{1}\>{(\mathtt{list}\,X)}$ (denoted ${\textstyle{\wedge_{1}}}P$ ) and $\mathtt{Forall2}\,R:\mathtt{rel}_{2}\>{(\mathtt{list}\,X)\>(\mathtt{list}\,Y)}$ (denoted ${\textstyle{\wedge_{2}}}R$ ) which are finitary conjunctions defined in the $\mathtt{List}$ module of the standard library, for $P:\mathtt{rel}_{1}\>X$ and $R:\mathtt{rel}_{2}\>{X\>Y}$ :

The free symbols $x, y : X$ and $l,m:\mathtt{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:\mathtt{rel}_{2}\>X$ , we say that a unary relation $P:\mathtt{rel}_{1}\>X$ is $T$ -upward closed if $P$ is stable under direct $T$ -images. We define: $\mathtt{upclosed}\>{T}\,{P}\mathrel{{:}\!{=}}\forall x\,y,\,T\,x\,y\mathrel{% \rightarrow}P\,x\mathrel{\rightarrow}P\,y$ .

For instance, the finitary conjunction ${\textstyle{\wedge_{1}}}P$ is upward closed for permutations, formally stated as $\mathtt{upclosed}\>{(\cdot\mathrel{\sim_{p}}\cdot)}\,{{\textstyle{\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:\mathtt{rel}_{2}\>X$ and a unary relation $P:\mathtt{rel}_{1}\>X$ , we define the inductive $T$ -cover of $P$ , denoted $\mathtt{cover}\>{\,}T\,P:\mathtt{rel}_{1}\>X$ by the two following inductive rules:

Notice that $P\,x$ (resp. $T\,x\,y$ and $\mathtt{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 $\mathtt{cover}\>{T}\,P\,x$ . Also in [25], the constructor $[\mathtt{cover\texttt{\char 95\relax}stop}]$ (resp. $[\mathtt{cover\texttt{\char 95\relax}next}]$ ) is called reflexivity (resp. infinity).

The non-dependent induction principle (or eliminator, depending on your preferred terminology) generated for the $\mathtt{cover}\>{T}\,P$ predicate has the following type:

\mathtt{cover\texttt{\char 95\relax}ind}\leavevmode\nobreak\ T\,P:\leavevmode% \nobreak\ \forall Q^{\prime},\,P\subseteq Q^{\prime}\mathrel{\rightarrow}(% \forall x,\,T\,x\subseteq Q^{\prime}\mathrel{\rightarrow}Q^{\prime}\,x)% \mathrel{\rightarrow}(\forall x,\,\mathtt{cover}\>{T}\,P\,x\mathrel{% \rightarrow}Q^{\prime}\,x).

Informally, it states that $\mathtt{cover}\>{T}\,P$ is included in any unary relation $Q^{\prime}$ closed under the constructors/rules $[\mathtt{cover\texttt{\char 95\relax}stop}]$ and $[\mathtt{cover\texttt{\char 95\relax}next}]$ . Coq auto-generates a slight variant⁷⁷7namely of type $\forall Q^{\prime},\,P\subseteq Q^{\prime}\mathrel{\rightarrow}(\forall x,\,T% \,x\subseteq\mathtt{cover}\>{T}\,P\mathrel{\rightarrow}T\,x\subseteq Q^{\prime% }\mathrel{\rightarrow}Q^{\prime}\,x)\mathrel{\rightarrow}(\forall x,\,\mathtt{% cover}\>{T}\,P\,x\mathrel{\rightarrow}Q^{\prime}\,x)$ . of $\mathtt{cover\texttt{\char 95\relax}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 $\mathtt{cover\texttt{\char 95\relax}ind}$ as a guarded $\mathtt{Fixpoint}$ , similar to the auto-generated one.

Using the $\mathtt{cover\texttt{\char 95\relax}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 ( $\mathtt{cover\texttt{\char 95\relax}morphism}$ ).

Let $X, Y$ be two types, $R:\mathtt{rel}_{2}\>X$ and $T:\mathtt{rel}_{2}\>Y$ be binary relations, and $P:\mathtt{rel}_{1}\>X$ and $Q:\mathtt{rel}_{1}\>Y$ be unary relations. We further assume a map $f:Y\mathrel{\rightarrow}X$ which is supposed to be a morphism w.r.t. $P/Q$ and $R/T$ , i.e. satisfying

\forall y,\,P(f\,y)\mathrel{\rightarrow}Q\,y\qquad\text{and}\qquad\forall y_{1% }\,y_{2},\,T\,y_{1}\,y_{2}\mathrel{\rightarrow}R\,(f\,y_{1})\,(f\,y_{2}).

Then we have $\forall x\,y,\,x=f\,y\mathrel{\rightarrow}\mathtt{cover}\>{R}\,P\,x\mathrel{% \rightarrow}\mathtt{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 $\mathtt{cover\texttt{\char 95\relax}ind}$ , we exceptionally give a detailed account of the proof for the $\mathtt{cover\texttt{\char 95\relax}morphism}$ statement.

Proof.

We first reorder the hypotheses and the goal becomes $\forall x,\,\mathtt{cover}\>{R}\,P\,x\mathrel{\rightarrow}\forall y,\,x=f\,y% \mathrel{\rightarrow}\mathtt{cover}\>{T}\,Q\,y$ , which we prove by induction on $\mathtt{cover}\>{R}\,P\,x$ : we factor out $Q^{\prime}$ in the goal as $\forall x,\,\mathtt{cover}\>{R}\,P\,x\mathrel{\rightarrow}Q^{\prime}\,x$ with $Q^{\prime}\mathrel{{:}\!{=}}\lambda\,{x},\,{\forall y,\,x=f\,y\mathrel{% \rightarrow}\mathtt{cover}\>{T}\,Q\,y}$ . Reasoning backwards, we apply the instance $\mathtt{cover\texttt{\char 95\relax}ind}\leavevmode\nobreak\ R\,P\,Q^{\prime}$ to the goal, replacing it with two sub-goals:⁸⁸8factoring out $Q^{\prime}$ and applying $\mathtt{cover\texttt{\char 95\relax}ind}$ are automated for us by the Coq $\mathtt{induction}$ tactic.

$\blacksquare$

$P\subseteq Q^{\prime}$ : unfolding $Q^{\prime}$ , we assume $x$ s.t. $P\,x$ and $y$ s.t. $x=f\,y$ and we have to show $\mathtt{cover}\>{T}\,Q\,y$ . We derive $P(f\,y)$ by substitution and then $Q\,y$ using the left morphism hypothesis. We then derive $\mathtt{cover}\>{T}\,Q\,y$ using the constructor $[\mathtt{cover\texttt{\char 95\relax}stop}]$ ;
$\blacksquare$

$\forall x,\,(R\,x\subseteq Q^{\prime})\mathrel{\rightarrow}Q^{\prime}\,x$ : we assume $x$ s.t. $\mathit{IH}_{x}:\forall z,\,R\,x\,z\mathrel{\rightarrow}\forall y^{\prime},z=f% \,y^{\prime}\mathrel{\rightarrow}\mathtt{cover}\>{T}\,Q\,y^{\prime}$ (corresponding to the induction hypothesis) and $y$ s.t. $x=f\,y$ , and we have to show $\mathtt{cover}\>{T}\,Q\,y$ . We substitute $x$ with $f\,y$ in $\mathit{IH}_{x}$ and get $\mathit{IH}_{y}:\forall z,\,R\,(f\,y)\,z\mathrel{\rightarrow}\forall y^{\prime% },z=f\,y^{\prime}\mathrel{\rightarrow}\mathtt{cover}\>{T}\,Q\,y^{\prime}$ . Applying the second constructor $[\mathtt{cover\texttt{\char 95\relax}next}]$ , we replace the goal $\mathtt{cover}\>{T}\,Q\,y$ with $\forall z,\,T\,y\,z\mathrel{\rightarrow}\mathtt{cover}\>{T}\,Q\,z$ . Hence we assume $z$ s.t. $H_{yz}:T\,y\,z$ and we now have to show $\mathtt{cover}\>{T}\,Q\,z$ . Using the right morphism hypothesis, we derive $H^{\prime}_{yz}:R\,(f\,y)\,(f\,z)$ . We instantiate the induction hypothesis as $\mathit{IH}_{y}\leavevmode\nobreak\ (f\,z)\leavevmode\nobreak\ H^{\prime}_{yz}% \leavevmode\nobreak\ z\leavevmode\nobreak\ \mathtt{eq\texttt{\char 95\relax}refl}$ and get $\mathtt{cover}\>{T}\,Q\,z$ as desired. Notice that we use the reflexive identity for $\mathtt{eq\texttt{\char 95\relax}refl}:f\,z=f\,z$ .

This concludes the proof. Using standard automation for backward proof-search (the $\mathtt{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 $f\,y$ for $x$ . $\hfill\blacktriangleleft$

For the rest of the section, we assume a fixed type $X$ to be used as carrier for binary relations $R,T:\mathtt{rel}_{2}\>X$ and unary relations $P,Q:\mathtt{rel}_{1}\>X$ . The monotonicity of $\mathtt{cover}$ can be obtained as a particular case, using the identity morphism $f\mathrel{{:}\!{=}}\lambda\,{x},\,x$ . More precisely, $\mathtt{cover}\>{(\cdot)}\,(\cdot)$ is antitonic in its first argument and monotonic in its second argument:

\mathtt{cover\texttt{\char 95\relax}mono}\leavevmode\nobreak\ R\leavevmode% \nobreak\ T\,P\,Q:\leavevmode\nobreak\ T\subseteq R\mathrel{\rightarrow}P% \subseteq Q\mathrel{\rightarrow}\mathtt{cover}\>{R}\,P\subseteq\mathtt{cover}% \>{T}\,Q.

Additionally to be increasing (by $[\mathtt{cover\texttt{\char 95\relax}stop}]$ ) and monotonic (by $\mathtt{cover\texttt{\char 95\relax}mono}$ ), $\mathtt{cover}\>{T}$ is also an idempotent operator making it a closure operator:

\mathtt{cover\texttt{\char 95\relax}idempotent}\leavevmode\nobreak\ T\,P:% \leavevmode\nobreak\ \mathtt{cover}\>{T}\,(\mathtt{cover}\>{T}\,P)\subseteq% \mathtt{cover}\>{T}\,P.

Proof.

Assuming an arbitrary $x$ , the proof of $\mathtt{cover}\>{T}\,(\mathtt{cover}\>{T}\,P)\,x\mathrel{\rightarrow}\mathtt{% cover}\>{T}\,P\,x$ proceeds by induction on $\mathtt{cover}\>{T}\,(\mathtt{cover}\>{T}\,P)\,x$ . $\hfill\blacktriangleleft$ Then we get that the $\mathtt{cover}\>{T}$ operator preserves $T$ -upward closed unary relations:

\mathtt{cover\texttt{\char 95\relax}upclosed}\leavevmode\nobreak\ T\,P:% \leavevmode\nobreak\ \mathtt{upclosed}\>{T}\,{P}\mathrel{\rightarrow}\mathtt{% upclosed}\>{T}\,{(\mathtt{cover}\>{T}\,P)}.

Proof.

We assume $\mathtt{upclosed}\>{T}\,{P}$ and an arbitrary $x$ and show $\mathtt{cover}\>{T}\,P\,x\mathrel{\rightarrow}\forall y,\,T\,x\,y\mathrel{% \rightarrow}\mathtt{cover}\>{T}\,P\,y$ by induction on $\mathtt{cover}\>{T}\,P\,x$ . $\hfill\blacktriangleleft$

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 $\mathtt{cover}$ predicate is a generalization of the accessibility predicate, also called $R$ -founded in [25].

Definition 4 ( $\mathtt{acc}$ (essibility), $R$ -founded).

Given a binary relation $R:\mathtt{rel}_{2}\>X$ , the $\mathtt{acc}$ (essibility) predicate⁹⁹9The variant $\mathtt{Acc}$ as defined in the Coq standard library module $\mathtt{Prelude}$ , simply uses the reversed relation $R^{-1}$ instead of $R$ for $\mathtt{acc}$ . So we have $\mathtt{Acc}\>{R}\simeq\mathtt{acc}\>{R^{-1}}$ and $\mathtt{Acc}\>{R^{-1}}\simeq\mathtt{acc}\>{R}$ . for $R$ and the $R$ -founded predicate¹⁰¹⁰10 $R$ -founded is defined in [25, Definition 3.1]. are defined inductively, each with one single rule:

A simple observation shows that the shape of the constructor $[\mathtt{acc\texttt{\char 95\relax}intro}]$ is the same as the second constructor $[\mathtt{cover\texttt{\char 95\relax}next}]$ of the $\mathtt{cover}$ predicate. Furthermore, the first constructor $[\mathtt{cover\texttt{\char 95\relax}stop}]$ can be neutralized by setting $P$ as the empty relation $\emptyset\mathrel{{:}\!{=}}\lambda\,{\_},\,\bot$ . Hence we immediately derive the equivalence:

Proposition 5.

The $\mathtt{acc}$ (essibility) predicate is an instance of the $\mathtt{cover}$ predicate.

\mathtt{acc\texttt{\char 95\relax}iff\texttt{\char 95\relax}cover\texttt{\char 9% 5\relax}empty}\leavevmode\nobreak\ R\leavevmode\nobreak\ x:\leavevmode\nobreak% \ \mathtt{acc}\>{R}\leavevmode\nobreak\ x\mathrel{\,\leftrightarrow\,}\mathtt{% cover}\>{R}\leavevmode\nobreak\ \emptyset\leavevmode\nobreak\ x.

Moreover, accessible elements are necessarily irreflexive. Indeed, we show $\forall x,\,\mathtt{acc}\>{R}\,x\mathrel{\rightarrow}R\,x\,x\mathrel{% \rightarrow}\bot$ by induction on $\mathtt{acc}\>{R}\,x$ . Hence it follows that the left premise $\lnot R\,x\,x$ of the constructor of $R$ -founded is superfluous:

Proposition 6.

$R$ -founded and accessibility define equivalent notions:

\mathtt{founded\texttt{\char 95\relax}iff\texttt{\char 95\relax}acc}% \leavevmode\nobreak\ R\leavevmode\nobreak\ x:\leavevmode\nobreak\ \mathtt{% founded}\>R\,x\mathrel{\,\leftrightarrow\,}\mathtt{acc}\>R\,x.

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

3.3 Inductive cover and inductive bars

Let $X$ be a carrier type for lists. We consider unary relations on the type $\mathtt{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:\mathtt{rel}_{1}\>{(\mathtt{list}\,X)}$ be a unary relation on lists. We define the inductive $\mathtt{bar}\,P:\mathtt{rel}_{1}\>{(\mathtt{list}\,X)}$ unary relation with the two following inductive rules:

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 $[\mathtt{bar\texttt{\char 95\relax}next}]$ would be written

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 $\mathbin{::}$ . Another more important difference compared to [10, Definition 6] or else [29], is the absence of the inductive rule

in Definition 7. We discard rule $[\mathtt{bar\texttt{\char 95\relax}monotone}]$ because it is admissible for monotone unary relations on finite sequences.

Definition 8 (Monotone unary relation).

A unary relation $P:\mathtt{rel}_{1}\>{(\mathtt{list}\,X)}$ is monotone if it satisfies $\mathtt{monotone}\,{P}\mathrel{{:}\!{=}}\forall x\,l,\,P\,l\mathrel{% \rightarrow}P(x\mathbin{::}l)$ .

The (discarded) $[\mathtt{bar\texttt{\char 95\relax}monotone}]$ rule/constructor would ensure that $\mathtt{bar}\,P$ is a monotone predicate even when $P$ is not monotone. However, as an instance of $\mathtt{cover\texttt{\char 95\relax}upclosed}$ , if $P$ is monotone then so is $\mathtt{bar}\,P$ ; see $\mathtt{bar\texttt{\char 95\relax}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 $\mathtt{extends}:\mathtt{rel}_{2}\>{(\mathtt{list}\,X)}$ binary relation on lists is defined by the single inductive rule:

We could have used the first order characterization $\mathtt{extends}\leavevmode\nobreak\ l\leavevmode\nobreak\ m\mathrel{\,% \leftrightarrow\,}\exists x,\,m=x\mathbin{::}l$ to give an alternate definition of $\mathtt{extends}$ . With this notion, we get the equivalence

\mathtt{upclosed\texttt{\char 95\relax}extends\texttt{\char 95\relax}iff% \texttt{\char 95\relax}monotone}\leavevmode\nobreak\ P:\leavevmode\nobreak\ % \mathtt{upclosed}\>{\mathtt{extends}}\,{P}\mathrel{\,\leftrightarrow\,}\mathtt% {monotone}\,{P}

as an immediate consequence, but the specialization goes further:

Proposition 10 ( $\mathtt{bar\texttt{\char 95\relax}iff\texttt{\char 95\relax}cover\texttt{\char 9% 5\relax}extends}$ ).

Given a unary relation $P:\mathtt{rel}_{1}\>{(\mathtt{list}\,X)}$ and a list $l:\mathtt{list}\,X$ , we have the equivalence $\mathtt{bar}\,P\leavevmode\nobreak\ l\mathrel{\,\leftrightarrow\,}\mathtt{% cover}\>{\mathtt{extends}}\,P\leavevmode\nobreak\ l$ .

Thanks to Proposition 10 and $\mathtt{upclosed\texttt{\char 95\relax}extends\texttt{\char 95\relax}iff% \texttt{\char 95\relax}monotone}$ , the two below results are specializations of respectively $\mathtt{cover\texttt{\char 95\relax}upclosed}$ and $\mathtt{cover\texttt{\char 95\relax}mono}$ .

\begin{array}[]{@{}l@{~~}l@{}}\mathtt{bar\texttt{\char 95\relax}monotone}% \leavevmode\nobreak\ P:\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ &\mathtt% {monotone}\,{P}\mathrel{\rightarrow}\mathtt{monotone}\,{(\mathtt{bar}\,P)};\\ \mathtt{bar\texttt{\char 95\relax}mono}\leavevmode\nobreak\ P\leavevmode% \nobreak\ Q:\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ &P\subseteq Q% \mathrel{\rightarrow}\mathtt{bar}\,P\subseteq\mathtt{bar}\,Q.\end{array}

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):

\begin{array}[]{l@{~:~}l}\mathtt{xm}\hfil\leavevmode\nobreak\ :\leavevmode% \nobreak\ &\forall\,A:\mathbb{P},\,A\mathrel{\vee}\lnot A;\\ \mathtt{dc}\hfil\leavevmode\nobreak\ :\leavevmode\nobreak\ &\forall\,(A:% \mathtt{Type})\,(R:\mathtt{rel}_{2}\>A),\,(\forall a\exists b,\,R\,a\,b)% \mathrel{\rightarrow}\forall a\exists\rho:\mathbb{N}\mathrel{\rightarrow}A,\,% \rho_{0}=a\mathrel{\wedge}\forall n,\,R\leavevmode\nobreak\ \rho_{n}% \leavevmode\nobreak\ \rho_{1+n}.\\ \end{array}

The names of the results that depend on these added axioms are suffixed with $\mathtt{\texttt{\char 95\relax}XM}$ or $\mathtt{\texttt{\char 95\relax}DC}$ or both for an unambiguous exposition.

We start with the following definitions of the positive characterization $\mathtt{cover\texttt{\char 95\relax}pos}$ , the negative characterization $\mathtt{cover\texttt{\char 95\relax}neg}$ , and the sequential characterization $\mathtt{cover\texttt{\char 95\relax}seq}$ .

Definition 11 (Nonequivalent characterizations of cover).

\begin{array}[]{l@{~\cdef~}l}\mathtt{cover\texttt{\char 95\relax}pos}% \leavevmode\nobreak\ T\,P\leavevmode\nobreak\ x\hfil\leavevmode\nobreak\ % \mathrel{{:}\!{=}}\leavevmode\nobreak\ &\lambda\,{Q:\mathtt{rel}_{1}\>X},\,{P% \subseteq Q\mathrel{\rightarrow}(\forall y,\,T\,y\subseteq Q\mathrel{% \rightarrow}Q\,y)\mathrel{\rightarrow}Q\,x};\\ \mathtt{cover\texttt{\char 95\relax}neg}\leavevmode\nobreak\ T\,P\leavevmode% \nobreak\ x\hfil\leavevmode\nobreak\ \mathrel{{:}\!{=}}\leavevmode\nobreak\ &% \lambda\,{Q:\mathtt{rel}_{1}\>X},\,{Q\,x\mathrel{\rightarrow}(\forall y,\,Q\,y% \mathrel{\rightarrow}\exists z,\,Q\,z\mathrel{\wedge}T\,y\,z)\mathrel{% \rightarrow}\exists y,P\,y\mathrel{\wedge}Q\,y};\\ \mathtt{cover\texttt{\char 95\relax}seq}\leavevmode\nobreak\ T\,P\leavevmode% \nobreak\ x\hfil\leavevmode\nobreak\ \mathrel{{:}\!{=}}\leavevmode\nobreak\ &% \lambda\,{\rho:\mathbb{N}\mathrel{\rightarrow}X},\,{\rho_{0}=x\mathrel{% \rightarrow}(\forall n,\,T\,\rho_{n}\leavevmode\nobreak\ \rho_{1+n})\mathrel{% \rightarrow}\exists n,\,P\,\rho_{n}}.\\ \end{array}

Although not equivalent, the constructive strength of these characterizations can be compared: they are displayed from the strongest ( $\mathtt{cover\texttt{\char 95\relax}pos}$ ) to the weakest ( $\mathtt{cover\texttt{\char 95\relax}seq}$ ). Beware that both $Q$ and $\rho$ are universally quantified over in the characterizations below.

The positive characterization $\mathtt{cover\texttt{\char 95\relax}pos}$ is really just a reordering of the implications in the induction principle $\mathtt{cover\texttt{\char 95\relax}ind}$ , so we get the following equivalence purely constructively:

\mathtt{cover\texttt{\char 95\relax}iff\texttt{\char 95\relax}cover\texttt{% \char 95\relax}pos}\leavevmode\nobreak\ T\,P\leavevmode\nobreak\ x:\leavevmode% \nobreak\ \mathtt{cover}\>{T}\,P\,x\mathrel{\,\leftrightarrow\,}\forall Q,\,% \mathtt{cover\texttt{\char 95\relax}pos}\leavevmode\nobreak\ T\,P\leavevmode% \nobreak\ x\leavevmode\nobreak\ Q.

The positive characterization is constructively stronger that the negative one:

\mathtt{cover\texttt{\char 95\relax}pos\texttt{\char 95\relax}\texttt{\char 95% \relax}cover\texttt{\char 95\relax}neg}\leavevmode\nobreak\ T\,P\leavevmode% \nobreak\ x:\leavevmode\nobreak\ (\forall Q,\,\mathtt{cover\texttt{\char 95% \relax}pos}\leavevmode\nobreak\ T\,P\leavevmode\nobreak\ x\leavevmode\nobreak% \ Q)\mathrel{\rightarrow}(\forall Q,\,\mathtt{cover\texttt{\char 95\relax}neg}% \leavevmode\nobreak\ T\,P\leavevmode\nobreak\ x\leavevmode\nobreak\ Q).

Proof.

We use $\forall Q,\,\mathtt{cover\texttt{\char 95\relax}pos}\leavevmode\nobreak\ T\,P% \leavevmode\nobreak\ x\leavevmode\nobreak\ Q$ as the formulation of an induction principle. $\hfill\blacktriangleleft$ The negative characterization is constructively stronger than the sequential one. The below proof argument anticipates the intuition behind the definition of the negative characterization.

\mathtt{cover\texttt{\char 95\relax}neg\texttt{\char 95\relax}\texttt{\char 95% \relax}cover\texttt{\char 95\relax}seq}\leavevmode\nobreak\ T\,P\leavevmode% \nobreak\ x:\leavevmode\nobreak\ (\forall Q,\,\mathtt{cover\texttt{\char 95% \relax}neg}\leavevmode\nobreak\ T\,P\leavevmode\nobreak\ x\leavevmode\nobreak% \ Q)\mathrel{\rightarrow}(\forall\rho,\,\mathtt{cover\texttt{\char 95\relax}% seq}\leavevmode\nobreak\ T\,P\leavevmode\nobreak\ x\leavevmode\nobreak\ \rho).

Proof.

Assuming a $T$ -sequence $\rho:\mathbb{N}\mathrel{\rightarrow}X$ , we instantiate $Q$ with the direct image $\rho(\mathbb{N})\mathrel{{:}\!{=}}\lambda\,{y},\,{\exists n,\rho_{n}=y}$ . We show $\mathtt{cover\texttt{\char 95\relax}neg}\leavevmode\nobreak\ T\,P\leavevmode% \nobreak\ x\leavevmode\nobreak\ \rho(\mathbb{N})\mathrel{\rightarrow}\mathtt{% cover\texttt{\char 95\relax}seq}\leavevmode\nobreak\ T\,P\leavevmode\nobreak\ % x\leavevmode\nobreak\ \rho$ and conclude. $\hfill\blacktriangleleft$

We now explain the intuition behind those definitions by turning to a classical interpretation where all those characterizations are equivalent, discussing the precise roles played by XM and DC. The negative characterization $\mathtt{cover\texttt{\char 95\relax}neg}$ is central to our analysis and can be understood in two ways, either as deriving from $\mathtt{cover\texttt{\char 95\relax}pos}$ or generalizing $\mathtt{cover\texttt{\char 95\relax}seq}$ :

\blacksquare

The first understanding of $\mathtt{cover\texttt{\char 95\relax}neg}$ is as contrapositive form of $\mathtt{cover\texttt{\char 95\relax}pos}$ :

\mathtt{cover\texttt{\char 95\relax}pos\texttt{\char 95\relax}iff\texttt{\char 9% 5\relax}neg\texttt{\char 95\relax}XM}\leavevmode\nobreak\ T\,P\leavevmode% \nobreak\ x\leavevmode\nobreak\ Q:\mathtt{cover\texttt{\char 95\relax}pos}% \leavevmode\nobreak\ T\,P\leavevmode\nobreak\ x\leavevmode\nobreak\ Q\mathrel{% \,\leftrightarrow\,}\mathtt{cover\texttt{\char 95\relax}neg}\leavevmode% \nobreak\ T\,P\leavevmode\nobreak\ x\leavevmode\nobreak\ (\lnot Q).

The proof involves excluded middle but first-order De Morgan transformations are enough to get the equivalence.¹¹¹¹11In the Coq script, we insist on obtaining that equivalence via De Morgan rewriting and congruence only. The converse implication of $\mathtt{cover\texttt{\char 95\relax}pos\texttt{\char 95\relax}\texttt{\char 95% \relax}cover\texttt{\char 95\relax}neg}$ above is unlikely to be constructively provable (see Section 3.5), but it is a direct corollary to $\mathtt{cover\texttt{\char 95\relax}pos\texttt{\char 95\relax}iff\texttt{\char 9% 5\relax}cover\texttt{\char 95\relax}neg\texttt{\char 95\relax}XM}$ ,¹²¹²12see $\mathtt{cover\texttt{\char 95\relax}neg\texttt{\char 95\relax}\texttt{\char 95% \relax}cover\texttt{\char 95\relax}pos\texttt{\char 95\relax}XM}$ . however assuming XM as an added axiom;

$\blacksquare$

The second way to understand the negative characterization $\mathtt{cover\texttt{\char 95\relax}neg}$ is to view it as a generalization of the sequential characterization $\mathtt{cover\texttt{\char 95\relax}seq}$ . Notice that the statement $\forall\rho,\,\mathtt{cover\texttt{\char 95\relax}seq}\leavevmode\nobreak\ T\,% P\leavevmode\nobreak\ x\leavevmode\nobreak\ \rho$ is the usual intuitive definition of being a $T$ -cover for $P$ :

Any infinite $T$ -sequence starting at $x$ meets $P$ .¹³¹³13Such formulation are more commonly found for the “intuitive” (read sequential) definition of “being a bar for $P$ ” [6]. See $\mathtt{bar\texttt{\char 95\relax}sequences}$ in Section 3.5 for the corresponding specialization.

However this interpretation depends on what are the inhabitants of the type $\mathbb{N}\mathrel{\rightarrow}X$ of which $\rho$ is a member; see Section 3.5. In the proof of $\mathtt{cover\texttt{\char 95\relax}neg\texttt{\char 95\relax}\texttt{\char 95% \relax}cover\texttt{\char 95\relax}seq}$ , we used the direct image $\rho(\mathbb{N})$ as a particular instance of $Q$ in $\mathtt{cover\texttt{\char 95\relax}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}\mathrel{\rightarrow}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,\,Q\,y\mathrel{\rightarrow}\exists z,\,Q\,z\mathrel{\wedge}T\,y\,z$ 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{array}[]{@{}l@{~}l@{}}\mathtt{cover\texttt{\char 95\relax}negative}% \leavevmode\nobreak\ T\,P\leavevmode\nobreak\ x:\hfil\leavevmode\nobreak\ &% \mathtt{cover}\>{T}\,P\leavevmode\nobreak\ x\mathrel{\rightarrow}\forall Q,\,Q% \,x\mathrel{\rightarrow}(\forall y,\,Q\,y\mathrel{\rightarrow}\exists z,\,Q\,z% \mathrel{\wedge}T\,y\,z)\mathrel{\rightarrow}\exists y,P\,y\mathrel{\wedge}Q\,% y\\ \mathtt{cover\texttt{\char 95\relax}sequences}\leavevmode\nobreak\ T\,P% \leavevmode\nobreak\ x:\hfil\leavevmode\nobreak\ &\mathtt{cover}\>{T}\,P% \leavevmode\nobreak\ x\mathrel{\rightarrow}\forall\rho,\,\rho_{0}=x\mathrel{% \rightarrow}(\forall n,\,T\,\rho_{n}\leavevmode\nobreak\ \rho_{1+n})\mathrel{% \rightarrow}\exists n,\,P\,\rho_{n}\end{array}

If one is interested in the converse implications, then, on the one hand, XM would be used to prove that $\forall Q,\,\mathtt{cover\texttt{\char 95\relax}neg}\leavevmode\nobreak\ T\,P% \leavevmode\nobreak\ x\leavevmode\nobreak\ Q$ implies $\mathtt{cover}\>{T}\,P\leavevmode\nobreak\ x$ . On the other hand, to recover $\forall Q,\,\mathtt{cover\texttt{\char 95\relax}neg}\leavevmode\nobreak\ T\,P% \leavevmode\nobreak\ x\leavevmode\nobreak\ Q$ from $\forall\rho,\,\mathtt{cover\texttt{\char 95\relax}seq}\leavevmode\nobreak\ T\,% P\leavevmode\nobreak\ x\leavevmode\nobreak\ \rho$ , one uses $\mathtt{DC}\leavevmode\nobreak\ \{x\mid Q\,x\}$ which is dependent choice specialized on the $\Sigma$ -type $\{x\mid Q\,x\}$ where $Q:\mathtt{rel}_{1}\>X$ . Indeed, the statement of $\mathtt{DC}\leavevmode\nobreak\ X$ , i.e. dependent choice specialized on type $X$ is:

\mathtt{DC}\leavevmode\nobreak\ X\mathrel{{:}\!{=}}\forall\,R:\mathtt{rel}_{2}% \>X,\,(\forall x\exists y,\,R\,x\,y)\mathrel{\rightarrow}\forall x\exists\rho:% \mathbb{N}\mathrel{\rightarrow}X,\,\rho_{0}=x\mathrel{\wedge}\forall n,\,R% \leavevmode\nobreak\ \rho_{n}\leavevmode\nobreak\ \rho_{1+n}.

When $Q:\mathtt{rel}_{1}\>X$ , we reformulate the instance $\mathtt{DC}\leavevmode\nobreak\ \{x\mid Q\,x\}$ as¹⁴¹⁴14see $\mathtt{DC\texttt{\char 95\relax}sig\texttt{\char 95\relax}\texttt{\char 95% \relax}DC\texttt{\char 95\relax}}$ $\Sigma$ in the Coq code.

\forall R,\,(\forall x,\,Q\,x\mathrel{\rightarrow}\exists y,\,Q\,y\mathrel{% \wedge}R\,x\,y)\mathrel{\rightarrow}\forall x,\,Q\,x\mathrel{\rightarrow}% \exists\rho,\,\rho_{0}=x\mathrel{\wedge}\forall n,\,Q\,\rho_{n}\mathrel{\wedge% }R\leavevmode\nobreak\ \rho_{n}\leavevmode\nobreak\ \rho_{1+n}

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

\mathtt{cover\texttt{\char 95\relax}seq\texttt{\char 95\relax}\texttt{\char 95% \relax}cover\texttt{\char 95\relax}neg\texttt{\char 95\relax}DC}\leavevmode% \nobreak\ T\,P\leavevmode\nobreak\ x:(\forall\rho,\,\mathtt{cover\texttt{\char 9% 5\relax}seq}\leavevmode\nobreak\ T\,P\leavevmode\nobreak\ x\leavevmode\nobreak% \ \rho)\mathrel{\rightarrow}(\forall Q,\,\mathtt{cover\texttt{\char 95\relax}% neg}\leavevmode\nobreak\ T\,P\leavevmode\nobreak\ x\leavevmode\nobreak\ Q).

Theorem 12 (in the spirit of Brouwer’s bar theorem).

Assuming $\mathtt{xm}$ and $\mathtt{dc}$ , the inductive and the sequential characterizations of covering are equivalent:

\mathtt{cover}\>{T}\,P\leavevmode\nobreak\ x\leavevmode\nobreak\ \mathrel{\,% \leftrightarrow\,}\leavevmode\nobreak\ \forall\rho,\rho_{0}=x\mathrel{% \rightarrow}(\forall n,\,T\,\rho_{n}\leavevmode\nobreak\ \rho_{1+n})\mathrel{% \rightarrow}\exists n,\,P\,\rho_{n}.

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:\mathtt{rel}_{1}\>{(\mathtt{list}\,\mathbb{N})},\,\mathtt{bar}% \leavevmode\nobreak\ P\leavevmode\nobreak\ {[\mskip 1.0mu]}\mathrel{\,% \leftrightarrow\,}\forall\alpha:\mathbb{N}\mathrel{\rightarrow}\mathbb{N},\,% \exists n,\,P\,[\alpha_{n-1};\ldots;\alpha_{0}].

The bar theorem statement is an instance of Theorem 12 where $T\mathrel{{:}\!{=}}\mathtt{extends}$ . Indeed, an $\mathtt{extends}$ -sequence of lists in $\mathbb{N}\mathrel{\rightarrow}\mathtt{list}\,X$ corresponds to the $n$ -prefixes of a sequence $\mathbb{N}\mathrel{\rightarrow}X$ ; see $\mathtt{Brouwer\texttt{\char 95\relax}bar\texttt{\char 95\relax}XM\texttt{% \char 95\relax}DC}$ in the Coq code.

3.5 Discussion

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

\begin{array}[]{l@{~~}l}\mathtt{acc\texttt{\char 95\relax}negative}\leavevmode% \nobreak\ x:\hfil\leavevmode\nobreak\ \leavevmode\nobreak\ &\mathtt{acc}\>{R}% \leavevmode\nobreak\ x\mathrel{\rightarrow}\forall Q,\,Q\,x\mathrel{% \rightarrow}(\forall y,\,Q\,y\mathrel{\rightarrow}\exists z,\,Q\,z\mathrel{% \wedge}R\,y\,z)\mathrel{\rightarrow}\bot;\\ \mathtt{acc\texttt{\char 95\relax}sequences}\leavevmode\nobreak\ x:\hfil% \leavevmode\nobreak\ \leavevmode\nobreak\ &\mathtt{acc}\>{R}\leavevmode% \nobreak\ x\mathrel{\rightarrow}\forall\rho,\,\rho_{0}=x\mathrel{\rightarrow}(% \forall n,\,R\leavevmode\nobreak\ \rho_{n}\leavevmode\nobreak\ \rho_{1+n})% \mathrel{\rightarrow}\bot;\\[4.30554pt] \mathtt{bar\texttt{\char 95\relax}negative}:\hfil\leavevmode\nobreak\ % \leavevmode\nobreak\ &\mathtt{bar}\leavevmode\nobreak\ P\leavevmode\nobreak\ {% [\mskip 1.0mu]}\mathrel{\rightarrow}\forall Q,\,Q\,{[\mskip 1.0mu]}\mathrel{% \rightarrow}\bigl{(}\forall l,\,Q\,l\mathrel{\rightarrow}\exists x,\,Q\,(x% \mathbin{::}l)\bigr{)}\mathrel{\rightarrow}\exists l,P\,l\mathrel{\wedge}Q\,l;% \\ \mathtt{bar\texttt{\char 95\relax}sequences}:\hfil\leavevmode\nobreak\ % \leavevmode\nobreak\ &\mathtt{bar}\leavevmode\nobreak\ P\leavevmode\nobreak\ {% [\mskip 1.0mu]}\mathrel{\rightarrow}\forall\alpha,\exists n,\,P\,[\alpha_{n-1}% ;\ldots;\alpha_{0}].\end{array}

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}\mathrel{\rightarrow}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}\mathrel{\rightarrow}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 $\mathtt{bar}\leavevmode\nobreak\ P\leavevmode\nobreak\ {[\mskip 1.0mu]}$ 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}\mathrel{\rightarrow}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},\ldots$ 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 bars [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:\mathtt{rel}_{2}\>X$ . We extend the binary relation $T$ to lists (viewed as finite sets), as ${T}^{\dagger}:\mathtt{rel}_{2}\>{(\mathtt{list}\,X)}$ using the direct image and this way, we can view FANs over $T$ as ${T}^{\dagger}$ -sequences over finite sets.

4.1 Lifting a relation to finite sets

We define the finitary image relation on $\mathtt{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}:\mathtt{rel}_{2}\>{(\mathtt{list}\,X)}$ , by ${T}^{\dagger}\mathrel{{:}\!{=}}\lambda\,{l\,m},\,{\forall y,\,y\in m\mathrel{% \rightarrow}\exists x,\,x\in l\mathrel{\wedge}T\,x\,y}$ , i.e. ${T}^{\dagger}\,l\,m$ 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}\mathrel{\rightarrow}m_{2}\subseteq m_{1}\mathrel{% \rightarrow}{T}^{\dagger}\leavevmode\nobreak\ l_{1}\leavevmode\nobreak\ m_{1}% \mathrel{\rightarrow}{T}^{\dagger}\leavevmode\nobreak\ l_{2}\leavevmode% \nobreak\ 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:

\begin{array}[]{@{}c@{}}\mathtt{fimage\texttt{\char 95\relax}split\texttt{% \char 95\relax}inv}\leavevmode\nobreak\ l_{1}\leavevmode\nobreak\ l_{2}% \leavevmode\nobreak\ m:\leavevmode\nobreak\ {T}^{\dagger}\leavevmode\nobreak\ % (l_{1}\mathbin{{+\mskip-10.0mu+}}l_{2})\leavevmode\nobreak\ m\mathrel{% \rightarrow}\exists\,m_{1}\,m_{2},\,m\mathrel{\sim_{p}}m_{1}\mathbin{{+\mskip-% 10.0mu+}}m_{2}\mathrel{\wedge}{T}^{\dagger}\leavevmode\nobreak\ l_{1}% \leavevmode\nobreak\ m_{1}\mathrel{\wedge}{T}^{\dagger}\leavevmode\nobreak\ l_% {2}\leavevmode\nobreak\ m_{2}\end{array}

which we show by induction on $m$ . Additionally, we show that ${T}^{\dagger}\leavevmode\nobreak\ ({\cdot})\leavevmode\nobreak\ k$ is upward closed for permutations for any $k$ , which can be written as $\mathtt{upclosed}\>{({\cdot}\mathrel{\sim_{p}}{\cdot})}\,{({T}^{\dagger}% \leavevmode\nobreak\ {\cdot}\leavevmode\nobreak\ k)}$ . And to conclude this section, if $P$ is upward closed for $T$ then the finitary conjunction ${\textstyle{\wedge_{1}}}P$ of $P$ (over lists) is upward closed for ${T}^{\dagger}$ , i.e. $\mathtt{upclosed}\>{T}\,{P}\mathrel{\rightarrow}\mathtt{upclosed}\>{{T}^{% \dagger}}\,{{\textstyle{\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:\mathtt{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 ${\textstyle{\wedge_{1}}}P$ , i.e.

\mathtt{FAN\texttt{\char 95\relax}cover}:\leavevmode\nobreak\ \mathtt{upclosed% }\>{T}\,{P}\mathrel{\rightarrow}\forall x,\,\mathtt{cover}\>{T}\,P\leavevmode% \nobreak\ x\mathrel{\rightarrow}\mathtt{cover}\>{{T}^{\dagger}}\leavevmode% \nobreak\ {\textstyle{\wedge_{1}}}P\leavevmode\nobreak\ {[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 ${\textstyle{\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 $\mathtt{upclosed}\>{T}\,{P}$ . We first show that $\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P$ is upward closed for permutations, stated as $\mathtt{upclosed}\>{({\cdot}\mathrel{\sim_{p}}{\cdot})}\,{(\mathtt{cover}\>{{T% }^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P)}$ . For this, we prove $\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P% \leavevmode\nobreak\ l\mathrel{\rightarrow}\forall m,\,l\mathrel{\sim_{p}}m% \mathrel{\rightarrow}\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {% \textstyle{\wedge_{1}}}P\leavevmode\nobreak\ m$ by induction on $\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P% \leavevmode\nobreak\ l$ .

Now, we establish the key result that $\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P$ is stable under (binary) union, herein represented by the append operation on lists:

\mathtt{cover\texttt{\char 95\relax}fimage\texttt{\char 95\relax}union}% \leavevmode\nobreak\ l\leavevmode\nobreak\ m:\leavevmode\nobreak\ \mathtt{% cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P% \leavevmode\nobreak\ l\mathrel{\rightarrow}\mathtt{cover}\>{{T}^{\dagger}}% \leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P\leavevmode\nobreak\ m\mathrel{% \rightarrow}\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{% \wedge_{1}}}P\leavevmode\nobreak\ (l\mathbin{{+\mskip-10.0mu+}}m).

The proof proceeds by nested induction, first on $\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P% \leavevmode\nobreak\ l$ and then on $\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P% \leavevmode\nobreak\ m$ , with a critical use of $\mathtt{fimage\texttt{\char 95\relax}split\texttt{\char 95\relax}inv}$ to invert two statements of shape ${T}^{\dagger}\leavevmode\nobreak\ (\cdot\mathbin{{+\mskip-10.0mu+}}\cdot)% \leavevmode\nobreak\ (\cdot)$ where the first argument of ${T}^{\dagger}$ is a union of lists. As a corollary of $\mathtt{cover\texttt{\char 95\relax}fimage\texttt{\char 95\relax}union}$ , we get the specialization where $l\mathrel{{:}\!{=}}{[x]}$ is a singleton as

\forall\,x\,m,\,\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {% \textstyle{\wedge_{1}}}P\leavevmode\nobreak\ {[x]}\mathrel{\rightarrow}\mathtt% {cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P% \leavevmode\nobreak\ m\mathrel{\rightarrow}\mathtt{cover}\>{{T}^{\dagger}}% \leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P\leavevmode\nobreak\ (x\mathbin{% ::}m)

and then, as a direct consequence

\mathtt{cover\texttt{\char 95\relax}fimage\texttt{\char 95\relax}Forall}% \leavevmode\nobreak\ l:\leavevmode\nobreak\ \bigl{(}\forall x,\,x\in l\mathrel% {\rightarrow}\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{% \wedge_{1}}}P\leavevmode\nobreak\ {[x]}\bigr{)}\mathrel{\rightarrow}\mathtt{% cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P% \leavevmode\nobreak\ l

for which we proceed by induction on $l$ .

We can conclude with the proof of the FAN theorem for inductive covers. We establish $\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P% \leavevmode\nobreak\ {[x]}$ , reasoning by induction on $\mathtt{cover}\>{T}\,P\leavevmode\nobreak\ x$ :

$\blacksquare$

the base case where $P\,x$ holds is trivially solved by giving a proof of ${\textstyle{\wedge_{1}}}P\leavevmode\nobreak\ {[x]}$ and then deriving $\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P% \leavevmode\nobreak\ {[x]}$ with an instance of first constructor $[\mathtt{cover\texttt{\char 95\relax}stop}]$ ;
$\blacksquare$

in the recursive case where $\forall y,\,T\,x\,y\mathrel{\rightarrow}\mathtt{cover}\>{{T}^{\dagger}}% \leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P\leavevmode\nobreak\ {[y]}$ is the induction hypothesis, we show $\forall l,\,{T}^{\dagger}\leavevmode\nobreak\ {[x]}\leavevmode\nobreak\ l% \mathrel{\rightarrow}\forall y,\,y\in l\mathrel{\rightarrow}\mathtt{cover}\>{{% T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P\leavevmode\nobreak% \ {[y]}$ and then combine this with $\mathtt{cover\texttt{\char 95\relax}fimage\texttt{\char 95\relax}Forall}$ and an instance of the second constructor $[\mathtt{cover\texttt{\char 95\relax}next}]$ .

This concludes our proof of the FAN theorem for inductive covers. $\hfill\blacktriangleleft$

We can immediately derive ${\textstyle{\wedge_{1}}}{(\mathtt{cover}\>{T}\,P)}\leavevmode\nobreak\ l% \mathrel{\rightarrow}\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {{% \textstyle{\wedge_{1}}}P}\leavevmode\nobreak\ l$ by induction on $l$ and then the following characterization of covering for the finitary image:

\mathtt{cover\texttt{\char 95\relax}fimage\texttt{\char 95\relax}iff}:% \leavevmode\nobreak\ \mathtt{upclosed}\>{T}\,{P}\mathrel{\rightarrow}\forall l% ,\,\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {{\textstyle{\wedge_{1}% }}P}\leavevmode\nobreak\ l\mathrel{\,\leftrightarrow\,}(\forall x,\,x\in l% \mathrel{\rightarrow}\mathtt{cover}\>{T}\,P\leavevmode\nobreak\ x).

i.e. the list $l$ is ${T}^{\dagger}$ -covered for ${\textstyle{\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 $\mathtt{list}\,X$ and $\mathtt{list}\,(\mathtt{list}\,X)$ . For $lc:\mathtt{list}\,(\mathtt{list}\,X)$ , let us first define the

\mathtt{FAN}\leavevmode\nobreak\ lc\mathrel{{:}\!{=}}\lambda\,{l},\,{{% \textstyle{\wedge_{2}}}{(\cdot\in\cdot)}\leavevmode\nobreak\ l\leavevmode% \nobreak\ lc}

i.e. if written as $l=[x_{1};\ldots;x_{n}]$ and $lc=[c_{1};\ldots;c_{p}]$ , $\mathtt{FAN}\leavevmode\nobreak\ lc\leavevmode\nobreak\ l$ means $n=p$ and $x_{1}\in c_{1},x_{2}\in c_{2},\ldots,x_{n}\in c_{n}$ . Stated in plain english, $l$ is a list of one-to-one choices for the choice list $l c$ ; see the inductive definition of ${\textstyle{\wedge_{2}}}R$ in Section 2. Using generic tools designed for the $\mathtt{finite}$ abstraction, we can show that $\mathtt{FAN}\leavevmode\nobreak\ lc$ is a finite, i.e.

\mathtt{FAN\texttt{\char 95\relax}finite}\leavevmode\nobreak\ lc:\leavevmode% \nobreak\ \mathtt{finite}\,{(\mathtt{FAN}\leavevmode\nobreak\ lc)}.

However in [10, page 102], the author gives a specific construction of a list which collects the lists of choices $l$ s.t. $\mathtt{FAN}\leavevmode\nobreak\ lc\leavevmode\nobreak\ l$ , that we denote $\mathtt{list\texttt{\char 95\relax}fan}\leavevmode\nobreak\ lc$ herein, satisfying:

\mathtt{list\texttt{\char 95\relax}fan\texttt{\char 95\relax}spec}\leavevmode% \nobreak\ lc:\leavevmode\nobreak\ \forall l,\,\mathtt{FAN}\leavevmode\nobreak% \ lc\leavevmode\nobreak\ l\mathrel{\,\leftrightarrow\,}l\in\mathtt{list\texttt% {\char 95\relax}fan}\leavevmode\nobreak\ lc.

Thus the dependent pair $(\mathtt{list\texttt{\char 95\relax}fan}\leavevmode\nobreak\ lc,\mathtt{list% \texttt{\char 95\relax}fan\texttt{\char 95\relax}spec}\leavevmode\nobreak\ lc)$ is an (explicitly given) proof of the proposition $\mathtt{finite}\,{(\mathtt{FAN}\leavevmode\nobreak\ lc)}$ . The value of $\mathtt{list\texttt{\char 95\relax}fan}\leavevmode\nobreak\ lc$ can be viewed as a generalization of the exponential function to lists, computing the list of choice sequences for $l c$ .

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

Theorem 15 (reminder of Theorem 6 of [10]).

Let $P:\mathtt{rel}_{1}\>{(\mathtt{list}\,X)}$ be unary relation. The following statement holds: $\mathtt{monotone}\,{P}\mathrel{\rightarrow}\mathtt{bar}\leavevmode\nobreak\ P% \leavevmode\nobreak\ {[\mskip 1.0mu]}\mathrel{\rightarrow}\mathtt{bar}% \leavevmode\nobreak\ \bigl{(}\lambda\,{lc},\,{{\textstyle{\wedge_{1}}}P\,(% \mathtt{list\texttt{\char 95\relax}fan}\leavevmode\nobreak\ lc)}\bigr{)}% \leavevmode\nobreak\ {[\mskip 1.0mu]}$ .

Proof.

We first reformulate the result as

\mathtt{FAN\texttt{\char 95\relax}bar}\leavevmode\nobreak\ P:\leavevmode% \nobreak\ \mathtt{monotone}\,{P}\mathrel{\rightarrow}\mathtt{bar}\leavevmode% \nobreak\ P\leavevmode\nobreak\ {[\mskip 1.0mu]}\mathrel{\rightarrow}\mathtt{% bar}\leavevmode\nobreak\ (\lambda\,{lc},\,{\mathtt{FAN}\leavevmode\nobreak\ lc% \subseteq P})\leavevmode\nobreak\ {[\mskip 1.0mu]}

which is an equivalent statement thanks to the monotonicity $\mathtt{bar\texttt{\char 95\relax}mono}$ of the $\mathtt{bar}$ predicate. Indeed, using $\mathtt{list\texttt{\char 95\relax}fan\texttt{\char 95\relax}spec}$ , we get the equivalence ${\textstyle{\wedge_{1}}}P\,(\mathtt{list\texttt{\char 95\relax}fan}\leavevmode% \nobreak\ lc)\mathrel{\,\leftrightarrow\,}\mathtt{FAN}\leavevmode\nobreak\ lc\subseteq P$ for any $l c$ . Now the statement $\mathtt{FAN\texttt{\char 95\relax}bar}\,P$ is independent of the implementation of $\mathtt{list\texttt{\char 95\relax}fan}$ .

Using the results of Section 3.3, we replace the hypotheses $\mathtt{monotone}\,{P}$ and $\mathtt{bar}\leavevmode\nobreak\ P\leavevmode\nobreak\ {[\mskip 1.0mu]}$ by $\mathtt{upclosed}\>{\,\mathtt{extends}}\,{P}$ and $\mathtt{cover}\>{\,\mathtt{extends}}\leavevmode\nobreak\ P\leavevmode\nobreak% \ {[\mskip 1.0mu]}$ , and the goal $\mathtt{bar}\leavevmode\nobreak\ (\lambda\,{lc},\,{\mathtt{FAN}\leavevmode% \nobreak\ lc\subseteq P})\leavevmode\nobreak\ {[\mskip 1.0mu]}$ becomes $\mathtt{cover}\>{\,\mathtt{extends}}\leavevmode\nobreak\ (\lambda\,{lc},\,{% \mathtt{FAN}\leavevmode\nobreak\ lc\subseteq P})\leavevmode\nobreak\ {[\mskip 1% .0mu]}$ . Hence, by Theorem 14 we get $\mathtt{cover}\>{{\mathtt{extends}}^{\dagger}}\leavevmode\nobreak\ {\textstyle% {\wedge_{1}}}P\leavevmode\nobreak\ {[{[\mskip 1.0mu]}]}$ . Then we transfer the inductive cover using $\mathtt{list\texttt{\char 95\relax}fan}$ as a morphism (Proposition 3):

\mathtt{cover}\>{{\mathtt{extends}}^{\dagger}}\leavevmode\nobreak\ {\textstyle% {\wedge_{1}}}P\leavevmode\nobreak\ {[{[\mskip 1.0mu]}]}\mathrel{\rightarrow}% \mathtt{cover}\>{\mathtt{extends}}\leavevmode\nobreak\ (\lambda\,{lc},\,{% \mathtt{FAN}\leavevmode\nobreak\ lc\subseteq P})\leavevmode\nobreak\ {[\mskip 1% .0mu]}

after having checked that the following statements hold: ${[{[\mskip 1.0mu]}]}=\mathtt{list\texttt{\char 95\relax}fan}\leavevmode% \nobreak\ {[\mskip 1.0mu]}$ , $\mathtt{extends}\leavevmode\nobreak\ l\leavevmode\nobreak\ m\mathrel{% \rightarrow}{\mathtt{extends}}^{\dagger}\leavevmode\nobreak\ (\mathtt{list% \texttt{\char 95\relax}fan}\,l)\leavevmode\nobreak\ (\mathtt{list\texttt{\char 9% 5\relax}fan}\,m)$ and ${\textstyle{\wedge_{1}}}P\leavevmode\nobreak\ (\mathtt{list\texttt{\char 95% \relax}fan}\leavevmode\nobreak\ lc)\mathrel{\rightarrow}\mathtt{FAN}% \leavevmode\nobreak\ lc\subseteq P$ . $\hfill\blacktriangleleft$

Theorem 6 of [10] (cf. Theorem 15), and its original proof, even though it uses one particular implementation of $\mathtt{list\texttt{\char 95\relax}fan}$ both in the proved statement and inside the arguments, can be adapted to work for any implementation of $\mathtt{list\texttt{\char 95\relax}fan}$ as soon as it satisfies $\mathtt{list\texttt{\char 95\relax}fan\texttt{\char 95\relax}spec}$ . The reason is that we pass through $\mathtt{FAN\texttt{\char 95\relax}bar}$ which is independent of the actual implementation of $\mathtt{list\texttt{\char 95\relax}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 $\mathtt{bar}$ s under binary intersection [10, Proposition 3]:

\mathtt{monotone}\,{P}\mathrel{\rightarrow}\mathtt{monotone}\,{Q}\mathrel{% \rightarrow}\mathtt{bar}\leavevmode\nobreak\ P\leavevmode\nobreak\ l\mathrel{% \rightarrow}\mathtt{bar}\leavevmode\nobreak\ Q\leavevmode\nobreak\ l\mathrel{% \rightarrow}\mathtt{bar}\leavevmode\nobreak\ (P\cap Q)\leavevmode\nobreak\ l

which is there established by nested inductions on $\mathtt{bar}\leavevmode\nobreak\ P\leavevmode\nobreak\ l$ , and then on $\mathtt{bar}\leavevmode\nobreak\ Q\leavevmode\nobreak\ l$ . On the contrary, the core argument in the proof of Theorem 14 lies in $\mathtt{cover\texttt{\char 95\relax}fimage\texttt{\char 95\relax}union}$ , i.e. the closure of $\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\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:\mathtt{rel}_{2}\>X$ and $P:\mathtt{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:\mathtt{rel}_{2}\>X$ , the paths in $T$ are described by a ternary relation $\mathtt{path}\leavevmode\nobreak\ {T}:X\mathrel{\rightarrow}\mathtt{list}\,X% \mathrel{\rightarrow}X\mathrel{\rightarrow}\mathbb{P}$ defined by two inductive rules:

Intuitively, $\mathtt{path}\leavevmode\nobreak\ {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:

\mathtt{upclosed\texttt{\char 95\relax}path}\leavevmode\nobreak\ T\,P:\mathtt{% upclosed}\>{T}\,{P}\mathrel{\rightarrow}\mathtt{upclosed}\>{(\lambda\,{x\,y},% \,{\exists p,\,\mathtt{path}\leavevmode\nobreak\ {T}\leavevmode\nobreak\ x% \leavevmode\nobreak\ p\leavevmode\nobreak\ y)}}\,{P}.

Definition 17 (Inductive rose tree).

The type of $X$ -indexed rose trees denoted $\mathtt{tree}\,{X}:\mathtt{Type}$ is inductively defined by a single rule:

where we denote ${\langle{x}|{l}\rangle}$ as a shortcut for $(\mathtt{node}\leavevmode\nobreak\ x\leavevmode\nobreak\ l)$ . The root of $t={\langle{x}|{l}\rangle}$ is indexed by $x$ and we write $\mathtt{root}\,{t}=x$ , and $l$ is the list of the sons of $t$ . We define the height of a rose tree, denoted $\mathtt{tree\texttt{\char 95\relax}ht}:\mathtt{tree}\,{X}\mathrel{\rightarrow}% \mathbb{N}$ , using the fixpoint equation $\mathtt{tree\texttt{\char 95\relax}ht}\>{{\langle{x}|{[t_{1};\ldots;t_{n}]}% \rangle}}=1+\mathtt{list\texttt{\char 95\relax}max}\>[\mathtt{tree\texttt{% \char 95\relax}ht}\>t_{1};\ldots;\mathtt{tree\texttt{\char 95\relax}ht}\>t_{n}]$ .

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

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 $\mathtt{branch}\leavevmode\nobreak\ t\leavevmode\nobreak\ p\leavevmode\nobreak\ 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:\mathtt{rel}_{2}\>X$ rooted at $x$ of which the paths from $x$ satisfy the property $P:\mathtt{list}\,X\mathrel{\rightarrow}X\mathrel{\rightarrow}\mathbb{P}$ .

Definition 18 (Representation).

Assume a binary relation $T:\mathtt{rel}_{2}\>X$ , a property for paths $P:\mathtt{list}\,X\mathrel{\rightarrow}X\mathrel{\rightarrow}\mathbb{P}$ and a point $x : X$ . We say that $P$ in $T$ at $x$ is strongly represented by $t:\mathtt{tree}\,{X}$ and write $\mathtt{strongly\texttt{\char 95\relax}represents}\leavevmode\nobreak\ T\,P\,x\>t$ if:

\mathtt{strongly\texttt{\char 95\relax}represents}\leavevmode\nobreak\ T\,P\,x% \leavevmode\nobreak\ t\mathrel{{:}\!{=}}\mathtt{root}\,{t}=x\mathrel{\wedge}% \forall\,p\,y,\,\mathtt{branch}\leavevmode\nobreak\ t\leavevmode\nobreak\ p% \leavevmode\nobreak\ y\mathrel{\,\leftrightarrow\,}\mathtt{path}\leavevmode% \nobreak\ {T}\leavevmode\nobreak\ x\leavevmode\nobreak\ p\leavevmode\nobreak\ % y\mathrel{\wedge}P\leavevmode\nobreak\ p\leavevmode\nobreak\ y.

We say that $P$ in $T$ at $x : X$ is represented by $t:\mathtt{tree}\,{X}$ and write $\mathtt{represents}\leavevmode\nobreak\ T\,P\,x\>t$ if:

\mathtt{represents}\leavevmode\nobreak\ T\,P\,x\leavevmode\nobreak\ t\mathrel{% {:}\!{=}}\mathtt{root}\,{t}=x\mathrel{\wedge}\forall\,p\,y,\,P\,p\,y\mathrel{% \rightarrow}(\mathtt{branch}\leavevmode\nobreak\ t\leavevmode\nobreak\ p% \leavevmode\nobreak\ y\mathrel{\,\leftrightarrow\,}\mathtt{path}\leavevmode% \nobreak\ {T}\leavevmode\nobreak\ x\leavevmode\nobreak\ p\leavevmode\nobreak\ % 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 $\mathtt{strongly\texttt{\char 95\relax}represents}\leavevmode\nobreak\ T\,P\,x% \>t\mathrel{\rightarrow}\mathtt{represents}\leavevmode\nobreak\ 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,¹⁵¹⁵15i.e. $\forall\,x\,y:X,\,x=y\mathrel{\vee}x\not=y$ . e.g. when $X=\mathbb{N}$ , then both $\mathtt{branch}\leavevmode\nobreak\ t\leavevmode\nobreak\ p\leavevmode\nobreak\ y$ and $\mathtt{path}\leavevmode\nobreak\ {T}\leavevmode\nobreak\ x\leavevmode\nobreak% \ p\leavevmode\nobreak\ y$ become decidable predicates. In that case, $\mathtt{strongly\texttt{\char 95\relax}represents}\leavevmode\nobreak\ T\,P\,x\>t$ implies that $P$ is decidable as well, an assumption we want to avoid for building representations. In the case of $\mathtt{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:\mathtt{rel}_{2}\>X$ which is furthermore finitely branching, i.e. $\forall x,\,\mathtt{finite}\,{(T\,x)}$ . We show that paths of bounded length can be strongly represented.

Theorem 19.

When $T:\mathtt{rel}_{2}\>X$ is finitely branching, for any $n:\mathbb{N}$ and any $x : X$ , the property $(\lambda\,{p\,y},\,{{\lfloor{p}\rfloor}\leq n})$ in $T$ at $x$ has a strong representation.

Proof.

We build the tree t s.t. $\mathtt{strongly\texttt{\char 95\relax}represents}\leavevmode\nobreak\ T% \leavevmode\nobreak\ (\lambda\,{p\,y},\,{{\lfloor{p}\rfloor}\leq n})% \leavevmode\nobreak\ x\leavevmode\nobreak\ t$ by induction on $n$ , after generalizing on $x$ . $\hfill\blacktriangleleft$

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

Theorem 20.

When $T:\mathtt{rel}_{2}\>X$ is finitely branching, for any property $P:\mathtt{list}\,X\mathrel{\rightarrow}X\mathrel{\rightarrow}\mathbb{P}$ and any point $x : X$ , the two following statements are equivalent:

$\blacksquare$

$\exists t,\,\mathtt{represents}\leavevmode\nobreak\ T\,P\,x\leavevmode\nobreak\ t$ ;
$\blacksquare$

$\exists n,\forall\,p\,y,\,\mathtt{path}\leavevmode\nobreak\ {T}\leavevmode% \nobreak\ x\leavevmode\nobreak\ p\leavevmode\nobreak\ y\mathrel{\rightarrow}P% \,p\,y\mathrel{\rightarrow}{\lfloor{p}\rfloor}<n$ .

Proof.

In the forward direction, the bound $n$ can be chosen to be the height $\mathtt{tree\texttt{\char 95\relax}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. $\mathtt{strongly\texttt{\char 95\relax}represents}\,T\,(\lambda\,{p\,y},\,{{% \lfloor{p}\rfloor}\leq n})\,x\,t$ . We then check that this tree $t$ represents $P$ in $T$ at $x$ . $\hfill\blacktriangleleft$

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¹⁶¹⁶16as sets of finite sequences of Booleans representing their finite branches. 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:\mathtt{rel}_{2}\>X$ , i.e. $\forall x,\,\mathtt{finite}\,{(T\,x)}$ , a $T$ -upward closed unary relation $P:\mathtt{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,\,\mathtt{represents}\leavevmode\nobreak\ T\leavevmode\nobreak\ (% \lambda\,{p\,y},\,{\lnot P\,y})\leavevmode\nobreak\ x\leavevmode\nobreak\ t$ .

Proof.

Using the length of paths, we define $\mathtt{circle}\,n$ , the circle (centered at $x$ ) of radius $n$ , and the collection of $Q:\mathtt{rel}_{1}\>{(\mathtt{list}\,X)}$ of finite supports of some circle as

\mathtt{circle}\,n\mathrel{{:}\!{=}}\lambda\,{y},\,{\exists p,\,\mathtt{path}% \leavevmode\nobreak\ {T}\leavevmode\nobreak\ x\leavevmode\nobreak\ p% \leavevmode\nobreak\ y\mathrel{\wedge}n={\lfloor{p}\rfloor}}\qquad Q\,l% \mathrel{{:}\!{=}}\exists n,\,\forall x,\,\mathtt{circle}\,n\,x\mathrel{\,% \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,\,\mathtt{finite}\,{(\mathtt{circle}\,n)}$ .

Let us show that $Q$ meets ${\textstyle{\wedge_{1}}}P$ . Indeed, as we assume $\mathtt{cover}\>{T}\,P\,x$ , using the FAN Theorem 14 for covers we get $\mathtt{cover}\>{{T}^{\dagger}}\leavevmode\nobreak\ {\textstyle{\wedge_{1}}}P% \leavevmode\nobreak\ {[x]}$ . Then we use $\mathtt{cover\texttt{\char 95\relax}negative}$ with $Q$ . We only need to show that $Q$ holds at ${[x]}$ and is ${T}^{\dagger}$ -unstoppable i.e. $\forall l,\,Q\,l\mathrel{\rightarrow}\exists m,\,Q\,m\mathrel{\wedge}{T}^{% \dagger}\,l\,m$ :

$\blacksquare$

$Q\,{[x]}$ holds because ${[x]}$ is a support for the circle of radius $0$ ;
$\blacksquare$

$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 ${\textstyle{\wedge_{1}}}P$ , then $P$ contains some circle, i.e. there is $n$ such that $\mathtt{circle}\,n\subseteq P$ . As a consequence, since $T$ -paths from $x$ of length greater that $n$ cross $\mathtt{circle}\,n$ 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,\,\mathtt{path}\leavevmode\nobreak\ {T}\leavevmode\nobreak\ x% \leavevmode\nobreak\ p\leavevmode\nobreak\ y\mathrel{\rightarrow}n\leq{\lfloor% {p}\rfloor}\mathrel{\rightarrow}P\,y$ holds and we conclude using Theorem 20. $\hfill\blacktriangleleft$

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

As the instance of Theorem 21 where $P\mathrel{{:}\!{=}}\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) $\mathtt{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:\mathtt{rel}_{2}\>X$ be a binary relation s.t. $\forall x,\,\mathtt{finite}\,{(T\,x)}$ and let $x : X$ be a $T$ -accessible point of $X$ , i.e. $\mathtt{acc}\>{T}\,x$ . Then there is a rose tree $t:\mathtt{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 bars. It is not exactly an instance of Theorem 21 because the properties of paths are not limited to those of their endpoint.

Theorem 23 (Kőnig’s lemma for inductive bars).

Let us assume a finitely branching binary relation $T:\mathtt{rel}_{2}\>X$ , a monotone unary relation $P:\mathtt{rel}_{1}\>{(\mathtt{list}\,X)}$ , and a point $x : X$ . If $\mathtt{bar}\leavevmode\nobreak\ P\leavevmode\nobreak\ {[\mskip 1.0mu]}$ then $\exists t,\,\mathtt{represents}\leavevmode\nobreak\ T\leavevmode\nobreak\ % \bigl{(}\lambda\,{p\,y},\,{\lnot P\,(\mathtt{rev}\,p)}\bigr{)}\leavevmode% \nobreak\ x\leavevmode\nobreak\ t$ .

Proof.

The proof is comparable (not identical) to the proof of Theorem 21 and uses $\mathtt{FAN\texttt{\char 95\relax}bar}$ and $\mathtt{bar\texttt{\char 95\relax}negative}$ instead as replacements for $\mathtt{FAN\texttt{\char 95\relax}cover}$ and $\mathtt{cover\texttt{\char 95\relax}negative}$ . $\hfill\blacktriangleleft$

5.4 Kőnig’s lemma for sequences of finite choices

Bar predicates can be specialized using the notion of good sequence, i.e. one containing a redundant pair w.r.t. a binary (redundancy) relation. This relation can be the identity, but there are other interesting cases, e.g. multiset inclusion [20]. In this case, bar predicates characterize inductive almost full relations [20, 31].

We assume a binary relation $R:\mathtt{rel}_{2}\>X$ to represent a notion of redundancy, and define two unary relations $\mathtt{good}\,{R}$ and $\mathtt{irred}\,R$ of type $\mathtt{rel}_{1}\>{(\mathtt{list}\,X)}$ , $\mathtt{good}\,{R}$ characterizing lists which contain a good pair, and $\mathtt{irred}\,R$ characterizing lists which are irredundant, i.e. avoiding good pairs:¹⁷¹⁷17See [21] for an equivalent inductive characterization of $\mathtt{good}\,{R}$ .

\begin{array}[]{l@{~{\cdef}~}l}\mathtt{good}\,{R}\leavevmode\nobreak\ p\hfil% \leavevmode\nobreak\ {\mathrel{{:}\!{=}}}\leavevmode\nobreak\ &\exists\,l\,x\,% m\,y\,r,\,p=l\mathbin{{+\mskip-10.0mu+}}{[x]}\mathbin{{+\mskip-10.0mu+}}m% \mathbin{{+\mskip-10.0mu+}}{[y]}\mathbin{{+\mskip-10.0mu+}}r\mathrel{\wedge}R% \,y\,x;\\ \mathtt{irred}\,R\leavevmode\nobreak\ p\hfil\leavevmode\nobreak\ {\mathrel{{:}% \!{=}}}\leavevmode\nobreak\ &\forall\,l\,x\,m\,y\,r,\,p=l\mathbin{{+\mskip-10.% 0mu+}}{[x]}\mathbin{{+\mskip-10.0mu+}}m\mathbin{{+\mskip-10.0mu+}}{[y]}% \mathbin{{+\mskip-10.0mu+}}r\mathrel{\rightarrow}R\,x\,y\mathrel{\rightarrow}% \bot.\end{array}

It is obvious that $\mathtt{good}\,{R}$ is monotone. Moreover, we show the correspondence between bad (i.e. not good) lists and irredundant ones:¹⁸¹⁸18 $\mathtt{good}\,{}$ and $\mathtt{irred}$ use $R$ in opposite ways, hence the use of the $\mathtt{rev}$ erse function.

\mathtt{not\texttt{\char 95\relax}good\texttt{\char 95\relax}iff\texttt{\char 9% 5\relax}irred}\leavevmode\nobreak\ R\leavevmode\nobreak\ p:\leavevmode\nobreak% \ \lnot\bigl{(}\mathtt{good}\,{R}\leavevmode\nobreak\ (\mathtt{rev}\,p)\bigr{)% }\mathrel{\,\leftrightarrow\,}\mathtt{irred}\,R\leavevmode\nobreak\ p.

Definition 24 (Almost full relation [31]).

For binary relations $R:\mathtt{rel}_{2}\>X$ , we define the predicate $\mathtt{af}\>{R}:\mathbb{P}$ using the two inductive rules, where ${R{\uparrow}u}\mathrel{{:}\!{=}}\lambda\,{x\,y},\,{R\,x\,y\mathrel{\vee}R\,u\,x}$ :

We recall that $\mathtt{af}\>{R}$ is another way of stating (i.e. is equivalent to) $\mathtt{bar}\leavevmode\nobreak\ (\mathtt{good}\,{R})\leavevmode\nobreak\ {[% \mskip 1.0mu]}$ (see e.g. [20, p. 11] or [21]) but below we just need the implication in this direction:

\mathtt{af\texttt{\char 95\relax}\texttt{\char 95\relax}bar\texttt{\char 95% \relax}good\texttt{\char 95\relax}nil}\leavevmode\nobreak\ R:\leavevmode% \nobreak\ \mathtt{af}\>{R}\mathrel{\rightarrow}\mathtt{bar}\leavevmode\nobreak% \ (\mathtt{good}\,{R})\leavevmode\nobreak\ {[\mskip 1.0mu]}.

Proof.

First we establish $\mathtt{bar}\leavevmode\nobreak\ (\mathtt{good}\,{R{\uparrow}u})\leavevmode% \nobreak\ p\mathrel{\rightarrow}\mathtt{bar}\leavevmode\nobreak\ (\mathtt{good% }\,{R})\leavevmode\nobreak\ (p\mathbin{{+\mskip-10.0mu+}}{[u]})$ by induction on $\mathtt{bar}\leavevmode\nobreak\ (\mathtt{good}\,{R{\uparrow}u})\leavevmode% \nobreak\ p$ . As an instance where $p\mathrel{{:}\!{=}}{[\mskip 1.0mu]}$ , we get $\mathtt{bar}\leavevmode\nobreak\ (\mathtt{good}\,{R{\uparrow}u})\leavevmode% \nobreak\ {[\mskip 1.0mu]}\mathrel{\rightarrow}\mathtt{bar}\leavevmode\nobreak% \ (\mathtt{good}\,{R})\leavevmode\nobreak\ {[u]}$ . Then we can show the implication $\mathtt{af}\>{R}\mathrel{\rightarrow}\mathtt{bar}\leavevmode\nobreak\ (\mathtt% {good}\,{R})\leavevmode\nobreak\ {[\mskip 1.0mu]}$ by induction on $\mathtt{af}\>{R}$ . $\hfill\blacktriangleleft$

We can deduce usual the sequential characterization of almost full relations, but, as with covers and bars, this characterization is constructively weaker.

\mathtt{af\texttt{\char 95\relax}sequences}\leavevmode\nobreak\ R:\leavevmode% \nobreak\ \mathtt{af}\>{R}\mathrel{\rightarrow}\forall\alpha:\mathbb{N}% \mathrel{\rightarrow}X,\,\exists\,i\,j,\,i<j\mathrel{\wedge}R\,\alpha_{i}\,% \alpha_{j}.

Proof.

We obtain $n$ such that $\mathtt{good}\,{R}\leavevmode\nobreak\ [\alpha_{n-1};\ldots;\alpha_{0}]$ using $\mathtt{af\texttt{\char 95\relax}\texttt{\char 95\relax}bar\texttt{\char 95% \relax}good\texttt{\char 95\relax}nil}$ above, followed by $\mathtt{bar\texttt{\char 95\relax}sequences}$ from Section 3.5. We conclude by analyzing the identity $l\mathbin{{+\mskip-10.0mu+}}{[x]}\mathbin{{+\mskip-10.0mu+}}m\mathbin{{+\mskip% -10.0mu+}}{[y]}\mathbin{{+\mskip-10.0mu+}}r=[\alpha_{n-1};\ldots;\alpha_{0}]$ where $R\,y\,x$ holds. $\hfill\blacktriangleleft$

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}\mathrel{\rightarrow}\mathtt{rel}_{1}\>X$ , we define a predicate $\mathtt{choice\texttt{\char 95\relax}list}\,P:\mathtt{rel}_{1}\>{(\mathtt{list% }\,X)}$ such that $\mathtt{choice\texttt{\char 95\relax}list}\,P\leavevmode\nobreak\ [x_{0};% \ldots;x_{n-1}]\mathrel{\,\leftrightarrow\,}P_{0}\,x_{0}\mathrel{\wedge}\cdots% \mathrel{\wedge}P_{n-1}\,x_{n-1}$ , i.e. $\mathtt{choice\texttt{\char 95\relax}list}\,P\leavevmode\nobreak\ l$ holds exactly when the members of $l$ are successive choices in $P_{0}$ , $P_{1}$ , …

Theorem 25.

Given an almost full relation, i.e. $R:\mathtt{rel}_{2}\>X$ s.t. $\mathtt{af}\>{R}$ , and a sequence of finite unary relations, i.e. $P:\mathbb{N}\mathrel{\rightarrow}\mathtt{rel}_{1}\>X$ s.t. $\forall n,\,\mathtt{finite}\,{P_{n}}$ . Then the length of irredundant choice lists for $P$ is (uniformly) bounded. Formally, we get:

\mathtt{af}\>{R}\mathrel{\rightarrow}(\forall n,\,\mathtt{finite}\,{P_{n}})% \mathrel{\rightarrow}\exists n,\,\forall l,\,\mathtt{choice\texttt{\char 95% \relax}list}\,P\leavevmode\nobreak\ l\mathrel{\rightarrow}\mathtt{irred}\,R% \leavevmode\nobreak\ l\mathrel{\rightarrow}{\lfloor{l}\rfloor}<n.

Proof.

From $\mathtt{af\texttt{\char 95\relax}\texttt{\char 95\relax}bar\texttt{\char 95% \relax}good\texttt{\char 95\relax}nil}$ , we know that $\mathtt{bar}\,(\mathtt{good}\,{R})\,{[\mskip 1.0mu]}$ holds and we apply the $\mathtt{FAN\texttt{\char 95\relax}bar}$ form of Theorem 15 and derive $\mathtt{bar}\leavevmode\nobreak\ (\lambda\,{lc},\,{\mathtt{FAN}\leavevmode% \nobreak\ lc\subseteq\mathtt{good}\,{R}})\leavevmode\nobreak\ {[\mskip 1.0mu]}$ .

We define $\mathtt{support}\leavevmode\nobreak\ n\leavevmode\nobreak\ l\mathrel{{:}\!{=}}% \forall x,\,P_{n}\,x\mathrel{\,\leftrightarrow\,}x\in l$ , meaning that $l$ is a supporting list for the (finite) unary relation $P_{n}$ . We use the $\mathtt{bar\texttt{\char 95\relax}negative}$ characterization of inductive bars applied to $\mathtt{bar}\leavevmode\nobreak\ (\lambda\,{lc},\,{\mathtt{FAN}\leavevmode% \nobreak\ lc\subseteq\mathtt{good}\,{R}})\leavevmode\nobreak\ {[\mskip 1.0mu]}$ with $Q\mathrel{{:}\!{=}}\lambda\,{lc},\,{\mathtt{choice\texttt{\char 95\relax}list}% \leavevmode\nobreak\ \mathtt{support}\leavevmode\nobreak\ (\mathtt{rev}% \leavevmode\nobreak\ lc)}$ . We get $l c$ such that $\mathtt{FAN}\leavevmode\nobreak\ lc\subseteq\mathtt{good}\,{R}$ and $\mathtt{choice\texttt{\char 95\relax}list}\leavevmode\nobreak\ \mathtt{support% }\leavevmode\nobreak\ (\mathtt{rev}\leavevmode\nobreak\ lc)$ .

Then we check that $n\mathrel{{:}\!{=}}{\lfloor{lc}\rfloor}$ satisfies the property $\forall l,\,\mathtt{choice\texttt{\char 95\relax}list}\leavevmode\nobreak\ P% \leavevmode\nobreak\ l\mathrel{\rightarrow}{\lfloor{l}\rfloor}=n\mathrel{% \rightarrow}\mathtt{good}\,{R}\leavevmode\nobreak\ (\mathtt{rev}\leavevmode% \nobreak\ l)$ . The same value then bounds the length of irredundant choice lists for $P$ . $\hfill\blacktriangleleft$

Again, we use a combination of a FAN theorem and the negative characterization of inductive bars. The assumption of finiteness $\forall n,\,\mathtt{finite}\,{P_{n}}:\mathbb{P}$ is not strong enough to be able to build a sequence $\mathbb{N}\mathrel{\rightarrow}\mathtt{list}\,X$ that enumerates the respective supports for $P_{0}$ , $P_{1}$ , … 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 $\mathtt{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 $\mathtt{cover}$ , $\mathtt{bar}$ or $\mathtt{af}$ predicates are lifted as:

\begin{array}[]{@{}l@{}}\mathtt{cover}_{t}\leavevmode\nobreak\ \{X\}% \leavevmode\nobreak\ (T:X\mathrel{\rightarrow}X\mathrel{\rightarrow}\mathtt{% Type})\leavevmode\nobreak\ (P:\mathtt{rel}_{1}\>X):X\mathrel{\rightarrow}% \mathtt{Type}\\ \mathtt{bar}_{t}\leavevmode\nobreak\ \{X\}\leavevmode\nobreak\ \bigl{(}P:% \mathtt{rel}_{1}\>{(\mathtt{list}\,X)}\bigr{)}:\mathtt{list}\,X\mathrel{% \rightarrow}\mathtt{Type}\\ \mathtt{af}_{t}\leavevmode\nobreak\ \{X\}\leavevmode\nobreak\ (R:\mathtt{rel}_% {2}\>X):\mathtt{Type}\\ \end{array}

and, as a consequence, parts of the $\mathtt{List}$ and $\mathtt{Permutation}$ library results need to be given $\mathtt{Type}$ -bounded variants as well. Noticeably, the transition relation argument $T$ in $\mathtt{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 $\mathtt{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 $\mathtt{Type}$ :

\mathtt{af}_{t}\,R\mathrel{\rightarrow}(\forall n,\,\mathtt{finite}_{t}\,{P_{n% }})\mathrel{\rightarrow}\{n:\mathbb{N}\mid\forall l,\,\mathtt{choice\texttt{% \char 95\relax}list}\,P\leavevmode\nobreak\ l\mathrel{\rightarrow}\mathtt{% irred}\,R\leavevmode\nobreak\ l\mathrel{\rightarrow}{\lfloor{l}\rfloor}<n\}

where $\mathtt{finite}_{t}\leavevmode\nobreak\ \{X\}\leavevmode\nobreak\ (P:X\mathrel% {\rightarrow}\mathbb{P})\mathrel{{:}\!{=}}\{l\mid\,\forall x,\,P\,x\mathrel{\,% \leftrightarrow\,}x\in l\}$ is the lifting of finiteness.

We delegate to the distributed Coq code, specifically file $\mathtt{constructive\texttt{\char 95\relax}konig\texttt{\char 95\relax}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:

$\blacksquare$

each sequent rule has finitely many premises, in fact less than two;
$\blacksquare$

for any conclusion, there are only finitely many rule instances having that conclusion;
$\blacksquare$

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 $\mathtt{Type}$ -bounded variant of Theorem 25 called $\mathtt{Constructive\texttt{\char 95\relax}Koenigs\texttt{\char 95\relax}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 $\mathrm{TREE}(n)$ monster

In [23], we build on a Coq constructive proof of Kruskal’s tree theorem [22] to implement $\mathrm{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) $\mathtt{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,\ldots,n\}$ is $\mathtt{af}$ and we use this relation as our redundancy relation. This means, using the sequential characterization $\mathtt{af\texttt{\char 95\relax}sequences}$ of Section 5.4, that any sequence $T_{1}$ , $T_{2}$ ,… of roses 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 $\mathrm{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. $\mathrm{TREE}(n)$ , can then be computed by unbounded linear search [23].¹⁹¹⁹19Using a $\mathtt{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 $\mathrm{TREE}(n)$ since writing $\mathrm{TREE}(3)$ in decimal would already exhaust all atoms of the known universe.

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 characterization, and shares properties with Brouwer’s notion of spread; c) it is relevant in practice, for instance when dealing with $\mathtt{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 positive/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.
[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/hl75.
[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 Interactive Theorem Proving, pages 250–265. Springer Berlin Heidelberg, 2012. doi:10.1007/978-3-642-32347-8_17.

[bib.bib1] [1] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[bib.bib2] [2] J. Berger. Brouwer’s fan theorem, 2021. doi:10.48550/arXiv.2001.00064.

[bib.bib3] [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.

[bib.bib4] [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.

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

[bib.bib6] [6] T. Coquand. About Brouwer’s Fan Theorem. Revue internationale de philosophie, 230:483–489, September 2004. URL: http://www.jstor.org/stable/23955601.

[bib.bib7] [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.

[bib.bib8] [8] H. B. Curry. A Theory of Formal Deductibility. Notre Dame mathematical lectures. University of Notre Dame, 1957.

[bib.bib9] [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.

[bib.bib10] [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.

[bib.bib11] [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.

[bib.bib12] [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.

[bib.bib13] [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.

[bib.bib14] [14] W. Hanf. Nonrecursive Tilings of the Plane. I. The Journal of Symbolic Logic, 39(2):283–285, 1974. doi:10.2307/2272640.

[bib.bib15] [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.

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

[bib.bib17] [17] S. Kripke. The Problem of Entailment (abstract). Journal of Symbolic Logic, 24:324, 1959.

[bib.bib18] [18] D. Kőnig. Über eine Schlussweise aus dem Endlichen ins Unendliche. Acta Sci. Math. (Szeged), 3(2–3):121–130, 1927.

[bib.bib19] [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.

[bib.bib20] [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.

[bib.bib21] [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.

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

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

[bib.bib24] [24] D. Myers. Nonrecursive Tilings of the Plane. II. The Journal of Symbolic Logic, 39(2):286–294, 1974. doi:10.2307/2272641.

[bib.bib25] [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/hl75.

[bib.bib26] [26] S. G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Logic. Cambridge University Press, 2 edition, 2009.

[bib.bib27] [27] A. S. Troelstra. Note on the Fan Theorem. The Journal of Symbolic Logic, 39(3):584–596, 1974. doi:10.2307/2272902.

[bib.bib28] [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.

[bib.bib29] [29] W. Veldman. Brouwer’s Real Thesis on Bars. Philosophia Scientiæ, pages 21–42, 2006. doi:10.4000/philosophiascientiae.404.

[bib.bib30] [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.

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

Constructive Substitutes for Kőnig’s Lemma

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Supplementary Material:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Coq preliminaries

3 Inductive covers

Definition 1 (Upward closed).

3.1 Inductive covers definition, basic results

Definition 2 (Inductive cover [25]).

Proposition 3 (𝚌𝚘𝚟𝚎𝚛⁢_⁢𝚖𝚘𝚛𝚙𝚑𝚒𝚜𝚖).

Proof.

Proof.

Proof.

3.2 Inductive cover and accessibility

Definition 4 (𝚊𝚌𝚌(essibility), R-founded).

Proposition 5.

Proposition 6.

3.3 Inductive cover and inductive bars

Definition 7 (Inductive bar).

Definition 8 (Monotone unary relation).

Definition 9 (list extension).

Proposition 10 (𝚋𝚊𝚛⁢_⁢𝚒𝚏𝚏⁢_⁢𝚌𝚘𝚟𝚎𝚛⁢_⁢𝚎𝚡𝚝𝚎𝚗𝚍𝚜).

3.4 Positive, negative and sequential characterizations

Definition 11 (Nonequivalent characterizations of cover).

Proof.

Proof.

Theorem 12 (in the spirit of Brouwer’s bar theorem).

3.5 Discussion

4 The FAN theorem for inductive covers

4.1 Lifting a relation to finite sets

Definition 13 (Finitary image).

4.2 Proof of the FAN theorem for inductive covers

Theorem 14 (FAN for inductive covers).

Proof.

4.3 The FAN theorem for inductive bars

Theorem 15 (reminder of Theorem 6 of [10]).

Proof.

5 Weaker variants of the contrapositive of Kőnig’s lemma

5.1 Path, rose trees and their branches

Definition 16 (Inductive path).

Definition 17 (Inductive rose tree).

5.2 Representing binary relations using rose trees

Definition 18 (Representation).

Theorem 19.

Proof.

Theorem 20.

Proof.

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

Theorem 21 (Kőnig’s lemma for inductive covers).

Proof.

Corollary 22 (Kőnig’s lemma for accessibility [1]).

Theorem 23 (Kőnig’s lemma for inductive bars).

Proof.

5.4 Kőnig’s lemma for sequences of finite choices

Definition 24 (Almost full relation [31]).

Proof.

Proof.

Theorem 25.

Proof.

5.5 Type-bounded variants and the FAN functional

6 Two examples of replacements of Kőnig’s lemma

6.1 The decidability from implicational relevance logic

6.2 Building Harvey Friedman’s 𝐓𝐑𝐄𝐄⁢(𝒏) monster

7 Conclusion

References

Proposition 3 ( $\mathtt{cover\texttt{\char 95\relax}morphism}$ ).

Definition 4 ( $\mathtt{acc}$ (essibility), $R$ -founded).

Proposition 10 ( $\mathtt{bar\texttt{\char 95\relax}iff\texttt{\char 95\relax}cover\texttt{\char 9% 5\relax}extends}$ ).

6.2 Building Harvey Friedman’s $\mathrm{TREE}(n)$ monster