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

Source: arXiv:2605.20452 · Published 2026-05-19 · By Franziskus Wiesnet

TL;DR

This paper investigates fundamental limits in proof theory regarding recursive syntactic characterizations of formula classes involved in the refined A-translation, a method that bridges classical and intuitionistic logic focused on the system MA^ω (minimal arithmetic with finite types). The refined A-translation, originating from work by Berger, Buchholz, and Schwichtenberg, classifies formulas into several recursive classes—definite, goal, relevant, and irrelevant formulas—each satisfying specific intuitionistic derivability properties. Schwichtenberg and Wainer previously noted that these properties hold for formulas beyond the originally defined definite class and posed the open problem of finding a complete recursive syntactic characterization of all such formulas. The key contribution of this paper is a negative result establishing that none of the four core properties admit any recursive characterization, effectively proving that this classification problem is undecidable under the consistency assumption of PA^ω (Peano Arithmetic with finite types). To complement this theoretical limitation, the author extends the framework by adding conjunction (∧) to the language of MA^ω and adapts the formula classes and translation theorem accordingly. Finally, a small Rust-based prover implementing the MA^ω theory and formula classes is presented, serving as an exploratory case study on Rust's applicability for proof assistant development rather than as formal verification of results. This work clarifies fundamental boundaries in syntactic proof classification and contributes practical insights on using Rust for constructing proof tools.

Key findings

• None of the four properties associated with the classes definite, goal, relevant, and irrelevant formulas admit a recursive characterization, assuming PA^ω is consistent (Prop 3.7).
• The property D[F/⊥] → D (for definite formulas D) is derivable for all D in the definite class but cannot be recursively decided for arbitrary D (Lem 3.5, Prop 3.7).
• The class Q of formulas closed under ∧, →, ∀ over Boolean variables satisfies (A → S) → (¬A → S) → S derivability, but no recursive decision procedure exists to decide membership (Prop 3.3).
• Extension of MA^ω language with conjunction ∧ preserves logical properties but requires adapting formula class definitions and the refined A-translation theorem accordingly (Section 4).
• The constructed small Rust prover for MA^ω and formula classes facilitated exploring class definition effects and functioned as a case study on Rust for proof assistants, highlighting modularity, ownership model, and testing infrastructure advantages.
• The undecidability proofs reduce from the halting problem via classical and intuitionistic embedding theorems linking PA^ω, HA^ω, and NA^ω (Theorem 2.12, Prop 3.3).
• Disjunction property in HA^ω is crucial for establishing the non-recursiveness, showing HA^ω ⊢ A ∨ ¬A implies semi-decidability of PA^ω soundness, which is impossible (Prop 3.3).

Threat model

The research addresses a theoretical 'threat model' of computability and decidability rather than an adversarial security scenario. The 'adversary' is conceptually analogous to a Turing machine attempting to decide membership in formula classes or proof properties given a formula. The paper assumes classical consistency of PA^ω and shows no recursive algorithm (adversary) can succeed in deciding if these properties hold universally.

Methodology — deep read

The paper operates within proof theory focused on minimal arithmetic MA^ω, a fragment of Heyting Arithmetic formulated with finite types and restrictions to negative formulas (no strong disjunction or existential quantifier, but extended with conjunction ∧). The threat model is mathematical undecidability rather than adversaries. The main data are syntactic formulas in MA^ω and their classifications. The author defines four classes of formulas (definite D, goal G, relevant R, irrelevant I) inductively via recursion on formula structure, based on refined A-translation theory from prior work by Berger et al. and Schwichtenberg-Wainer.

The paper revisits classical results embedding classical Peano arithmetic PA^ω into the negative fragment NA^ω of intuitionistic logic via the Gödel-Gentzen negative translation A¬¬, with proofs that derivability in PA^ω corresponds to derivability in NA^ω (Theorem 2.12). Using these embeddings and known undecidability results for PA^ω, the author constructs reductions proving no recursive algorithm can decide membership in the classes defined by the four key properties (Lemmas 3.5 and Props 3.3, 3.7).

Part of the methodology is adapting the language of MA^ω to include conjunction (∧), previously absent, and updating definitions of formula classes accordingly. This includes modifying the induction and recursive definitions while preserving fundamental derivability properties (Section 4).

