The computational content of classical arithmetic

TL;DR

This paper reviews methods for extracting computational content from classical first-order arithmetic proofs, emphasizing variants of the G"odel-Gentzen translation to obtain efficient interpretations.

Contribution

It surveys various proof-theoretic techniques, including lesser-known variants, for deriving computational content from classical arithmetic, highlighting their relationships and efficiencies.

Findings

Variants of the G"odel-Gentzen translation provide canonical computational interpretations.

Some lesser-known methods offer more efficient extraction of computational content.

The relationships between different translation methods are analyzed.

Abstract

Almost from the inception of Hilbert's program, foundational and structural efforts in proof theory have been directed towards the goal of clarifying the computational content of modern mathematical methods. This essay surveys various methods of extracting computational information from proofs in classical first-order arithmetic, and reflects on some of the relationships between them. Variants of the G\"odel-Gentzen double-negation translation, some not so well known, serve to provide canonical and efficient computational interpretations of that theory.