Embedding First-order Classical Logic into Gurevich's Extended First-order Intuitionistic Logic: The Role of Strong Negation.

In this study, a theorem for embedding first-order classical logic into Gure- vich’s extended first-order intuitionistic logic with strong negation is investi- gated in terms of the Gödel–Gentzen negative translation. First, an alternative cut-free Gentzen-style sequent calculus ELK for first-order classical logic is in- troduced to extend Gentzen’s sequent calculus LK for first-order classical logic. Second, a theorem for embedding ELK into a Gentzen-style sequent calculus ELJ for Gurevich’s extended first-order intuitionistic logic with strong negation is proved using an extended Gödel–Gentzen negative translation. Finally, a theorem for embedding ELK into Gentzen’s sequent calculus LJ for first-order intuitionistic logic is obtained using a slightly modified version of the extended Gödel–Gentzen negative translation.

Authors

• Norihiro Kamide

Keywords

No keywords are indexed for this paper.