The computational content of arithmetical proofs
type: Item
instance of: scholarly article
title: The computational content of arithmetical proofs
zbMATH Open document ID: 1269.03055
DOI: 10.1215/00294527-1716811
author: Stefan Hetzl
published in: Notre Dame Journal of Formal Logic
publication date: 2012-11-23T00:00:00Z
full work available at URL: https://projecteuclid.org/euclid.ndjfl/1348524113
review text: Natural deductions in intuitionistic arithmetic have a unique normal form. This is not true for Gentzen-style sequent derivations, especially in classical arithmetic. Using a special redundancy construction from a previous work with M. Baaz, the author proves that for a wide class of arithmetical theories \(T\) the number of possible cut-free forms of a single arithmetical derivation in \(T\) of a \(\Sigma^0_1\)-formula is not bounded by any function provably recursive in \(T\).
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F30
zbMATH DE Number: 6110273
zbMATH Keywords: cut elimination
zbMATH Keywords: normal form
zbMATH Keywords: first-order arithmetic
zbMATH Keywords: arithmetical proofs
zbMATH Keywords: computational content
zbMATH Keywords: arithmetical theories
zbMATH Keywords: provably recursive function
reviewed by: G. E. Mints
MaRDI profile type: Publication
OpenAlex ID: W2167350042
cites work: Zur Widerspruchsfreiheit der Zahlentheorie
cites work: The computational content of classical arithmetic
cites work: On the non-confluence of cut-elimination
cites work: Logic for Programming, Artificial Intelligence, and Reasoning
cites work: Q4179016
cites work: Untersuchungen über das logische Schliessen. II
cites work: The consistency of arithmetics
cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
cites work: Q4396176
cites work: On the interpretation of intuitionistic number theory
cites work: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
cites work: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
cites work: On the interpretation of non-finitist proofs–Part II
cites work: Q3964564
cites work: Q4255509
cites work: Exploring the computational content of the infinite pigeonhole principle
cites work: Strong normalisation of cut-elimination in classical logic
description: scientific article; zbMATH DE number 6110273