?

Log in

No account? Create an account

The fan "theorem"

The fan theorem is a theorem of Brouwer's original intuitionistic analysis, which follows from the principle of bar induction. In a classical setting it is also a theorem, thanks to the principle of excluded middle.

In constructive type theory it is not a theorem (yet), although by adding a principle of bar induction we can formally prove it. (see http://www.brics.dk/RS/98/39/BRICS-RS-98-39.ps.gz)

My interest in the fan theorem comes from some specific places where it appears, like the completeness theorem of Wim Veldman or giving type-theoretical explanation to backtracking. Hence I am interested in specific instances of it and their computational contents.

I was wondering what is the problem with the general formulation however and that is why I tried to express it in Coq, for the particular fan Cantor space. It boils down to giving a proof of the following:

B : (nat -> option bool) -> Prop
bB : forall a : nat -> bool, exists l : nat, B (IS a l)
mB : forall (a : nat -> bool) (l : nat), B (IS a l) -> B (IS a (S l))
============================
exists n : nat, forall a : nat -> bool, B (IS a n)

Comments

the coq code with some definitions

(** Theory

A spread is a tree where all branches have infinite height. There
is no restriction on the number of subbranches at each node. (That
"branches have infinite hight" means that whenever you have
aconcrete finite branch then there is at least one branch in the
spread of which it is an initial segment.)

A fan is a spread where at each node there are finitelly many
subbranches.

A bar on a spread is a collection of finite branches, such that for
each branch of the spread, we have an initial segment of the branch
belonging to the bar. A bar is monotone when any extension of a
branch inside the bar is also in the bar.

The fan theorem says: Give me a fan and give me a monotone bar, and
I will give you a number n such that all initial segments of the
fan with length n belong to the bar.
*)
Require Import Compare_dec.

Definition Baire := (nat->nat)->Prop.
Definition Cantor := (nat->bool)->Prop.

(** The fan theorem for Cantor space seen as a fan *)
Section Cantor_fan.

(** (computing) an initial segment of a branch in Cantor space *)
Definition IS (a:nat->bool)(l:nat)(n:nat) : option bool :=
if (leb n l) then (Some (a n)) else None.

Eval compute in (IS (leb 0) 5 0).
Eval compute in (IS (leb 0) 5 1).
Eval compute in (IS (leb 0) 5 5).
Eval compute in (IS (leb 0) 5 6).

Definition bar (B:(nat->option bool)->Prop) :=
forall (a:nat->bool), exists l:nat, B (IS a l).

Definition monotone (B:(nat->option bool)->Prop) :=
forall (a:nat->bool)(l:nat), B (IS a l) -> B (IS a (S l)).

Theorem fanthm : forall B, bar B -> monotone B ->
exists n, forall (a:nat->bool), B (IS a n).
Proof.
intros B bB mB.
red in bB, mB.
(* how on earth can we produce a witnessing n? does having more
information about B help? like a definition of a B coming from
an actually use of the fan theorem in a concrete context. *)
Qed.

End Cantor_fan.