After I "quit probability" in 1992, I worked for some years on elementary intuitionistic axiomatics, especially intuitionistic geometry, related to the type theory group. (Gilles Kahn's implementation of my axiomatics of constructive geometry was one of the first such implementations.) The most important part of the group's work was Aarne Ranta's type-theoretical grammar. It led later to his Grammatical Framework (GF) that can be found displayed at his home page.
From 1997 on, I have mainly worked on proof theory, both systematically and with historical-foundational questions in mind. There are three books: Structural Proof Theory , written with Sara Negri and published by Cambridge University Press in 2001 (paperback edition 2008), Proof Analysis: A Contribution to Hilbert's Last Problem, written with Sara Negri, Cambridge University Press, 2011, paperback 2014, and Elements of Logical Reasoning, Cambridge University Press 2013. The last one began as an elementary textbook, but became also a statement about my views on logic more generally. A historical appendix describes the development of the deductive machinery of logic from Aristotle to 1930. Another appendix contains a new proof of normalization by induction on the last rule in a derivation, and the interpretation of arbitrary cuts in terms of natural deduction.
I had the good fortune to find a handwritten manuscript version of Gentzen's doctoral thesis in February 2005. It turned out that the ms. contained a detailed proof of normalization for intuitionistic natural deduction. There is an English translation of the proof in item II.44. I have been preparing since many years Gentzen's shorthand notes for publication and hope to come out with a first volume in 2015.
I History and philosophy of science
2. Interpretations of probability
3. Probability and causality
4. History of science
II Logic and foundations
2. Foundations of geometry
3. Intuitionism
4. Proof theory
5. History and philosophy of logic
III Reviews
I History and philosophy of science
2. The rise of probabilistic thinking, in T. Baldwin, ed, Cambridge History of Philosophy 1870--1945, pp. 621-628, Cambridge University Press 2003.
2. Interpretations of probability
4. Reductive relations in interpretations of probability, Synthese, vol. 48 (1981), pp. 61-75.
5. Probability and determinism, Philosophy of Science, vol. 49 (1982), pp. 52-66.
6. The generalization of de Finetti's theorem to stationary probabilities, in P. Asquith and T. Nickles, eds, PSA 1982, vol. 1, pp. 137-144, Philosophy of Science Association, East Lansing, Michigan 1982.
7. The significance of the ergodic decomposition of stationary probabilities for the interpretation of probability, Synthese, vol. 52 (1983), pp. 419-432.
8. The method of arbitrary functions, The British Journal for the Philosophy of Science, vol. 33 (1983), pp. 37-47.
9. Ergodic theory and the foundations of probability, in B. Skyrms and W.L. Harper, eds, Causation, Chance and Credence. Proceedings of the Irvine Conference on Probability and Causation, vol. 1, pp. 257-277, Kluwer, Dordrecht 1988.
10. Probability in dynamical systems, in J. Fenstad et al., eds, Logic, Methodology, and Philosophy of Science VIII, pp. 427-443, North-Holland, Amsterdam 1989.
11. de Finetti's earliest works on the foundations of probability, Erkenntnis, vol. 31 (1989), pp. 263-282.
12. Finite partial exchangeability, Statistics \& Probability Letters, vol. 11 (1991), pp. 91-94, Abstract.
13. Five questions on probability. In A. Hajek and V. Hendricks, eds, Five Questions on Probability and Statistics, pp. 149-162, Automatic Press 2009.
15. Description of experiments in physics: a dynamical approach, in E.I. Bitsakis and C.A. Nicolaides, eds, The Concept of Probability, pp. 199-206, Kluwer, Dordrecht 1989.
16. Probabilistic causality from a dynamical point of view, Topoi, vol. 8 (1990), pp. 11-18.
4. History of science
18. Instability and the accumulation of small effects, in M. Heidelberger and L. Kr\"uger, eds, Probability and Conceptual Change in Scientific Thought, pp. 77-93, B. Kleine Verlag, Bielefeld 1982.
19. Classical physics and determinism, in M. Heidelberger, L. Kr\"uger and R. Rheinwald, eds, Probability Since 1800, pp. 415-429, B. Kleine Verlag, Bielefeld 1983.
20. Probabilistic physics the classical way, in L. Kr\"uger, G. Gigerenzer, and M. Morgan, eds, The Probabilistic Revolution, vol. 2, pp. 379-407, MIT Press, Cambridge 1987.
21. Boltzmann's ergodic hypothesis, Archive for History of Exact Sciences, vol. 42 (1991), pp. 71-89. Summary.
22. Oresme's proof of the ergodicity of rotations of a circle through an irrational angle, Historia Mathematica, vol. 20 (1993), pp. 428-433. Summary.
23. Illustrations of method in Ptolemaic astronomy, Grazer Philosophische Studien, vol. 48 (1994/5), pp. 69-82.
24. Theory and experiment in the study of Brownian motion and radioactivity, (with comments by Manfred Stoeckler: How to learn from experiments), in D. Anapolitanos et al., eds, Philosophy and the Many Faces of Science, pp. 144-154, Rowman & Littlefield, 1998.
25. A. N. Kolmogorov, Grundlagen der Wahrscheinlichkeitsrechnung (1933), in I. Grattan-Guinness, ed, Landmarks in Western Mathematics: Case Studies 1640--1940, pp. 960-969, Elsevier 2005.
II Logic and foundations
2. Proof Analysis: A Contribution to Hilbert's Last Problem, written with Sara Negri, Cambridge University Press, 2011.
3. Elements of Logical Reasoning, Cambridge University Press 2013. A first book in logic.
4. From Hilbert's program to Gentzen's program, in E. Menzler-Trott, Logic's Lost Genius, pp. 365-402, American Mathematical Society, Providence, Rhode Island 2007.
5. Proof theory of classical and intuitionistic logic, in L. Haaparanta, ed, History of Modern Logic, pp. 499-515, Oxford Univers ity Press, 2009.
6. Gödel, Gentzen, Goodstein: the magic sound of a G-string. The Mathematical Intelligencer, vol. 36 (2014), vol. 36, pp. 22-27.
7. Greek mathematical texts as a literary genre. Essay review of Fabio Acerbi, Il silenzio delle sirene: la matematica greca antica . In History and Philosop\ hy of Logic , vol. 34 (2013), pp. 381-392.
2. Foundations of geometry
9. The axioms of constructive geometry, Annals of Pure and Applied Logic, vol. 76 (1995), pp. 169-200, Abstract.
10. Formalization of Hilbert's geometry of incidence and parallelism, Synthese, vol. 110 (1997), pp. 127-141, Abstract.
11. A constructive theory of ordered affine geometry , (dvi file), Indagationes Mathematicae, vol. 9 (1998), pp. 549-562. Summary.
12. A constructive approach to Sylvester's conjecture, Journal of Universal Computer Science, vol. 11 (2005), pp. 2165-2178.
13. A dialogue on the foundations of geometry. In Approaching Truth: Essays in Honour of Ilkka Niiniluoto, ed. S. Pihlström et al., pp. 83-97, College Publications, London 2007.
14. Combinatorial analysis of proofs in projective and affine geometry, Annals of Pure and Applied Logic, vol. 162 (2010), pp. 144-161.
16. Organization and development of a constructive axiomatization , (dvi file) , in S. Berardi and M. Coppo, eds, Types for Proofs and Programs, pp. 288-296 (LNCS, vol. 1158), Springer, Berlin 1996.
17. From Kripke models to algebraic counter-valuations, (with Sara Negri), in H. de Swart, ed, Automated Reasoning with Analytic Tableaux and Related Methods, pp. 247-261 (LNAI, vol. 1397), Springer, Berlin 1998, Summary.
18. Order in open intervals of computable reals, Mathematical Structures in Computer Science, vol. 9 (1999), pp. 103-108, Introduction.
19. Positive lattices, in P. Schuster et al., eds, Reuniting the Antipodes, pp. 185-197, Kluwer, Dordrecht 2001.
20. The duality of classical and constructive notions and proofs, (with Sara Negri), in L. Crosilla and P. Schuster, eds, From Sets and Types to Topology and Analysis: Practicable Foundations of Constructive Mathematics, pp. 149-161, Oxford Logic Guides, Oxford 2005.
4. Proof theory
22. A problem of normal form in natural deduction, Mathematical Logic Quarterly, vol. 46 (2000), pp. 121-124, pdf file.
23. A proof of Gentzen's Hauptsatz without multicut, Archive for Mathematical Logic, vol. 40 (2001), pp. 9-18, pdf file.
24. Natural deduction with general elimination rules, Archive for Mathematical Logic, vol. 40 (2001), pp. 541-567, pdf file.
25. Sequent calculus in natural deduction style, (with Sara Negri), The Journal of Symbolic Logic, vol. 65, 2001, pp. 1803-1816, pdf file.
26. Permutability of rules in lattice theory, (with Sara Negri), Algebra Universalis, vol. 48 (2002), pp. 473-477.
27. Translations from natural deduction to sequent calculus, Mathematical Logic Quarterly , vol. 49 (2003), pp. 435-443, pdf file.
28. Proof systems for lattice theory, (with Sara Negri), Mathematical Structures in Computer Science , vol. 14 (2004), pp. 507-526
29. Proof-theoretical analysis of order relations, (with Sara Negri and Thierry Coquand), Archive for Mathematical Logic, vol. 43 (2004), pp. 297-309.
30. Natural deduction: some recent developments, (scheduled to appear in the proceedings of the Dresden Summer School 2003).
31. Normal derivability in modal logic, Mathematical Logic Quarterly, vol. 51 (2005), pp. 632-638, pdf file.
32. Gentzen's original proof of the consistency of arithmetic revisited. In G. Primiero and S. Rahman (eds.) Acts of Knowledge - History, Philosophy and Logic, pp. 151-171, College Publications, London 2009, pdf file.
33. Aristotle's deductive logic: a proof-theoretical study. To appear in Proof, eds D. Probst and P. Schuster, pdf file.
34. A sequent calculus isomorphic to Gentzen's natural deduction. The Review of Symbolic Logic, vol. 4 (2011), pp. 43-53, pdf file.
35. Normal derivability in classical natural deduction. (With A. Siders), The Review of Symbolic Logic, vol. 5 (2012), pp 205-211, pdf file.
36. From axiomatic logic to natural deduction. Studia Logica, vol. 102 (2014), pp 1167-1184, pdf file.
37. Explicit composition and its use in proofs of normalization. Advances in Proof-Theoretical Semantics, T. Piecha and P. Schroeder-Heister, eds, pp 139-152, Springer 2015. pdf file.
38. Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction. Written with Sara Negri. In D. Probst and P. Schuster, eds, Proof. In press.
40. Rereading Gentzen, Synthese, vol. 173 (2003), pp. 195-209.
41. Skolem's discovery of Goedel-Dummett logic, Studia Logica, vol. 73 (2003), pp. 153-157.
42. Ein Leben, ein Werk -- Gedanken über das wissenschaftliche Schaffen des finnischen Logikers Oiva Ketonen, in R. Seising, ed, Form, Zahl, Ordnung: Studien zur Wissenschafts- und Technikgeschichte, pp. 427-435, Franz Steiner Verlag, Stuttgart 2004.
43. In the shadows of the Loewenheim-Skolem theorem: Early combinatorial analyses of mathematical proofs, The Bulletin of Symbolic Logic, vol. 13 (2007), pp. 189-225, eps file
44. The development of proof theory. In Stanford Encyclopaedia of Philosophy, on-line edition, April 2008. Revised 2014.
45. Gentzen's proof of normalization for intuitionistic natural deduction. The Bulletin of Symbolic Logic, vol. 14 (2008), pp. 240-257, eps file.
46. Gentzen's logic. In Handbook of the History of Logic. Volume 5. Logic from Russell to Church, D. Gabbay and J. Woods, eds, pp. 667-721, Elsevier 2009.
47. Gentzen's proof systems: byproducts in a work of genius. The Bulletin of Symbolic Logic, vol. 18 (2012), pp. 313-367, pdf file.
48. Generality and existence: quantificational logic in historical perspective. The Bulletin of Symbolic Logic, vol. 20 (2014), pp. 417-448, pdf file.
49. From Hauptsatz to Hilfssatz. In R. Kahle and M. Rathjen, eds, Gentzen's Centenary: The Quest of Consistency, Springer 2015, pp. 89-126, pdf file.
50. Bar induction in the proof of termination of Gentzen's reduction procedure. Written with Annika Siders. In R. Kahle and M. Rathjen, eds, Gentzen's Centenary: The Quest of Consistency, Springer 2015, pp. 127-129, pdf file.
51. Meaning in use. Written with Sara Negri. In Dag Prawitz on Meaning and Proofs, ed H. Wansing, Springer Trends in Logic Series (2015), pp. 239-257.
52. Greek mathematical texts as a literary genre. Essay review of Fabio Acerbi's Il silenzio delle sirene: la matematica greca antica. In History and Philosophy of Logic, vol. 34 (2013), pp. 381-392. a href="http:articles.html/vonPlato2013Acerbi.pdf">pdf file.
2. Review of Dirk van Dalen, L. E. J. Brouwer: Mystic, Geometer, and Intuitionist, in The Bulletin of Symbolic Logic, vol. 7 (2001), pp. 129--132.
3. Review of Ptolemy's Almagest, edited and annotated by G. J. Toomer, and of David Pingree, Preceptum Canonis Ptolomei, in Isis: An International Review Devoted to the History of Science and Its Cultural Influences, vol. 92 (2001), pp. 149-150.
4. Review of V. Hendricks et al., eds, Proof Theory: History and Philosophical Significance, in The Bulletin of Symbolic Logic, vol. 8 (2002), pp. 431--432.
5. Essay review of Kurt Gödel, Collected Works IV--V: Correspondence, ed. S. Feferman et al., The Bulletin of Symbolic Logic, vol. 10 (2004), pp. 558--563.
6. Review of David Hilbert's Lectures on the Foundations of Geometry, 1891--1902, ed. by M. Hallett and U. Majer, The Bulletin of Symbolic Logic, vol. 12 (2006), pp. 492-494.
7. Review of Kurt Gödel: Essays for His Centennial. Edited by S. Feferman, C. Parsons, and S. Simpson. History and Philosophy of Logic, vol. 32 (2012), pp. 402-404.
8. Review of Kurt Gödel and the Foundations of Mathematics. Edited by M. Baaz et al., The Mathematical Intelligencer , vol. 35, No. 2 (2013), pp. 70-73.
9. Review of David Hilbert's Lectures on the Foundations of Arithmetic and Logic, 1917-1933 . Edited by W. Ewald and W. Sieg. The Bulletin of Symbolic Logic, vol. 20 (2014), pp. 363-365.