Bulletin of Symbolic Logic 8 (3):439-440 (2002)

Jeremy Avigad
Carnegie Mellon University
Summary. A constructive realizablity interpretation for classical arithmetic is presented, enabling one to extract witnessing terms from proofs of 1 sentences. The interpretation is shown to coincide with modified realizability, under a novel translation of classical logic to intuitionistic logic, followed by the Friedman-Dragalin translation. On the other hand, a natural set of reductions for classical arithmetic is shown to be compatible with the normalization of the realizing term, implying that certain strategies for eliminating cuts and extracting a witness from the proof of a 1 sentence are insensitive to the order in which reductions are applied.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/3062217
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 56,060
Through your library

References found in this work BETA

Notation Systems for Infinitary Derivations.Wilfried Buchholz - 1991 - Archive for Mathematical Logic 30 (5-6):277-296.
The Correspondence Between Cut-Elimination and Normalization II.J. Zucker - 1974 - Annals of Mathematical Logic 7 (2):113.
Gödel's Functional Interpretation.Jeremy Avigad & Solomon Feferman - 2000 - Bulletin of Symbolic Logic 6 (4):469-470.

View all 7 references / Add more references

Citations of this work BETA

Add more citations

Similar books and articles


Added to PP index

Total views
34 ( #299,547 of 2,403,710 )

Recent downloads (6 months)
1 ( #550,229 of 2,403,710 )

How can I increase my downloads?


My notes