Cut-elimination, Completeness and Craig Interpolation Theorems for Gurevich's Extended First-order Intuitionistic Logic with Strong Negation.

Gurevich’s extended first-order intuitionistic logic with strong negation (GI) is defined as a new Gentzen-type sequent calculus. The logic GI is also known to be an extension of Nelson’s first-order constructive three-valued logic N3 by adding intuitionistic negation. The cut-elimination, completeness, and Craig interpolation theorems for GI are proved using some theorems for embedding GI into first-order intuitionistic logic.

Authors

• Norihiro Kamide

Keywords

No keywords are indexed for this paper.