English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

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. Introduction In Gentzen's formalization of first-order logic, the essential difference between the classical system LK and the intuitionistic system LJ is that sequents A i , . . . , Λm -+ Bx,..., Bn are restricted to the case n < 1 for the intuitionistic system LJ (see, for example Kleene [5], p. 444). The restriction n < 1 for the intuitionistic system applies both to the rules of inference, which are otherwise the same for LJ and LK, and to the form of the provable sequents. Thus it is possible for a sequent like ->A v -ΛA with n < 1 to be provable in LK without being provable in LJ. Occasionally one might wish to work within the formalism of LJ and still be able to derive all sequents with n < 1 that are provable in the classical system LK. This can be done by adjoining to LJ the Peirce rule ADB9T-+A T-+A (see Curry [1], p. 193). Yet there does not appear to be any simple method in the literature of translating proofs in LK into proofs in LJ + Peirce (Gordeev [4], p. 148). It is the purpose of this paper to provide such a method. Felscher ([2], p. 150) has observed that the proof in Curry [1] (pp. 208-215, 329-331) of the cut elimination theorem for LJ 4Peirce cannot be formalized in primitive recursive arithmetic. Thus Gordeev in [4] proves the cut elimination theorem for LJ + Peirce anew, using a complex series of transformations to obtain such a primitive recursive operator. A consequence of our work will be a much simpler operator which makes use of the standard cut elimination theorem for LK. Received June 20, 1989; revised October 8, 1990

Classical logic, intuitionistic logic, and the Peirce rule.