The computational content of classical arithmetic

MaRDI QIDQ3001090zbMATH OpenFDO

Authors Jeremy Avigad

Publication date 31 May 2011

Full work available at URL https://arxiv.org/abs/0901.2551

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) First-order arithmetic and fragments (03F30)

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.

Cited in

(6)

• The computational content of arithmetical proofs
• On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
• Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
• Classical arithmetic is quite unnatural
• scientific article; zbMATH DE number 1241698 (Why is no real title available?)
• scientific article; zbMATH DE number 691421 (Why is no real title available?)

This page was built for publication: The computational content of classical arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3001090)