KnowledgeBase » 
SEMINAR
» ID = 703
Realizing Bar Induction in Nuprl
by Mark Bickford
2012
Abstract
Brouwer's Bar Induction is a form of induction that is true in classical logic and also in intuitionistic logic.
The Fan theorem (a bar on a finitely branching tree is a uniform bar) is proved by bar induction and has consequences that are useful in analysis (Fan implies a weak form of Konig's lemma).
To add Bar Induction to Nuprl, we must state it as an inference rule. Since Bar Induction can be used to construct things (such as paths in a tree) the Nuprl rule must define the realizer for Bar Induction.
I will show how we construct the realizer for Bar Induction by a "bootstrapping" method:
We introduce a weak Bar Induction rule for proving only membership judgments (that a term is in a type) and use the weak Bar Induction rule to prove that the realizer for full Bar Induction exists. Then we can prove the Fan theorem and extract its realizer.