file.pdf (208.72 kB)
Download file

The Computational Content of Classical Arithmetic to Appear in a Festschrift for Grigori Mints

Download (208.72 kB)
journal contribution
posted on 01.01.2009, 00:00 authored by Jeremy AvigadJeremy Avigad
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 Godel-Gentzen double-negation translation, some not so well known, serve to provide canonical and efficient computational interpretations of that theory.

History

Publisher Statement

All Rights Reserved

Date

01/01/2009

Usage metrics

Categories

Keywords

Exports