On the non-confluence of cut-elimination

Abstract. Westudy cut-elimination in first-orderclassical logic. Weconstructa sequenceofpolynomiallength proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their propositional structure. This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.

• Type: Journal
• Year: 2011
• Where: JSYML
• Authors: Matthias Baaz, Stefan Hetzl
• Keywords: Cut-free Normal Forms, JSYML 2011, Normal Forms, first-orderclassical Logic