The computational content of classical arithmetic

2009/01/16 by Jeremy Avigad, Avigad, Jeremy
Computer Science · Mathematics · #03F10 #03F30 #03F50 #Computability, Logic, AI Algorithms #FOS: Mathematics #History and Theory of Mathematics #Logic (math.LO) #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.0901.2551

openalex publication_date 2009/01/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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ödel-Gentzen double-negation translation, some not so well known, serve to provide canonical and efficient computational interpretations of that theory.

Related

• Proof Theory
• Passages of Proof
• Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs
• Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
• Sequential algorithms and the computational content of classical proofs