On the Limits of Recursive Characterizations in the Refined $A$-Translation
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2605.20452
curl -X POST /api/v1/records/arxiv/2605.20452/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2605.20452/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'