{"id":"arxiv/2605.20452","url":"https://arxiv.org/abs/2605.20452","tags":["math.LO"],"score":0,"title":"On the Limits of Recursive Characterizations in the Refined $A$-Translation","domain":"math.LO","source":"arxiv","authors":["Franziskus Wiesnet"],"reviews":0,"subject":"math.LO","summary":"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$-translation, due to Berger, Buchholz, and Schwichtenberg, is based on recursively defined classes of formulas in minimal arithmetic $\\mathsf{MA}^ω$, in particular the classes of definite and goal formulas. One of its basic properties is that $D[\\bot := F] \\to D$ is derivable for every definite formula $D$. Schwichtenberg and Wainer observed that this property also holds for formulas outside the class of definite formulas…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-05-19","reactions":{}}