Complementing the theoretical work, the author implemented a small proof assistant (or prover) in the Rust programming language, encoding the definitions of MA^ω, the four formula classes, and some proof principles. While not formally verifying the full theorems, the implementation served to experiment with formula class changes and assess Rust’s suitability for developing proof assistants from a software engineering perspective. Insights on its strong type system, ownership and borrowing, modularity, and integrated testing were discussed.

Overall, the work combines rigorous proof-theoretic arguments relying on embeddings and classical undecidability with constructive definitions and software implementation to form a comprehensive study of the limits of recursive syntactic characterization in refined A-translation.

Technical innovations

• Proof that the classes of formulas satisfying properties from refined A-translation (definite, goal, relevant, irrelevant) cannot be recursively characterized, establishing an explicit undecidability boundary for these syntactic classifications (prior open problem).
• Extension of the language of minimal arithmetic MA^ω by incorporating conjunction ∧, and adapted definitions and proofs for the formula classes and refined A-translation theorem.
• Systematic, simultaneously inductive recursive definitions of the four formula classes ensuring well-foundedness while expanding prior foundational definitions.
• Rust-based implementation of a small prover for MA^ω and the formula classes, exploring a new programming language paradigm (ownership, borrowing) for proof assistant development.

Baselines vs proposed

• No direct quantitative baselines; theoretical undecidability results compared to prior conjectured decidability or open problem in Schwichtenberg and Wainer's work.
• Rust prover compared qualitatively with Minlog (existing proof assistant implementing refined A-translation in computable functionals), highlighting tradeoffs in language paradigms and implementation approaches.

Limitations

• Negative results depend on the consistency assumption of PA^ω; if PA^ω were inconsistent, decidability claims would fail.
• Rust prover is a prototype and does not formally verify theorems or proofs; no mechanized proof checking is presently done.
• Extensions by conjunction preserve logical content but specific impacts on complexity or expressivity of formula classes are not deeply analyzed.
• No adversarial or practical evaluation of the prover’s utility or performance beyond conceptual case study.
• Results focus on syntactic characterizations only; semantic or alternative characterizations potentially remain unexplored.

Open questions / follow-ons

• Can alternative, non-recursive characterizations (e.g., semantic, proof-theoretic, or using restricted oracle access) meaningfully describe the formula classes with key refined A-translation properties?
• How does the addition of conjunction ∧ impact computational complexity or program extraction from proofs compared to the original system without conjunction?
• Might variants of the A-translation or other intuitionistic embeddings admit recursive characterizations for some subclasses or for restricted formula fragments?
• Can Rust or similar modern programming languages be further leveraged to build more robust, mechanized proof assistants for MA^ω and related systems, potentially automating undecidability proofs?

Why it matters for bot defense

While the paper focuses on foundational proof theory and program extraction rather than bot detection or CAPTCHA systems directly, its results bear conceptual relevance to bot-defense research centered on symbolic verification and synthesis of security properties. The undecidability of recursive syntactic classifications highlights intrinsic limitations on algorithmic recognition of formula classes representing computational properties, which parallels limitations faced in automatically distinguishing benign versus malicious bot behavior via syntactic pattern detection. Additionally, the extended framework with conjunctions and the studied Rust prover illustrate challenges and opportunities when designing symbolic reasoning engines or verification components that might underlie advanced CAPTCHA or bot-challenge mechanisms—especially those relying on proof-based or logic-based challenge-response techniques. Researchers working on CAPTCHA logic obfuscation or program synthesis defenses could take inspiration from the negative results to understand the limits of recursive classifications in constructing provably bot-resistant puzzles. Meanwhile, the case study on Rust indicates practical insights for engineers implementing secure symbolic tools in modern memory-safe languages.

Cite

@article{arxiv2605_20452,
  title={ On the Limits of Recursive Characterizations in the Refined $A$-Translation },
  author={ Franziskus Wiesnet },
  journal={arXiv preprint arXiv:2605.20452},
  year={ 2026 },
  url={https://arxiv.org/abs/2605.20452}
}

Read the full paper

• arXiv:2605.20452 (abstract)
• arXiv:2605.20452 (PDF)