{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T11:29:54Z","timestamp":1777548594298,"version":"3.51.4"},"reference-count":18,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":1107,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2011,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length 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 prepositional structure.<\/jats:p><jats:p>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.<\/jats:p>","DOI":"10.2178\/jsl\/1294171002","type":"journal-article","created":{"date-parts":[[2011,1,4]],"date-time":"2011-01-04T15:22:35Z","timestamp":1294154555000},"page":"313-340","source":"Crossref","is-referenced-by-count":5,"title":["On the non-confluence of cut-elimination"],"prefix":"10.1017","volume":"76","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Hetzl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200002115_ref017","unstructured":"Urban Christian , Classical logic and computation, Ph.D. thesis, University of Cambridge, 10 2000."},{"key":"S0022481200002115_ref014","first-page":"313","article-title":"Reconstruction ofa proofby its analysis","volume":"293","author":"Orevkov","year":"1987","journal-title":"Doklady Akademii Nauk"},{"key":"S0022481200002115_ref013","volume-title":"8th Soviet Conference on Mathematical Logic","author":"Orevkov","year":"1984"},{"key":"S0022481200002115_ref012","first-page":"137","article-title":"Lower bounds for increasing complexity of derivations after cut elimination","volume":"88","author":"Orevkov","year":"1979","journal-title":"Zapiski Nauchnykh Seminarov Leningradskogo Otdelemya Matematicheskogo Instituta"},{"key":"S0022481200002115_ref010","volume-title":"Applied proof theory: Proof interpretations and their use in mathematics","author":"Kohlenbach","year":"2008"},{"key":"S0022481200002115_ref009","volume-title":"Grundlagen der Mathematik II","author":"Hilbert","year":"1939"},{"key":"S0022481200002115_ref008","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"S0022481200002115_ref007","volume-title":"Proofs and types","author":"Girard","year":"1989"},{"key":"S0022481200002115_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-005-0275-1"},{"key":"S0022481200002115_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/BF01565428"},{"key":"S0022481200002115_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201363"},{"key":"S0022481200002115_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BF01625836"},{"key":"S0022481200002115_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"S0022481200002115_ref016","first-page":"104","article-title":"Lower bounds on Herbrand's theorem","volume":"75","author":"Statman","year":"1979","journal-title":"Proceedings of the American Mathematical Society"},{"key":"S0022481200002115_ref006","volume-title":"Proof theory and logical complexity","author":"Girard","year":"1987"},{"key":"S0022481200002115_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80023-2"},{"key":"S0022481200002115_ref001","doi-asserted-by":"publisher","DOI":"10.1145\/322248.322249"},{"key":"S0022481200002115_ref018","first-page":"123","article-title":"Strong normalization of cut-elimination in classical logic","volume":"45","author":"Urban","year":"2000","journal-title":"Fundamenta Informaticae"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200002115","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T15:24:16Z","timestamp":1556378656000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200002115\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,3]]}},"alternative-id":["S0022481200002115"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1294171002","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,3]]}}}