Abstract

In 1952, S.C. Kleene introduced a Gentzen-type system $G3$ which is designed to be suitable for showing that the given sequents (and consequently the corresponding formulae) are unprovable in the intuitionistic logic. We show that some classes of predicate formulae are unprovable in the intuitionistic predicate calculus, using the system $G3$ and some properties of sequents that remain invariant throughout derivations in this system. The unprovability of certain formulae obtained by Kleene follows from our results as a corollary.

Keywords: Sequent calculus; intuitionistic logic; unprovability.

MSC: 03B20, 03B22, 03F03, 03F05

Pages:  180--189     

Volume  71 ,  Issue  1-2 ,  2019