BRICS RS-98-39 D. Fridlender: An Interpretation of the Fan Theorem in Type Theory BRICS

Basic Research in Computer Science

An Interpretation of the Fan Theorem in Type Theory

Daniel Fridlender BRICS Report Series RS-98-39 ISSN 0909-0878 December 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/39/

An Interpretation of the Fan Theorem in Type Theory^{⋆}

Daniel Fridlender

BRICS^{⋆⋆}, Department of Computer Science, University of Aarhus Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark

                          e-mail: daniel@brics.dk

Abstract. This article presents a formulation of the fan theorem in Martin-Löf’s type theory. Starting from one of the standard versions of the fan theorem we gradually introduce reformulations leading to a final version which is easy to interpret in type theory. Finally we describe a formal proof of that final version of the fan theorem.

Keywords: type theory, fan theorem, inductive bar.

1 Introduction

In informal constructive mathematics, the fan theorem is an easy consequence of the rule of bar induction. Both are about infinite objects which makes their interpretation in Martin-Löf’s type theory non trivial. Bar induction can be represented in type theory, as proposed in [Mar68] and shown also in this article. But still from this interpretation it is not clear how to formulate and prove the fan theorem formally in type theory.

This is because, whereas the usual informal language to treat bar induction and the fan theorem is the same, the formal treatment of the fan theorem in type theory is technically more involved than that of bar induction. The concept of finiteness is difficult to handle simultaneously in an elegant, completely formal and constructive way; and it seems hard to avoid dealing explicitly with fans, whereas spreads are avoided in the type-theoretic interpretation of bar induction.

⋆ Partially developed during the author’s stay at Göteborg University, Sweden.

⋆⋆

Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

The fan theorem is very important in constructive mathematics since it makes possible to reconstruct large parts of traditional analysis. For explanations of the fan theorem and its role in constructive analysis see for instance [Dum77] and [TvD88].

The goal in this article is to present a formulation and a proof of the fan theorem in type theory. The type-theoretic version of the fan theorem presented here has been used in [Fri97] to interpret in type theory an intuitionistic proof of Higman’s lemma which uses the fan theorem [Vel94]. However, in [Fri97] the type-theoretic fan theorem is only mentioned and the proof is omitted. The importance of the fan theorem justifies this more extended presentation.

Type theory here means Martin-Löf’s type theory, of which there exist different formulations (for example, [Mar75], [Mar84], [NPS90] and [Tas97]). The exposition here should suit all of them. The proof of the fan theorem presented here has been written down in full detail with the assistance of the proof-editor ALF [Mag94] which is an implementation of the formulation of type theory given in [Tas97].

The rest of this article is organized as follows. Section 2 introduces some notations and definitions to be used in the whole article, and gives an informal presentation of bar induction and the fan theorem.

Section 3 shows a type-theoretic interpretation of bar induction and some of its properties.

Finally, Section 4 formulates and proves the fan theorem in type theory.

2 Bar induction and the fan theorem

2.1 Preliminaries

Notations:

N the set of the natural numbers. Variables: n, m, k. A^{∗} the set of the lists (finite sequences) of elements of the set A.

Variables: \overline{u}, \overline{v}, \overline{w}. Even \overline{\overline{u}}, \overline{\overline{v}}, \overline{\overline{w}} when A is a set of lists.

<a_{1}, …, a_{n}> is the notation for lists.

\overline{u} ∗ \overline{v} is the concatenation between lists.

\overline{u} • a is a notation for concatenations of the form \overline{u}∗ <a>.

The variables α, β are used to denote infinite sequences of natural numbers. An initial segment <α(0), …, α(n−1)> of α is denoted \overline{α}(n). Given a set S of finite sequences of natural numbers, if ∀n [\overline{α}(n) ∈ S], then we write α ∈ S. We denote by S^{c} the set N^{∗}\S.

Definition 1 (tree). A tree is a set T of finite sequences of natural numbers (intuitively, a set of finite branches) which satisfy

<> ∈ T  T is inhabited
∀\overline{u} [\overline{u} ∈ T ∨ \overline{u} ∉ T ]  T is decidable
∀\overline{u}, n [\overline{u} • n ∈ T ⇒ \overline{u} ∈ T ]  T is closed under predecessor

Definition 2 (finitely branching). A finitely branching tree is a tree T which satisfy

