Classical logic, intuitionistic logic, and the peirce rule

Abstract

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. © University of Notre Dame. All rights reserved.