MATEMATIČKI VESNIK
МАТЕМАТИЧКИ ВЕСНИК



MATEMATIČKI VESNIK
Intuitionistic unprovability
Š. Dautović, M. Zekić

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.

Creative Commons License

Keywords: Sequent calculus; intuitionistic logic; unprovability.

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

Pages:  180--189     

Volume  71 ,  Issue  1-2 ,  2019