{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,4]],"date-time":"2026-08-04T00:48:37Z","timestamp":1785804517837,"version":"3.56.0"},"reference-count":71,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":501,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log"],"published-print":{"date-parts":[[2012,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Gentzen's systems of natural deduction and sequent calculus were byproducts in his program of proving the consistency of arithmetic and analysis. It is suggested that the central component in his results on logical calculi was the use of a tree form for derivations. It allows the composition of derivations and the permutation of the order of application of rules, with a full control over the structure of derivations as a result. Recently found documents shed new light on the discovery of these calculi. In particular, Gentzen set up five different forms of natural calculi and gave a detailed proof of normalization for intuitionistic natural deduction. An early handwritten manuscript of his thesis shows that a direct translation from natural deduction to the axiomatic logic of Hilbert and Ackermann was, in addition to the influence of Paul Hertz, the second component in the discovery of sequent calculus. A system intermediate between the sequent calculus <jats:italic>LI<\/jats:italic> and axiomatic logic, denoted <jats:italic>LIG<\/jats:italic> in unpublished sources, is implicit in Gentzen's published thesis of 1934\u201335. The calculus has half rules, half \u201cgroundsequents,\u201d and does not allow full cut elimination. Nevertheless, a translation from <jats:italic>LI<\/jats:italic> to <jats:italic>LIG<\/jats:italic> in the published thesis gives a subformula property for a complete class of derivations in <jats:italic>LIG<\/jats:italic>. After the thesis, Gentzen continued to work on variants of sequent calculi for ten more years, in the hope to find a consistency proof for arithmetic within an intuitionistic calculus.<\/jats:p>","DOI":"10.2178\/bsl\/1344861886","type":"journal-article","created":{"date-parts":[[2012,8,13]],"date-time":"2012-08-13T08:44:52Z","timestamp":1344847492000},"page":"313-367","source":"Crossref","is-referenced-by-count":26,"title":["Gentzen's Proof Systems: Byproducts in a Work of Genius"],"prefix":"10.1017","volume":"18","author":[{"given":"Jan","family":"von Plato","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600000019_ref015","doi-asserted-by":"publisher","DOI":"10.1002\/andp.19113390111"},{"key":"S1079898600000019_ref064","unstructured":"Skolem T. [1919], Untersuchungen \u00fcber die Axiome des Klassenkalk\u00fcls und \u00fcber Produktations- und Summationsprobleme, welche gewisse Klassen von Aussagen betreffen, as reprinted in Skolem 1970, pp. 67\u2013101."},{"key":"S1079898600000019_ref010","first-page":"48","volume-title":"Sitzungsberichte der Preussischen Akademie der Wissenschaften","author":"Brouwer","year":"1928"},{"key":"S1079898600000019_ref050","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050170"},{"key":"S1079898600000019_ref046","first-page":"411","volume-title":"Models, algebras, and proofs","author":"Lopez-Escobar","year":"1999"},{"key":"S1079898600000019_ref029","doi-asserted-by":"publisher","DOI":"10.1007\/BF01448090"},{"key":"S1079898600000019_ref003","volume-title":"Beitr\u00e4ge zur axiomatischen Behandlung des Logik-Kalk\u00fcls","author":"Bernays","year":"1918"},{"key":"S1079898600000019_ref022","first-page":"288","article-title":"Investigations into logical deduction","volume":"1","author":"Gentzen","year":"1964","journal-title":"American Philosophical Quarterly"},{"key":"S1079898600000019_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/BF01565428"},{"key":"S1079898600000019_ref012","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-85729-537-8"},{"key":"S1079898600000019_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/BF02015371"},{"key":"S1079898600000019_ref049","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609107"},{"key":"S1079898600000019_ref011","volume-title":"Mystic, geometer, and intuitionist: The life of L. E. J. Brouwer","volume":"II","author":"van Dalen","year":"2005"},{"key":"S1079898600000019_ref039","volume-title":"Grundlagen der Mathematik I-II","author":"Hilbert","year":"1939"},{"key":"S1079898600000019_ref057","volume-title":"Natural deduction: A proof-theoretical study","author":"Prawitz","year":"1965"},{"key":"S1079898600000019_ref036","doi-asserted-by":"publisher","DOI":"10.1007\/BF02940602"},{"key":"S1079898600000019_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/BF01564760"},{"key":"S1079898600000019_ref060","doi-asserted-by":"publisher","DOI":"10.2307\/2274279"},{"key":"S1079898600000019_ref043","volume-title":"Annales Academiae Scientiarum Fennicae","author":"Ketonen","year":"1944"},{"key":"S1079898600000019_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/BF01449946"},{"key":"S1079898600000019_ref035","doi-asserted-by":"publisher","DOI":"10.1007\/BF01448445"},{"key":"S1079898600000019_ref037","doi-asserted-by":"publisher","DOI":"10.1007\/BF01457953"},{"key":"S1079898600000019_ref031","first-page":"42","volume-title":"Sitzungsberichte der Preussischen Akademie der Wissenschaften","author":"Heyting","year":"1930"},{"key":"S1079898600000019_ref028","volume-title":"Collected works","volume":"1","author":"G\u00f6del","year":"1986"},{"key":"S1079898600000019_ref038","volume-title":"Grundz\u00fcge der theoretischen Logik","author":"Hilbert","year":"1928"},{"key":"S1079898600000019_ref026","unstructured":"G\u00f6del K. [1933], Zur intuitionistischen Arithmetik und Zahlentheorie, as reprinted in Godel (1986), pp. 286\u2013295."},{"key":"S1079898600000019_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/BF01448897"},{"key":"S1079898600000019_ref014","doi-asserted-by":"publisher","DOI":"10.1002\/andp.19053220806"},{"key":"S1079898600000019_ref044","volume-title":"Introduction to metamathematics","author":"Kleene","year":"1952"},{"key":"S1079898600000019_ref056","volume-title":"The Review of Symbolic Logic","author":"von Plato","year":"2012"},{"key":"S1079898600000019_ref008","first-page":"309","article-title":"Semantic entailment and formal derivability","volume":"18","author":"Beth","year":"1955","journal-title":"Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, Afd. Letterkunde"},{"key":"S1079898600000019_ref002","doi-asserted-by":"publisher","DOI":"10.21099\/tkbjm\/1496162804"},{"key":"S1079898600000019_ref033","first-page":"72","article-title":"Intuitionistische Wiskunde","volume":"4","author":"Heyting","year":"1935","journal-title":"Mathematica B"},{"key":"S1079898600000019_ref027","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"S1079898600000019_ref023","volume-title":"The collected papers of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"S1079898600000019_ref069","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0609-2_1"},{"key":"S1079898600000019_ref020","first-page":"19","article-title":"Neue Fassung des Widerspruchsfreiheitsbeweises f\u00fcr die reine Zahlentheorie","volume":"4","author":"Gentzen","year":"1938","journal-title":"Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften"},{"key":"S1079898600000019_ref070","volume-title":"From Frege to Godel, A source book in mathematical logic, 1879\u20131931","author":"van Heijenoort","year":"1967"},{"key":"S1079898600000019_ref071","first-page":"331","volume":"3","author":"Zach","year":"1999","journal-title":"Completeness before Post: Bernays, Hilbert, and the development of propositional logic"},{"key":"S1079898600000019_ref061","first-page":"246","volume":"8","author":"Schroeder-Heister","year":"2002","journal-title":"Resolution and the origins of structural reasoning: early proof-theoretic ideas of Hertz and Gentzen"},{"key":"S1079898600000019_ref007","first-page":"1","volume-title":"Contributions to logic and methodology in honor of J. M. Bochenski","author":"Bernays","year":"1965"},{"key":"S1079898600000019_ref006","doi-asserted-by":"publisher","DOI":"10.2307\/2269018"},{"key":"S1079898600000019_ref047","volume-title":"Logic's lost genius: The life of Gerhard Gentzen","author":"Menzler-Trott","year":"2007"},{"key":"S1079898600000019_ref066","doi-asserted-by":"publisher","DOI":"10.2307\/2274910"},{"key":"S1079898600000019_ref025","doi-asserted-by":"publisher","DOI":"10.1007\/BF01700692"},{"key":"S1079898600000019_ref067","volume-title":"The structural complexity of proofs","author":"Statman","year":"1974"},{"key":"S1079898600000019_ref032","doi-asserted-by":"publisher","DOI":"10.1007\/BF02028143"},{"key":"S1079898600000019_ref058","first-page":"91","article-title":"Gentzen's Hauptsatz for the systems NI and NK","volume":"8","author":"Raggio","year":"1965","journal-title":"Logique et Analyse"},{"key":"S1079898600000019_ref034","volume-title":"Intuitionism: An introduction","author":"Heyting","year":"1956"},{"key":"S1079898600000019_ref055","doi-asserted-by":"publisher","DOI":"10.1017\/S1755020310000195"},{"key":"S1079898600000019_ref041","first-page":"119","article-title":"Der Minimalkalk\u00fcl, ein reduzierter intuitionistischer Formalismus","volume":"4","author":"Johansson","year":"1936","journal-title":"Compositio Mathematica"},{"key":"S1079898600000019_ref063","unstructured":"Siders A. [2012b], Gentzen s consistency proof without heightlines, submitted for publication."},{"key":"S1079898600000019_ref042","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200910118"},{"key":"S1079898600000019_ref045","unstructured":"Kolmogorov A. [1925], On the principle of excluded middle, translation of Russian original in van Heijenoort (1967), pp. 416\u2013437."},{"key":"S1079898600000019_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BF01447860"},{"key":"S1079898600000019_ref005","volume-title":"Logical calculus","author":"Bernays","year":"1936"},{"key":"S1079898600000019_ref013","first-page":"49","volume-title":"Workshop on programming for logic teaching","author":"Dyckhoff","year":"1988"},{"key":"S1079898600000019_ref030","doi-asserted-by":"publisher","DOI":"10.1007\/BF01454856"},{"key":"S1079898600000019_ref053","first-page":"240","volume":"14","author":"von Plato","year":"2008","journal-title":"Gentzen's proof of normalization for natural deduction"},{"key":"S1079898600000019_ref052","first-page":"189","volume":"13","author":"von Plato","year":"2007","journal-title":"In the shadows of the L\u00f6wenheim\u2013Skolem theorem: early combinatorial analyses of mathematical proofs"},{"key":"S1079898600000019_ref040","first-page":"232","volume-title":"Polish Logic 1920\u20131939","author":"Jaskowski","year":"1934"},{"key":"S1079898600000019_ref024","first-page":"245","volume":"14","author":"Gentzen","year":"2008","journal-title":"The normalization of derivations"},{"key":"S1079898600000019_ref062","volume-title":"The quest for consistency","author":"Siders","year":"2012"},{"key":"S1079898600000019_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201363"},{"key":"S1079898600000019_ref054","doi-asserted-by":"publisher","DOI":"10.1016\/S1874-5857(09)70017-2"},{"key":"S1079898600000019_ref059","doi-asserted-by":"publisher","DOI":"10.2307\/2369962"},{"key":"S1079898600000019_ref065","volume-title":"Selected works in logic","author":"Skolem","year":"1970"},{"key":"S1079898600000019_ref068","volume-title":"Autologic","author":"Tennant","year":"1992"},{"key":"S1079898600000019_ref051","doi-asserted-by":"publisher","DOI":"10.1007\/s001530100091"},{"key":"S1079898600000019_ref048","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340"},{"key":"S1079898600000019_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/BF01283841"}],"container-title":["The Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600000019","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,24]],"date-time":"2019-04-24T19:31:46Z","timestamp":1556134306000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600000019\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9]]},"references-count":71,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,9]]}},"alternative-id":["S1079898600000019"],"URL":"https:\/\/doi.org\/10.2178\/bsl\/1344861886","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,9]]}}}