Jean van Heijenoort's contributions to proof theory and its history (Q1942094)

Every logic student knows \textit{J. van Heijenoort} through [From Frege to Gödel. Cambridge, Mass.: Harvard University Press (1967; Zbl 0183.00601)]. But, his work on model-theoretic proof theory, the falsifiability tree method in particular, is not widely known and is mostly unpublished, according to the author. In this article, he presents a survey of this aspect and a complete list of van Heijenoort's unpublished writings. The author provides a wide scope of background material, beginning with Frege's \textit{Begriffsschrift} and Hilbert's \textit{Beweistheorie} -- their aims and differences, etc. Then comes Löwenheim-Skolem's work on non-characterizability and Herbrand's work as a proof-theoretic counterpart to this. Indeed, Herbrand expansion can be viewed in the context of treating quantifiers as infinitary conjunctions and disjunctions. (Van Heijenoort has done a lot of work on Herbrand. He edited [\textit{J. Herbrand}, Écrits logiques. Paris: Presses Universitaires de France (1968; Zbl 0194.30305)], a complete work). The author gives `a suspense story', so to speak, about ``Herbrand errors'' -- who discovered what, when, how to correct, who said what to whom, when, and so forth. About the tree method, the author begins with a ``brief history'' including C. L. Dodgson (a.k.a. Lewis Carroll), Beth, and Smullyan. After giving a short explanation of the method and samples of theorems, he reports that van Heijenoort proved its consistency and completeness for classical, intuitionistic, modal, 3-valued, and higher-order logics, through many unpublished papers. This article carries an extensive bibliography (208 items). Internal cross reference is wrong here and there; for instance, [86] is not a translation of [96], but of [85].