The computational content of arithmetical proofs (Q1762353)

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\).