Intuitionistic unprovability

Authors

  • Š. Dautović Mathematical Institute of the Serbian Academy of Sciences and Arts, Kneza Mihaila 36, p.p. 367, 11001 Belgrade, Serbia Author
  • M. Zekić Mathematical Institute of the Serbian Academy of Sciences and Arts, Kneza Mihaila 36, p.p. 367, 11001 Belgrade, Serbia Author

Keywords:

Sequent calculus, intuitionistic logic, unprovability

Subjects:

03B20, 03B22, 03F03, 03F05

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.

Downloads

Published

2019-04-15

Issue

Vol. 71 No. 1-2 (2019): Vol. 71, Issue 1-2

Section

Articles

License

Copyright (c) 2019 Authors retain copyright to their work.

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.