On the Limits of Recursive Characterizations in the Refined $A$-Translation

Franziskus Wiesnet

This paper studies the limits of recursive classifications in proof theory and program extraction, using the refined $A$-translation as a central example. The refined $A$-translati…