Journal article

Translations Between Gentzen-Prawitz and Jaskowski-Fitch Natural Deduction Proofs

Shawn Standefer

Studia Logica | SPRINGER | Published : 2019


Two common forms of natural deduction proof systems are found in the Gentzen–Prawitz and Ja´skowski–Fitch systems. In this paper, I provide translations between proofs in these systems, pointing out the ways in which the translations highlight the structural rules implicit in the systems. These translations work for classical, intuitionistic, and minimal logic. I then provide translations for classical S4 proofs.


Awarded by Australian Research Council

Funding Acknowledgements

I would like to thank Greg Restall, Allen Hazen, Rohan French, Fabio Lampert, and the members of the Melbourne Logic Seminar for feedback on this work. I am grateful to two anonymous referees for their detailed, constructive reports, which significantly improved the presentation of this paper and helped me to correct some errors. I owe a special thanks to Valeria de Paiva, Luiz Carlos Pereira, and Edward Hermann Haeusler, whose short course on tree-style natural deduction at NASSLLI 2016 motivated this research. This research was supported by the Australian Research Council, Discovery Grant DP150103801.