Motivation

A proof that an output exists can contain enough information to compute that output. Classical proofs make this connection less direct: an existence claim may be established through a contradiction without displaying its witness. This mission formalizes the extraction method of Berger, Buchholz, and Schwichtenberg in Refined program extraction from classical proofs (2002), especially Sections 2–5 and Corollary 5.3. The paper allows certain assumptions to remain unproved and permits specifications beyond quantifier-free formulas.

Setting

The formal language has natural-number and boolean types, function types, and System T terms built from variables, constants, application, abstraction, and primitive recursion. A separate typing judgment checks which type a term has. Formulas are built from boolean atoms, falsity, implication, and universal quantification. The extended language also contains a distinguished propositional symbol $X$.

An object variable is a parameter of a formula or a program; an assumption variable labels a hypothesis in a proof. These are different roles. A proof with no free assumption variables may still contain free object parameters. The formalization represents derivability by proof terms and an inductive judgment. The systems $Z$ and $Z_0$ differ by the availability of ex falso; superscript $X$ permits the extra propositional symbol.

Two mutually defined syntactic classes identify the permitted assumptions and specifications. Definite formulas $D$ include atomic formulas, suitable implications, and universal quantifications. Goal formulas $G$ include atomic formulas, suitable implications, and universal quantifications subject to the paper's relevance restrictions. The constructors in IsDefiniteFormula and IsGoalFormula specify these restrictions explicitly.

Write $A^X$ for replacing falsity by $X$. The assignment $\tau_\nu(A)$ associates either a program type or the symbol $*$ to a formula, taking $\tau_\nu(X)=\nu$. A comprehension term $\mathcal A=\lambda z^\nu.A_0$ substitutes a program into an ordinary formula $A_0$. Modified realizability relates a program $r$ to a formula $A$, written $r\,\mathbf{mr}_{\mathcal A}\,A$; its clause for $X$ is $\mathcal A(r)$. When the assigned type is $*$, the realizer is the omitted symbol $\varepsilon$.

Targets

The first milestones formalize the logical infrastructure: Lemmas 2.1–2.3, Lemmas 3.1–3.2, and the refined translation theorem, Theorem 3.3. The soundness milestone, Theorem 4.1, asks for a derivation of

$$\llbracket M\rrbracket\,\mathbf{mr}_{\mathcal A}\,B$$

from the realizability translations of the free assumptions of a derivation $M:B$. Theorems 5.1 and 5.2 state the computational consequence under supplied realizers and the existence of uniform realizers for definite and goal formulas.

The main target is Corollary 5.3. Let $D_1,\ldots,D_n$ be definite formulas, let $G$ be a goal formula, and let $y$ be fresh for the assumptions. Choose formula realizers $t_1,\ldots,t_n,s$ before choosing a proof $M$. For every admissibly named $Z_0$ derivation

$$M:D_1\to\cdots\to D_n\to\bigl(\forall y\,(G\to\bot)\bigr)\to\bot,$$

the extracted program $p=\llbracket M^X\rrbracket$ exists and the well-typed output $e=p\,t_1\cdots t_n\,s$ satisfies

$$Z\vdash D_1\to\cdots\to D_n\to G[y:=e].$$

Arguments assigned $*$ are omitted. The chosen realizers may retain the formulas' free object parameters. The final goal combinator abstracts $y$.

Significance

The mathematical extraction result is proved in the paper. This mission asks for a machine-checked formalization of that result and its supporting logical transformations. It makes the actual extracted term part of the specification: correctness must apply to the term computed from the supplied derivation.

All six milestones and the main target, corrected Corollary 5.3, are now Proved on Prove2me. On 1 November 2026, the complete proof of corrected Theorem 4.1 was accepted, resolving the previously accepted reductions for Theorems 5.1 and 5.2 and Corollary 5.3. The mission has no open proof dependencies. The soundness submission matches the exact published statement and uses only Lean’s standard axioms, with no proof holes or additional freshness premises.

The accepted proofs include capture-avoiding substitution, compatibility with formula conversion, extraction typing and free-variable bounds, the natural-number and Boolean induction realizers, and the parameter-renaming argument needed for unrestricted soundness.

Difficulty

Named variables make scope part of the mathematical work. Formula conversion may rename a binder without changing the proof term, so inspecting only the variable names written in that proof cannot justify capture-sensitive substitution. Universal introduction also requires freshness for undischarged assumptions. Finally, uniformity in the comprehension term does not mean that a realizing program is closed with respect to the specification's free parameters. Each of these distinctions must survive composition of the extraction results.

Formalization scope

The development uses Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. BBS2002_Arithmetic supplies syntax, substitution, conversion, and derivability. BBS2002_Extraction supplies the formula classes, type assignment, and structural extraction. BBS2002_V2_Realizability supplies the corrected realizability translation and naming convention. The revised targets use namespace BBS2002.V2; the first three accepted milestones retain their original names.

The V2 translation chooses fresh bound variables and preserves free parameters. Its indexed realizers distinguish an omitted argument from a term without supplying a default term at an invalid input. Extraction admissibility requires a typed closed dummy term, consistent assumption labels, and separation between assumption labels and object-variable identifiers within the proof. It imposes no global separation from comprehension parameters.

The November 2026 correction replaces the original Theorems 4.1, 5.1, 5.2 and the main target. The changes address variable capture, the missing freshness condition for assumptions, and an incorrect closedness requirement on uniform realizers. The former targets are retained as deprecated historical records. The revised Corollary 5.3 explicitly exhibits successful raw extraction, rather than relying on a default result when extraction fails. These corrections were checked against the source and accompanied by an independent code-only read-back and concrete regression examples; all corrected targets now have accepted proofs.

Reusable contributions include substitution and conversion lemmas, preservation of typing and free variables, hygienic proof transformations, and the realizability soundness proof. A conditional reduction must record its open dependencies and must not be reported as a completed proof.

Selected references

Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic 114(1–3), 2002, pp. 3–25. The mission's theorem page references use the author's preprint pagination: Sections 2–5, pp. 3–14; Theorem 4.1, p. 12; Theorems 5.1–5.2, pp. 12–14; Corollary 5.3, p. 14.