On the non-confluence of cut-elimination

DOI10.2178/jsl/1294171002zbMath1220.03048OpenAlexW2152266130MaRDI QIDQ3083141

Matthias Baaz, Stefan Hetzl

Publication date: 18 March 2011

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2178/jsl/1294171002

zbMATH Keywords

confluencecut-eliminationfirst-order arithmeticwitness extraction

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items

UNSOUND INFERENCES MAKE PROOFS SHORTER, Herbrand's theorem as higher order recursion, The computational content of arithmetical proofs, On the form of witness terms, Expansion trees with cut

Cites Work

• Unnamed Item
• Unnamed Item
• The number of proof lines and the size of proofs in first order logic
• Extracting Herbrand disjunctions by functional interpretation
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Theorem Proving via General Matings
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• The consistency of arithmetics