Completeness of predicate Gentzen calculus with respect to intuitionistic Kripke semantics

Abstract

This paper deals with intuitionistic logic and completeness of Gentzen calculus with respect to its semantics. We present a rather simple proof for the case where the language is at most countable but may contain function symbols.

Keywords

• completeness
• Gentzen calculus
• intuitionistic predicate logic
• tree proof
• saturated sequent