Authors: Dautović, Šejla 
Zekić, Mladen 
Title: Intuitionistic unprovability
Journal: Matematički Vesnik
Volume: 71
Issue: 1-2
First page: 180
Last page: 189
Issue Date: 1-Jan-2019
Rank: M52
ISSN: 0025-5165
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: Intuitionistic logic | Sequent calculus | Unprovability
Publisher: Društvo Matematičara Srbije
Project: Representations of logical structures and formal languages and their application in computing 

Show full item record

Page view(s)

checked on May 9, 2024

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.