Content deleted Content added
→Technical Definition: more info. |
→Technical Definition: adding a cite to the Handbook of Proof Theory. |
||
Line 15:
The idea is that one extends the sequence arbitrarily, using the recursion term ''B'' to determine the effect, until a constant 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 constant node: the same requirement that is needed to invoke a bar induction.
<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==
| |||