speleologic (speleologic) wrote,
speleologic
speleologic

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)
Tags: coq, fan theorem
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 1 comment