Journal article
Translations Between Gentzen-Prawitz and Jaskowski-Fitch Natural Deduction Proofs
Shawn Standefer
Studia Logica | SPRINGER | Published : 2019
Abstract
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.
Grants
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.