Classical logic, intuitionistic logic, and the Peirce rule.
Henry Africk · Notre Dame Journal of Formal Logic · 1992
A simple method is provided for translating proofs in Gentzen's LK into proofs in Gentzen's LJ with the Peirce rule adjoined.A consequence is a simpler cut elimination operator for LJ + Peirce that is primitive recursive.