pith. sign in

arxiv: 2605.20452 · v1 · pith:33SOQT7Snew · submitted 2026-05-19 · 🧮 math.LO

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

Franziskus Wiesnet This is my paper

Pith reviewed 2026-05-21 06:59 UTC · model grok-4.3

classification 🧮 math.LO
keywords refined A-translationrecursive characterizationminimal arithmeticformula classesdefinite formulasprogram extractionintuitionistic derivability
0
0 comments X

The pith

Four properties central to the refined A-translation cannot be captured by any recursive syntactic definition.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper investigates the boundaries of recursive syntactic classifications for formulas in minimal arithmetic MA^ω when used for program extraction via the refined A-translation. It starts from the observation that definite formulas satisfy the derivability of D[⊥ := F] → D, but this property and three related ones hold for formulas beyond the standard recursive classes. The main result is a proof that none of these four properties can be characterized by a recursive definition based on formula structure. The work also extends the original framework by incorporating conjunction into the language and adapts the classes and translation theorem accordingly.

Core claim

The central claim is that none of the four properties—those satisfied by definite formulas, goal formulas, and two additional related classes—admits a recursive characterization with respect to intuitionistic derivability in the language of MA^ω. This negative result persists after extending the language to include conjunction, where the refined A-translation theorem is restated with adapted classes, though possible recursive extensions of the classes are considered without resolving the characterization problem.

What carries the argument

The four formula properties in the refined A-translation, defined relative to intuitionistic derivability of implications like D[⊥ := F] → D in MA^ω, which were originally introduced via recursive syntactic conditions on formulas.

If this is right

  • Adding conjunction to MA^ω requires adapting the definitions of the four classes while preserving the statement of the refined A-translation theorem.
  • The extended formulation allows discussion of possible recursive extensions to the classes that might include more formulas satisfying the properties.
  • A small Rust implementation of MA^ω and the formula classes can be used to test concrete examples of the classes without serving as formal verification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The negative result suggests that complete characterizations of the properties may require non-recursive or semantic criteria rather than purely syntactic ones.
  • Similar limits on recursive classifications could affect other proof-theoretic methods that rely on inductive definitions of formula classes for extraction.
  • The Rust case study implies that general-purpose languages with strong typing can support exploration of proof-theoretic concepts even if they are not designed as full proof assistants.

Load-bearing premise

That any recursive characterization of the properties would have to be given by a syntactic inductive definition over the structure of formulas in MA^ω.

What would settle it

A concrete recursive inductive definition over formula structure that exactly identifies all formulas D for which D[⊥ := F] → D is intuitionistically derivable in MA^ω would falsify the claim.

read the original abstract

This paper studies the limits of recursive syntactic 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}^\omega$, 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 and asked for a useful characterization of all formulas $D$ for which $D[\bot := F] \to D$ is intuitionistically derivable. In addition to definite formulas, the refined $A$-translation involves three further classes of formulas satisfying related properties. We show that none of these four properties admits a recursive characterization. In addition to this negative result, we extend the framework of refined $A$-translation. First, we add conjunction $\wedge$ to the language of $\mathsf{MA}^\omega$, whose original formulation contains only the logical connectives $\forall$ and $\to$, and adapt the formula classes accordingly. Second, we present the corresponding slightly extended formulation of the refined $A$-translation theorem and discuss possible recursive extensions of these classes. Finally, we discuss a small prover written in Rust which implements the theory $\mathsf{MA}^\omega$ and the four formula classes. The prover is not used as a formal verification of the results, but serves as a case study for examining Rust as a programming language for proof assistants. We highlight some advantages and drawbacks of Rust in this setting, including its strong type system, support for partial constructions, ownership and borrowing model, modularity, and testing infrastructure.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper studies limits of recursive syntactic characterizations for properties in the refined A-translation over minimal arithmetic MA^ω. It establishes a negative result: none of the four properties (centered on definite formulas, goal formulas, and the derivability of D[⊥ := F] → D and related substitution behaviors under intuitionistic derivability) admits a recursive characterization via syntactic inductive definition over formula structure. The paper then extends the setting by adding conjunction to MA^ω, adapts the four classes accordingly, states a corresponding extended refined A-translation theorem, discusses only approximate recursive extensions in the extended language, and presents a Rust implementation of MA^ω and the classes as an exploratory case study rather than formal verification.

