Content deleted Content added
Tom.Reding (talk | contribs) m →Technical Definition: Fix Category:CS1 maint: Uses authors parameter: vauthors/veditors or enumerate multiple authors/editors; WP:GenFixes on, enum'd 3 author/editor WLs, using AWB |
m →Technical Definition: typo and general fixes, replaced: pass though → pass through using AWB |
||
Line 14:
Provided that for every sufficiently long function (λα)''r'' of type '''V'''<sup>''i''</sup> → '''R''', there is some ''n'' with ''L''<sub>''n''</sub>(''r'') = ''B''<sub>''n''</sub>((λα)''r'', (λ''x'':'''V''')''L''<sub>''n''+1</sub>(''r'')), the bar induction rule ensures that ''f'' is well-defined.
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
The principles of bar induction and bar recursion are the intuitionistic equivalents of the axiom of [[dependent choice]]s.<ref>{{cite book|author=Jeremy Avigad|author-link=Jeremy Avigad|author2=Solomon Feferman|author2-link=Solomon Feferman|chapter=VI: Gödel's functional ("Dialectica") interpretation|title=''Handbook of Proof Theory''|editor=S. R. Buss|editor-link=S. R. Buss|year=1999|url=http://math.stanford.edu/~feferman/papers/dialectica.pdf}}</ref>
| |||