Bar recursion: Difference between revisions

Revision as of 23:24, 24 November 2010

Revision as of 01:23, 29 November 2010

Line 1:

'''Bar recursion''' is a generalized form of recursion developed by Spector in his 1962 paper <ref>{{cite book|author=C. Spector|chapter=Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics|editor=F. D. E. Dekker|title=Recursive Function Theory: Proc. Symoposia in Pure Mathematics|volume=5|pages=1-271–27|year=1962|publisher=[[American Mathematical Society]]}}</ref>. It is related to [[bar induction]] in the same fashion that [[primitive recursion]] is related to ordinary [[induction]], or [[transfinite recursion]] is related to [[transfinite induction]].

==Technical Definition==

Line 16:

The idea is that one extends the sequence arbitrarily, using the recursion term ''B'' to determine the effect, until a sufficiently long node of the tree of sequences over '''V''' is reached; then the base term ''L'' determines the final value of ''f''. The well-definedness condition corresponds to the requirement that every infinite path must eventually pass though a sufficiently long node: the same requirement that is needed to invoke a bar induction.

The principles of bar induction and bar recursion are the intuitionistic equivalents of the axiom of [[dependent choice]]s. <ref>{{cite book|authors=[[Jeremy Avigad]], [[Solomon Feferman]]|chapter=VI: Godel's functional ("Dialectica") interpretation|title=''Handbook of Proof Theory''|editor=[[S. R. Buss]]|year=1999|url=http://math.stanford.edu/~feferman/papers/dialectica.pdf}}</ref>

==References==

<references/>

{{Uncategorized|date=November 2010}}