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

TL;DR

This paper investigates the non-recursive nature of certain formula classes in proof theory's refined $A$-translation, extends the framework with conjunction, and explores Rust-based proof assistant implementation.

Contribution

It proves that the properties defining these classes cannot be characterized recursively, extends the translation framework, and evaluates Rust for proof assistant development.

Findings

None of the four properties admits a recursive characterization.

Extended the refined $A$-translation to include conjunction.

Developed a Rust-based prover for $ extsf{MA}^ extomega$ and the formula classes.

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.