Using the concept of
notations for infinitary derivations we give an explanation of Takeuti's reduction steps on finite derivations (used in his consistency proof for Π
1
1-CA) in terms of the more perspicious infinitary approach from [BS88].
Mathematics Subject Classification (2000): 03F05, 03F15
Received: 27 April 1999 / Published online: 21 March 2001