Significance. The negative result, if established by the under- and over-generation arguments, is significant for proof theory and program extraction: it shows that the syntactic classes central to the refined A-translation cannot be captured by the usual recursive inductive definitions, thereby clarifying the boundaries of this approach and motivating non-recursive or semantic alternatives. The extension to conjunction and the discussion of approximate extensions broaden the framework's applicability, while the Rust case study offers concrete observations on language features for proof-assistant development.

major comments (1)
  1. [Negative-result section] The section establishing the negative result: the argument that every candidate inductive definition either under- or over-generates must explicitly identify, for each of the four properties, the precise set of formulas satisfying the target intuitionistic derivability condition (D[⊥ := F] → D and its relatives) so that the mismatch with the inductive class is verifiable.
minor comments (2)
  1. [Abstract] Abstract: a one-sentence indication of the method (under-/over-generation relative to the derivability set) would help readers assess the negative result without reading the full text.
  2. [Rust prover section] Rust-prover section: expand the listed advantages and drawbacks with one concrete code fragment or limitation observed during implementation of the formula-class predicates.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation of the paper and the recommendation for minor revision. We address the major comment on the negative-result section below.

read point-by-point responses

  1. Referee: [Negative-result section] The section establishing the negative result: the argument that every candidate inductive definition either under- or over-generates must explicitly identify, for each of the four properties, the precise set of formulas satisfying the target intuitionistic derivability condition (D[⊥ := F] → D and its relatives) so that the mismatch with the inductive class is verifiable.

    Authors: We agree that this would improve the clarity and verifiability of the negative result. The manuscript introduces the four properties by specifying the intuitionistic derivability conditions they satisfy and then proves that none of them can be captured by a recursive syntactic definition by exhibiting formulas that are under- or over-generated by any such definition. To make this more explicit as suggested, we will revise the section to state, for each property, the precise set of formulas meeting the condition before analyzing the inductive candidates. This is a clarification that does not affect the validity of the existing proofs. revision: yes

Circularity Check

0 steps flagged

No significant circularity; negative result is self-contained

full rationale

The central negative claim—that none of the four properties (D[⊥ := F] → D and relatives) admits a recursive syntactic characterization—is established by direct proof that any candidate inductive definition over formula structure either under- or over-generates relative to the set of formulas satisfying the intuitionistic derivability condition in MA^ω. This comparison is external to any fitted parameter or self-referential definition. The subsequent adaptation for conjunction and the Rust prover case study introduce no load-bearing reductions to the paper's own inputs. No self-citation chain or ansatz smuggling supports the core result, which remains independent of prior work by the same author.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the standard background of minimal arithmetic MA^ω and intuitionistic derivability; no new free parameters or invented entities are introduced.

axioms (2)
  • standard math Standard axioms and rules of minimal arithmetic MA^ω
    The paper works inside the existing theory MA^ω whose axioms are presupposed.
  • domain assumption Intuitionistic derivability for the implication D[⊥ := F] → D
    The four properties are defined in terms of what is intuitionistically derivable.

pith-pipeline@v0.9.0 · 5870 in / 1268 out tokens · 46428 ms · 2026-05-21T06:59:13.213450+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