∀\overline{u} ∈ T ∃m ∀n [\overline{u} • n ∈ T ⇒ n < m].

Definition 3 (spread, fan). A spread is a tree in which every node has at least one successor, that is, a tree S satisfying

∀\overline{u} ∈ S ∃n [\overline{u} • n ∈ S].

A finitely branching spread is called a fan.

Definition 4 (bar). Given a set U ⊆ N^{∗} and a spread S, U is a bar on S if

∀α ∈ S ∃n [\overline{α}(n) ∈ U].

When S = N^{∗}, S is called the universal spread and U is said to be a bar.

Proposition 1. Given a spread S and a bar U on S, then V = U∪S^{c} is a bar.

We can prove that V is a bar by letting α be an arbitrary infinite sequence of natural numbers and finding n such that \overline{α}(n) ∈ V. To this end, we determine a sequence of natural numbers β whose initial segments are the same as those of α as long as they belong to S. As soon as an initial segment of α does not belong to S, β deviates from α. From that point, the initial segments of β are arbitrary segments in S. That is,

β(i) = \{ \begin{matrix}α(i) & if \overline{α}(i+1) ∈ S \\ k & if \overline{α}(i+1) ∉ S, for some k such that \overline{β}(i) • k ∈ S \end{matrix}

As β ∈ S, and U is a bar on S, we can obtain n such that \overline{β}(n) ∈ U. Now, either \overline{α}(n) ∈ S, in which case \overline{α}(n) = \overline{β}(n) ∈ U ⊆ V, or \overline{α}(n) ∉ S, hence \overline{α}(n) ∈ S^{c} ⊆ V. Therefore, V is a bar.

2.2 Bar induction

Bar induction is the following rule, which is an axiom of intuitionistic logic

∀\overline{u} ∈ X \overline{u} ∈ Y  X is included in Y
∀\overline{u} ∈ X ∀n [\overline{u} • n ∈ X]  X is monotone
∀\overline{u} \{[∀n \overline{u} • n ∈ Y] ⇒ \overline{u} ∈ Y\}  Y is hereditary
∀α ∃n [\overline{α}(n) ∈ X]  X is a bar

<> ∈ Y BI

for X , Y ⊆ N^{∗}. For other formulations of the rule of bar induction and their justification see [Dum77].

2.3 Fan theorem

The most important consequence of the rule of bar induction is the fan theorem.

Theorem 1 (fan theorem). Given a fan F, and a monotone bar U on F, then

∃n ∀α ∈ F [\overline{α}(n) ∈ U].

Intuitively, the fan theorem states that for any finitely branching tree all whose branches are finite, there is an upper bound on the length of the branches. The tree, not explicit in the statement of the theorem, is the set F \ U (when U is decidable and <> ∉ U).

The fan theorem can also be read as stating that every finitely branching tree all whose branches are finite is itself finite, that is, has a finite number of nodes. This is so, since for a finitely branching tree, the existence of an upper bound on the length of the branches is equivalent with it being finite.

A proof of the fan theorem can be obtained using the rule of bar induction with Y = \{\overline{u} | ∃n ∀α ∈ F [α starts with \overline{u} ⇒ \overline{α}(n) ∈ U]\} and X = U ∪ F^{c}. Proposition 1 guarantees that X is a bar. The monotonicity of X follows from those of U and F^{c}. The inclusion of X in Y can be proved by letting \overline{u} ∈ X be arbitrary and choosing n as the length of \overline{u}. To prove that Y is hereditary we assume that, for an arbitrary \overline{u}, ∀k \overline{u}•k ∈ Y holds, and prove that \overline{u} ∈ Y also holds. If \overline{u} ∉ F, then \overline{u} ∈ Y clearly holds, since no α ∈ F starts with \overline{u}. Otherwise, as F is finitely branching there exists m such that for all k, \overline{u} • k ∈ F ⇒ k < m. As for each k, \overline{u} • k ∈ Y, it is possible to determine n_{0}, … n_{m−1} such that for each k < m and α ∈ F if α starts with \overline{u} • k, then \overline{α}(n_{k}) ∈ U. To show that \overline{u} ∈ Y, we choose n to be max {n_{k} | k < m} and use the monotonicity of U.

2.4 Other formulations of the fan theorem

So far, we have used the terminology which is standard in the literature. It is possible to give alternative presentations of the fan theorem, some of which, are actually not formulated in terms of fans but in terms of arbitrary finitely branching trees.

In this section, we explore other formulations of the fan theorem with the purpose of obtaining one which is easier to represent in type theory. We shall see that there is no need to introduce notions like fan or tree in type theory, since the fan theorem can be reformulated without explicit use of those notions.

Some of the formulations that we will introduce are in terms of a special kind of tree, which we call independent-choice trees.

Definition 5 (independent-choice). An independent-choice tree is a tree I such that for all \overline{u}, \overline{v} ∈ I of equal length,

∀n [\overline{u} • n ∈ I ⇔ \overline{v} • n ∈ I].

There is a one-to-one correspondence between independent-choice fans and infinite sequences of nonempty finite subsets of N. An independent-choice fan I is determined by a sequence I_{0}, I_{1}, … of nonempty finite subsets of N. The branches of I of length n are obtained by choosing one element from each of the sets I_{0}, I_{1}, …, I_{n−1} in that order. Every choice is independent of the other choices done to determine the branch. Similarly, there is a one-to-one correspondence between independent-choice finitely branching trees and (not necessarily infinite) sequences of nonempty finite subsets of N.

We list a few statements equivalent to the one of the fan theorem.

Theorem 2 (alternatives to fan theorem). The fan theorem is equivalent to the validity of

∀ monotone bar U ∃n ∀α ∈ T [\overline{α}(n) ∈ U]

in any of the following cases:

1. for all fan T ,

2. for all finitely branching tree T ,

3. for all independent-choice fan T ,

4. for all independent-choice finitely branching tree T .

The only difference between the fan theorem and item 1 is that in the latter U runs over bars on the universal spread, rather than over bars on the fan. With this modification, the fan theorem can be formulated for finitely branching trees as well (item 2). On the other hand, it is enough to restrict attention to independent-choice fans or trees (items 3 and 4).

To prove Theorem 2 notice that the domain on which T ranges in item 2 includes the one on which it ranges in item 1, and so item 2 ⇒ item 1. Analogously, item 2 ⇒ item 4, item 1 ⇒ item 3, and item 4 ⇒ item 3. Similarly, the domain on which U ranges in the fan theorem includes the one on which it ranges in Theorem 2, so Theorem 1 ⇒ item 1.

To finish the proof of Theorem 2 it is enough to prove that item 3 ⇒ item 2 and item 1 ⇒ Theorem 1. For the former, let T be an arbitrary finitely branching tree and U an arbitrary monotone bar. Let I be the least independent-choice fan containing T . Determine n such that ∀α ∈ I [\overline{α}(n) ∈ U]. As α ∈ T ⇒ α ∈ I, we obtain ∀α ∈ T [\overline{α}(n) ∈ U].

Finally, to prove that item 1 ⇒ Theorem 1, let F be an arbitrary fan and U an arbitrary bar on F. Define V = U ∪ F^{c}. By Proposition 1, V is a bar. Then, by item 1 there is an n such that for all α ∈ F, \overline{α}(n) ∈ V. As \overline{α}(n) ∈ F, \overline{α}(n) ∈ U.

Theorem 3 (more alternatives to fan theorem). The fan theorem is equivalent to the validity of

∀ monotone bar U ∃n ∀\overline{u} ∈ T [length(\overline{u}) = n ⇒ \overline{u} ∈ U]

in any of the following cases:

5. for all fan T ,

6. for all finitely branching tree T ,

7. for all independent-choice fan T ,

8. for all independent-choice finitely branching tree T .

Just as in the proof of Theorem 2, it is easy to obtain that item 6 ⇒ item 5, item 6 ⇒ item 8, item 5 ⇒ item 7, and that item 8 ⇒ item 7. Item 6 follows from item 7 in the same way as item 2 followed from item 3 in Theorem 2.

Finally, the equivalence between item 5 and item 1 of Theorem 2 is also easy, since given a fan T , all \overline{u} ∈ T of length n is equal to \overline{α}(n), for some α ∈ T .

Theorem 4 (one more alternative to fan theorem). For all monotone bar U and all infinite sequence I_{0}, I_{1}, … of finite subsets of N,

∃n [I_{0} × … × I_{n−1} ⊆ U],

where I_{0} × … × I_{n−1} = {<a_{0}, …, a_{n−1}> | ∀i a_{i} ∈ I_{i}}.

Theorem 4 is equivalent to the fan theorem.

Let T be the set ⋃{I_{0} × … × I_{i−1} | i ∈ N }. Clearly, T is a finitely branching tree. By item 6 of Theorem 3, there is a natural number n such that all the sequences in T of length n belong to U. Those sequences are exactly the elements in the set I_{0} × … × I_{n−1}.

Conversely, to prove that item 8 of Theorem 3 follows from Theorem 4, let T be an arbitrary independent-choice finitely branching tree. Let I_{i} be the set \{k ∈ N | ∃\overline{u} [length(\overline{u}) = i ∧ \overline{u} • k ∈ T ]\}. Given \overline{u} ∈ T of length n, we have \overline{u} ∈ I_{0} × … × I_{n−1} ⊆ U.

The advantage of the formulation of the fan theorem as in Theorem 4 is that it avoids the notions of fan and finitely branching tree. Also, if we extend the definition of bar to sets of finite sequences of finite subsets of natural numbers, rather than only sets of finite sequences of natural numbers, then we may write the fan theorem in the following way. Let \overline{I} range over finite sequences of finite subsets of N, and ⨂ denote the operation to obtain the Cartesian product of such a finite sequence, that is, ⨂ <I_{0}, …, I_{n−1}> = I_{0}×…×I_{n−1}.

Theorem 5 (fan theorem, final reformulation). Given a monotone set U of finite sequences of natural numbers, if U is a bar, then so is \{\overline{I} | ⨂ \overline{I} ⊆ U\}.

This is the formulation which is represented in type theory by Theorem 6.

3 Inductive bars

Following the Curry-Howard isomorphism ([CF58] and [How80]) every proposition is represented in type theory by the set of its proofs. Predicates, subsets and families of sets are identified with each other, in the sense that every predicate over the elements of a set A, every subset of A, and every family of sets indexed by the elements of A, is represented by a function which when applied to an element of A returns a set.

Given a predicate U over a set A and a list \overline{u} in A^{∗}, we let ⋀\overline{u} U or

⋀_{\overline{u}} U

mean that all the elements in the list \overline{u} satisfy U. In type theory, it can be defined inductively with the following introduction rules.

⋀_{<>} U  \begin{matrix}⋀\overline{u} U & U(a) \\ ⋀_{\overline{u}•a} U \end{matrix}

Notice that ⋀_{\overline{u}∗\overline{v}} U is equivalent to ⋀\overline{u} U ∧ ⋀\overline{v} U. Associated to the definition of ⋀\overline{u} U we have the following principle of induction, for every predicate X over A^{∗}.

\begin{aligned}⋀\overline{u} U & X (<>) & ∀\overline{v} [X (\overline{v}) ∧ U(a) ⇒ X (\overline{v} • a)] \\ & & X (\overline{u}) \end{aligned}

When using this principle we refer to it as induction on “the” proof that ⋀\overline{u} U, where “the” proof is the proof of ⋀\overline{u} U available at that moment.

In type theory, we formulate the definition of bar for predicates over lists of elements of an arbitrary set, rather than only for predicates over lists of natural numbers. The following definition is a variation on an idea taken from [Mar68].

Definition 6 (inductive bars). Given a set A and a predicate U over A^{∗}, U is an inductive bar if U | <> (to be read U bars the empty sequence), where this is inductively defined with the following introduction rules.

{U(\overline{u}) \atop U | \overline{u}}  {U | \overline{u} \atop U | \overline{u} • a}  {∀a ∈ A [U | \overline{u} • a] \atop U | \overline{u}}

Notice that if U(\overline{u}) ⇒ V(\overline{u}) for every \overline{u} ∈ A^{∗}, then also U | \overline{u} ⇒ V | \overline{u} for every \overline{u} ∈ A^{∗}. Associated to the definition of U | \overline{u} we have the following principle of induction, for every predicate Y over A^{∗}.

\begin{matrix}U | \overline{u} \\ ∀\overline{v} ∈ A^{∗} [U(\overline{v}) ⇒ Y(\overline{v})] \\ ∀\overline{v} ∈ A^{∗} ∀a ∈ A [Y(\overline{v}) ⇒ Y(\overline{v} • a)] \\ ∀\overline{v} ∈ A^{∗} \{[∀a ∈ A Y(\overline{v} • a)] ⇒ Y(\overline{v})\} \end{matrix} ; Y(\overline{u})

When using this principle we refer to it as induction on “the” proof that U | \overline{u}, where “the” proof is the proof of it available at that moment.

With this principle of induction it is possible to prove in type theory that the rule BI —with inductive bars instead of bars, and arbitrary sets instead of natural numbers— is derivable. For that proof it is convenient to define the following reverse-append function, which is denoted ↩.

\begin{matrix}\overline{u} ↩ <> = \overline{u} \\ \overline{u} ↩ (\overline{v} • a) = (\overline{u} • a) ↩ \overline{v} \end{matrix}

An interpretation in type theory of the rule BI is:

∀\overline{u} ∈ A^{∗} [X (\overline{u}) ⇒ Y(\overline{u})]  X is included in Y
∀\overline{u} ∈ A^{∗} ∀a ∈ A [X (\overline{u}) ⇒ X (\overline{u} • a)] X is monotone
∀\overline{u} ∈ A^{∗} \{[∀a ∈ A Y(\overline{u} • a)] ⇒ Y(\overline{u})\} Y is hereditary
X | \overline{u}  X bars \overline{u}

Y(\overline{u}) BITT

This rule can be derived by showing ∀\overline{v} ∈ A^{∗} Y(\overline{u} ↩ \overline{v}) by induction on the proof that X | \overline{u}.

In a type-theoretic context, by bar induction we refer to the rule BITT. When applying bar induction we will refer by monotonicity condition (of X), hereditary condition (of Y), and inclusion condition (that is, X ⊆ Y) to the instances corresponding to the premises of the rule.

Proposition 2. Given a set A, a monotone predicate U over A^{∗} and a list \overline{u} of elements of A, then

U | \overline{u} ⟺ V\overline{u} | <>,

where V\overline{u} = λ\overline{v} U(\overline{u} ∗ \overline{v}).

The ⇐ part is easy, and is left to the reader. Hint: use bar induction with X = V\overline{u} and Y = λ\overline{v} [U | \overline{u} ∗ \overline{v}]; or, for another proof which does not use monotonicity of U, by induction on the proof that V\overline{u} | <>.

We sketch a proof of the ⇒ part, which is by bar induction with X = U and Y = λ\overline{u} [V\overline{u} | <>]. The monotonicity condition is hypothesis of the proposition and the inclusion condition is trivial. It remains to prove the hereditary condition. Assume that for all a ∈ A, V_{\overline{u}•a} | <>. We have to show V\overline{u} | <>. In order to do so, we prove that for all a ∈ A, V\overline{u} | <a>. Now, this follows from V_{\overline{u}•a} | <> by bar induction with X = V_{\overline{u}•a} and Y = λ\overline{v} [V\overline{u} | <a> ∗ \overline{v}].

Proposition 3. Given a set A, two monotone predicates U, V over A^{∗} and a list \overline{u} of elements of A, then

U | \overline{u} ∧ V | \overline{u} ⟹ W | \overline{u},

where W = λ\overline{u} [U(\overline{u}) ∧ V(\overline{u})].

We sketch a proof of Proposition 3 by bar induction with X = U and Y = λ\overline{u} [V | \overline{u} ⇒ W | \overline{u}]. The monotonicity condition is hypothesis of the proposition. The hereditary condition follows from the facts that λ\overline{u} [W | \overline{u}] is hereditary and λ\overline{u} [V | \overline{u}] is monotone. Finally, the inclusion condition can be proved by bar induction with X = V and Y = λ\overline{u} [U(\overline{u}) ⇒ W | \overline{u}], repeating the previous reasoning, except that the new inclusion condition is trivial.

4 Fan theorem in type theory

The result we present here is a type-theoretic version of the fan theorem as formulated in Theorem 5, except that it will be expressed for an arbitrary set A rather than only for natural numbers. Finite subsets I_{i} of A will be represented by lists \overline{u}_{i} of elements of A. Finite sequences \overline{I} of such subsets, by lists \overline{\overline{u}} of lists. The function ⨂ occurring in the statement of Theorem 5 will be represented by a function which when applied to a list of lists <\overline{u}_{1}, …, \overline{u}_{n−1}> computes another list representing the Cartesian product I_{1} ×…×I_{n−1}.

To define ⨂ we first define the binary Cartesian product ×^{f} parametrized with a function f. Then, the finite Cartesian product ⨂_{b}^{f} also parametrized. Finally we instantiate it to obtain ⨂.

Given a function f : A → B, we denote by \overline{f} : A^{∗} → B^{∗} the function which maps f on every element of its argument.

\begin{matrix}\overline{f}( <>) = <> \\ \overline{f}(\overline{u} • a) = \overline{f}(\overline{u}) • f(a) \end{matrix}

Example 1. \overline{f}(<a_{0}, …, a_{n−1}>) =<f(a_{0}), …, f(a_{n−1})>.

Now, the function ×^{f}, which given a function f : A → B → C, and two lists \overline{u} ∈ A^{∗} and \overline{v} ∈ B^{∗} returns a variation of the Cartesian product of \overline{u} and \overline{v}. Instead of returning a list in (A × B)^{∗}, it returns a list in C^{∗} by applying the function f to the components of each possible pair.

\begin{matrix}<> ×^{f} \overline{v} = <> \\ (\overline{u} • a) ×^{f} \overline{v} = \overline{u} ×^{f} \overline{v} ∗ \overline{f(a)}(\overline{v}) \end{matrix}

Example 2. \overline{u} ×^{f} <> = <>, for every \overline{u}.

Example 3.

<a_{0}, a_{1}> ×^{f} <b_{0}, b_{1}> = <f(a_{0}, b_{0}), f(a_{0}, b_{1}), f(a_{1}, b_{0}), f(a_{1}, b_{1})>.

The function ⨂_{b}^{f}, given a function f : B → A → B, a base value b ∈ B, and \overline{\overline{u}} ∈ A^{∗}^{∗}, returns a list in B^{∗}, each of whose values is the result of iterating the function f along one tuple, assigning b to the empty tuple. Each tuple consists of one element from the first list of \overline{\overline{u}}, one from the second, etc. in the style of the Cartesian product.

\begin{matrix}⨂_{b}^{f}( <>) = <b> \\ ⨂_{b}^{f}(\overline{\overline{u}} • \overline{u}) = ⨂_{b}^{f}(\overline{\overline{u}}) ×^{f} \overline{u} \end{matrix}

Example 4.

\begin{matrix}⨂_{b}^{f}(<<a_{0}, a_{1}>, <b_{0}, b_{1}>>) \\ = <f(f(b, a_{0}), b_{0}), f(f(b, a_{0}), b_{1}), f(f(b, a_{1}), b_{0}), f(f(b, a_{1}), b_{1})>. \end{matrix}

Finally, the Cartesian product is obtained by giving • as the function to iterate, and <> as the base value.

⨂(\overline{\overline{u}}) = ⨂_{<>}^{•} (\overline{\overline{u}})

Example 5. ⨂( <>) = <<>>.

Example 6. ⨂(\overline{\overline{u}} • <>) = <>, for every \overline{\overline{u}}. Example 7.

⨂(<<a_{0}, a_{1}>, <b_{0}, b_{1}>>)= <<a_{0}, b_{0}>, <a_{0}, b_{1}>, <a_{1}, b_{0}>, <a_{1}, b_{1}>>.

The set \{\overline{I} | ⨂ \overline{I} ⊆ U\} in Theorem 5 can be interpreted as a predicate P on lists \overline{\overline{u}} of lists which is true when ⨂(\overline{\overline{u}}) is “included” in U. As ⨂(\overline{\overline{u}}) is actually not a set but a list, by it being “included” in U we mean that every element in the list ⨂(\overline{\overline{u}}) satisfies U, that is, ⋀_{⨂(\overline{\overline{u}})} U. Thus, the predicate P is in fact interpreted by the function

λ\overline{\overline{u}} [⋀_{⨂(\overline{\overline{u}})} U]. Hence, in type theory Theorem 5 becomes:

Theorem 6 (fan theorem in type theory). Given a set A and a monotone predicate U over A^{∗}, then if U is an inductive bar, so is the predicate

λ\overline{\overline{u}} [_{⨂(\overline{\overline{u}})}^{⋀} U] .

Lemma 1. The following properties hold for every \overline{u}, \overline{v}, \overline{w}, and \overline{\overline{u}}

1. \overline{u} ∗ \overline{v} ×^{f} \overline{w} = (\overline{u} ×^{f} \overline{w}) ∗ (\overline{v} ×^{f} \overline{w})

2. <a> ×^{f} \overline{u} ∗ \overline{v} = (<a>×^{f} \overline{u}) ∗ (<a>×^{f} \overline{v})

3. ⨂(<\overline{w} • a> ∗\overline{\overline{u}}) = ⨂(<\overline{w}> ∗\overline{\overline{u}}) ∗ ⨂(<<a>> ∗\overline{\overline{u}})

4. ⋀_{⨂(\overline{\overline{u}})} [λ\overline{u} U(<a> ∗\overline{u})] ⟹ ⋀_{⨂(<<a>>∗\overline{\overline{u}})} U

Item 1 can be proved by induction on \overline{v}. Item 2 follows from the fact that \overline{g}(\overline{u} ∗ \overline{v}) = \overline{g}(\overline{u}) ∗ \overline{g}(\overline{v}) (letting g be f(a)), which can also be proved by induction on \overline{v}. Item 3 can be proved by induction on \overline{\overline{u}}, using Example 6 in the base case and item 1 in the inductive case.

Though technically laborious, item 4 is intuitively clear since all the tuples in ⨂(<< a >> ∗\overline{\overline{u}}) are of the form <a> ∗\overline{u} with \overline{u} a tuple in ⨂(\overline{\overline{u}}). We omit that proof here.

For the proof of Theorem 6, we define, for \overline{u} ∈ A^{∗},

V\overline{u} = λ\overline{\overline{u}} [_{⨂(\overline{\overline{u}})}^{⋀} (λ\overline{v} U(\overline{u} ∗ \overline{v}))] .

We give a proof by bar induction with X = U and Y = λ\overline{u} \{V\overline{u} | <>\}.

The inclusion condition is U(\overline{u}) ⇒ V\overline{u} | <>, which is easy, since when U(\overline{u}) holds, even V\overline{u}( <>) holds because ⨂( <>) = <<>> by Lemma 1. The monotonicity condition is hypothesis of the theorem. The hereditary condition is (∀a ∈ A [V_{\overline{u}•a} | <>]) ⇒ V\overline{u} | <>. We assume

∀a ∈ A [V_{\overline{u}•a} | <>]  (1)

and given an arbitrary \overline{v} we prove V\overline{u} | <\overline{v}> by induction on \overline{v}.

If \overline{v} = <>, then V\overline{u} | <<>> is direct since V\overline{u}(<<>>) holds because of the facts that ⨂(<<>>) = <> holds by Lemma 1 and that ⋀_{<>} is trivially true regardless of the predicate.

If \overline{v} = \overline{w} • a for some \overline{w} ∈ A^{∗} (such that V\overline{u} | <\overline{w}>) and a ∈ A, then we know by (1) that

V_{\overline{u}•a} | <> and V\overline{u} | <\overline{w}>

and still have to prove

V\overline{u} | <\overline{w} • a> .

By Proposition 2 it can be written like this: we know

V_{\overline{u}•a} | <> and [λ\overline{\overline{u}} V\overline{u}(<\overline{w}> ∗\overline{\overline{u}})] | <>,

(hence, by Proposition 3 we know also that

[λ\overline{\overline{u}} [V_{\overline{u}•a}(\overline{\overline{u}}) ∧ V\overline{u}(<\overline{w}> ∗\overline{\overline{u}})]] | <>  (2)

holds) and have to prove

[λ\overline{\overline{u}} V\overline{u}(<\overline{w} • a> ∗\overline{\overline{u}})] | <> .  (3)

To prove that (2) ⇒ (3), it is enough to prove that for every \overline{\overline{u}} ∈ A^{∗}^{∗},

V_{\overline{u}•a}(\overline{\overline{u}}) ∧ V\overline{u}(<\overline{w}> ∗\overline{\overline{u}}) ⟹ V\overline{u}(<\overline{w} • a> ∗\overline{\overline{u}})

holds. By the definition of V\overline{u} and item 3 of Lemma 1, the right-hand side is equivalent to

V\overline{u}(<\overline{w}> ∗\overline{\overline{u}}) ∧ V\overline{u}(<<a>> ∗\overline{\overline{u}})

which follows from the left-hand side because, by item 4 of Lemma 1, V_{\overline{u}•a}(\overline{\overline{u}}) implies V\overline{u}(<<a>> ∗\overline{\overline{u}}).

Acknowledgements

I am grateful to Marc Bezem, Thierry Coquand, Monika Seisenberger, Jan Smith and Wim Veldman for fertile discussions about the fan theorem.

References

[CF58] H. Curry and R. Feys. Combinatory Logic, volume I. North-Holland, 1958.

[Dum77] M. Dummett. Elements of Intuitionism. Clarendon Press, Oxford, 1977.

[Fri97] D. Fridlender. Higman’s Lemma in Type Theory. In Types for proofs and programs, Lecture Notes in Computer Science 1512, 1997.

[How80] W. Howard. The Formulae-as-Types Notion of Construction. In J. Seldin and J. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, London, 1980.

[Mag94] L. Magnusson. The Implementation of ALF - a Proof Editor Based on Martin-Löf’s Monomorphic Type Theory with Explicit Substitution. PhD thesis, Department of Computing Science, Chalmers University of Technology and University of Göteborg, 1994.

[Mar68] P. Martin-Löf. Notes on Constructive Mathematics. Almqvist & Wiksell, 1968.

[Mar75] P. Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium 1973, pages 73–118, Amsterdam, 1975. North-Holland Publishing Company.

[Mar84] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.

[NPS90] B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s Type Theory. An Introduction. Oxford University Press, 1990.

[Tas97] A. Tasistro. Substitution, Record Types and Subtyping in Type Theory, with Applications to the Theory of Programming. PhD thesis, Department of Computing Science at Chalmers University of Technology and University of Göteborg, 1997.

[TvD88] A. Troelstra and D. van Dalen. Constructivism in Mathematics, An Introduction, Volume I. North-Holland, 1988.

[Vel94] W. Veldman. Intuitionistic Proof of the General non-Decidable case of Higman’s Lemma. Personal communication, 1994.

Recent BRICS Report Series Publications

RS-98-39 Daniel Fridlender. An Interpretation of the Fan Theorem in Type Theory. December 1998. 15 pp. To appear in International Workshop on Types for Proofs and Programs 1998, TYPES ’98 Selected Papers, LNCS, 1999.

RS-98-38 Daniel Fridlender and Mia Indrika. An n-ary zipWith in Haskell. December 1998. 12 pp.

RS-98-37 Ivan B. Damgård, Joe Kilian, and Louis Salvail. On the (Im)possibility of Basing Oblivious Transfer and Bit Commitment on Weakened Security Assumptions. December 1998. 22 pp. To appear in Advances in Cryptology: International Conference on the Theory and Application of Cryptographic Techniques, EUROCRYPT ’99 Proceedings, LNCS, 1999.

RS-98-36 Ronald Cramer, Ivan B. Damgård, Stefan Dziembowski, Martin Hirt, and Tal Rabin. Efficient Multiparty Computations with Dishonest Minority. December 1998. 19 pp. To appear in Advances in Cryptology: International Conference on the Theory and Application of Cryptographic Techniques, EURO-CRYPT ’99 Proceedings, LNCS, 1999.

RS-98-35 Olivier Danvy and Zhe Yang. An Operational Investigation of the CPS Hierarchy. December 1998.

RS-98-34 Peter G. Binderup, Gudmund Skovbjerg Frandsen, Peter Bro Miltersen, and Sven Skyum. The Complexity of Identifying Large Equivalence Classes. December 1998. 15 pp.

RS-98-33 Hans Hüttel, Josva Kleist, Uwe Nestmann, and Massimo Merro. Migration = Cloning ; Aliasing (Preliminary Version). December 1998. 40 pp. To appear in 6th International Workshop on the Foundations of Object-Oriented, FOOL6 Informal Proceedings, 1998.

RS-98-32 Jan Camenisch and Ivan B. Damgård. Verifiable Encryption and Applications to Group Signatures and Signature Sharing. December 1998. 18 pp.

RS-98-31 Glynn Winskel. A Linear Metalanguage for Concurrency. November 1998. 21 pp.

RS-98-30 Carsten Butz. Finitely Presented Heyting Algebras. November 1998. 30 pp.