The computational content of arithmetical proofs

DOI10.1215/00294527-1716811zbMath1269.03055OpenAlexW2167350042MaRDI QIDQ1762353

Stefan Hetzl

Publication date: 23 November 2012

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://projecteuclid.org/euclid.ndjfl/1348524113

zbMATH Keywords

normal formcut eliminationfirst-order arithmeticarithmetical theoriesprovably recursive functionarithmetical proofscomputational content

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Structure of proofs (03F07)

Related Items (1)

Expansion trees with cut

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Untersuchungen über das logische Schliessen. II
• Zur Widerspruchsfreiheit der Zahlentheorie
• Exploring the Computational Content of the Infinite Pigeonhole Principle
• The computational content of classical arithmetic
• On the non-confluence of cut-elimination
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Logic for Programming, Artificial Intelligence, and Reasoning
• On the interpretation of non-finitist proofs–Part II
• On the interpretation of intuitionistic number theory
• The consistency of arithmetics

This page was built for publication: The computational content of arithmetical proofs