On the Graphical Representation of Proofs as Trees

I examine the history of tree-style representations of deductions. Their use in (structural) proof theory was popularised by Gentzen, but scholars have long been aware that similar ‘proof-trees’ were used already by Paul Hertz in his proof theoretic work (which was known to Gentzen) during the 1920s. Hertz furthermore cites two earlier authors for their use of graphical representations of deductions: George Pólya and Stanisław Zaremba. I study their work and the graphical notations presented therein, and compare them to both Hertz' and Gentzen's proof-trees. Zaremba relies on tree-style representations of deductions to claim that certain deductions cannot be reduced to linear deductions. I discuss this claim at some length, relating it to the standard (Hilbert-style) definition of a linear deduction, which does not bear out Zaremba's claim. Zaremba's work does, however, set a task for further historical research since he cites as a decisive influence on his work on proof theory another Polish logician, Jan Śleszyński, whose work contains various passages describing in programmatic terms ideas (structural) proof theory later came to investigate. Finally, I offer an account of the advantages of proof-trees over linear deductions for the purposes of (structural) proof theory.