17 extracted references · 17 canonical work pages

  1. [1]

    Refined program extraction from classical proofs

    Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg. “Refined program extraction from classical proofs”. In:Annals of Pure and Applied Logic114.1–3 (Apr. 2002), pp. 3–25.issn: 0168-0072.doi:10.1016/s0168-0072(01)00073-2

    work page doi:10.1016/s0168-0072(01)00073-2 2002

  2. [2]

    New kinds of realizability and the Markov rule

    A. G. Dragalin. “New kinds of realizability and the Markov rule”. In:Dokl. Akad. Nauk SSSR251.3 (1980), pp. 534–537.issn: 0002-3264.url:https://m.mathnet.ru/php/ archive.phtml?wshow=paper&jrnid=dan&paperid=43449&option_lang=eng. 18

    work page 1980

  3. [3]

    Classically and intuitionistically provably recursive functions

    Harvey Friedman. “Classically and intuitionistically provably recursive functions”. In:Higher Set Theory. Ed. by Gert H. Müller and Dana S. Scott. Berlin, Heidelberg: Springer Berlin Heidelberg, 1978, pp. 21–27.isbn: 978-3-540-35749-0

    work page 1978

  4. [4]

    Negative Translations Not Intuitionistically Equivalent to the Usual Ones

    Jaime Gaspar. “Negative Translations Not Intuitionistically Equivalent to the Usual Ones”. In:Studia Logica101.1 (Oct. 2012), pp. 45–63.issn: 1572-8730.doi: 10. 1007/s11225-011-9367-6

    work page 2012

  5. [5]

    Untersuchungen über das logische Schließen. I

    Gerhard Gentzen. “Untersuchungen über das logische Schließen. I”. In:Mathematische Zeitschrift39.1 (Dec. 1935), pp. 176–210.issn: 1432-1823.doi:10.1007/bf01201353

    work page doi:10.1007/bf01201353 1935

  6. [6]

    Assumes Rust 1.90.0 or later and Rust 2024 Edition

    Steve Klabnik, Carol Nichols, and Chris Krycho.The Rust Programming Language. Assumes Rust 1.90.0 or later and Rust 2024 Edition. Sept. 18, 2025.url:https: //doc.rust-lang.org/book/(visited on 05/13/2026)

    work page 2024

  7. [7]

    Springer Monographs in Mathematics

    Ulrich Kohlenbach.Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer Berlin Heidelberg, 2008. isbn: 9783540775331.doi:10.1007/978-3-540-77533-1

    work page doi:10.1007/978-3-540-77533-1 2008

  8. [8]

    Syntactic translations and provably recursive functions

    Daniel Leivant. “Syntactic translations and provably recursive functions”. In:Journal of Symbolic Logic50.3 (Sept. 1985), pp. 682–688.issn: 1943-5886.doi: 10.2307/ 2274322

    work page 1985

  9. [9]

    Refinement of Classical Proofs for Program Extraction

    Diana Ratiu. “Refinement of Classical Proofs for Program Extraction”. PhD thesis. Ludwig–Maximilians–Universität München, Apr. 2011.doi:10.5282/EDOC.13505

    work page doi:10.5282/edoc.13505 2011

  10. [10]

    Cambridge University Press, Dec

    HelmutSchwichtenbergandStanleyS.Wainer.Proofs and Computations.Perspectives in Logic. Cambridge University Press, Dec. 2012.isbn: 9781139031905.doi:10.1017/ cbo9781139031905

    work page 2012

  11. [11]

    On the Constructive Content of Proofs

    Monika Seisenberger. “On the Constructive Content of Proofs”. PhD thesis. Ludwig- Maximilians University Munich, Mar. 2003.doi:10.5282/edoc.1619

    work page doi:10.5282/edoc.1619 2003

  12. [12]

    Cambridge University Press, 2007

    Peter Smith.Introduction to Gödel’s Theorems. Cambridge University Press, 2007. isbn: 9780511346293

    work page 2007

  13. [13]

    Analysisofmethodsforextractionofprogramsfromnon-constructive proofs

    TrifonTrifonov.“Analysisofmethodsforextractionofprogramsfromnon-constructive proofs”. PhD thesis. Ludwig-Maximilians-Universität München, 2012.doi:10.5282/ EDOC.14030

    work page 2012

  14. [14]

    Springer Berlin Heidelberg, 1973.isbn: 9783540378068.doi: 10.1007/ bfb0066739

    Anne Sjerp Troelstra.Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer Berlin Heidelberg, 1973.isbn: 9783540378068.doi: 10.1007/ bfb0066739

    work page 1973

  15. [15]

    An introduction

    Anne Sjerp Troelstra and Dirk van Dalen.Constructivism in mathematics. An introduction. Volume 1. Ed. by D. Dalen. Studies in logic and the foundations of mathematics v. 121. Amsterdam: North-Holland, 1988. 342 pp.isbn: 9780080570884

    work page 1988

  16. [16]

    Cambridge University Press, July 2000.isbn: 9781139168717.doi: 10.1017/cbo9781139168717

    Anne Sjerp Troelstra and Helmut Schwichtenberg.Basic Proof Theory. Cambridge University Press, July 2000.isbn: 9781139168717.doi: 10.1017/cbo9781139168717

    work page doi:10.1017/cbo9781139168717 2000

  17. [17]

    GitHub repository

    Franziskus Wiesnet.MAω-Checker. GitHub repository. 2026.url: https://github. com/FranziskusWiesnet/MAOmegaChecker(visited on 05/12/2026). 19

    work page 2026