Abstract.
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].
Similar content being viewed by others
Author information
Authors and Affiliations
Additional information
Received: 27 April 1999 / Published online: 21 March 2001
Rights and permissions
About this article
Cite this article
Buchholz, W. Explaining the Gentzen–Takeuti reduction steps: a second-order system. Arch. Math. Logic 40, 255–272 (2001). https://doi.org/10.1007/s001530000064
Issue Date:
DOI: https://doi.org/10.1007/s001530000064