The Gentzen-Kripke construction of the intermediate logic LQ (Q1187547)

The intermediate logic LQ is is a logic obtained from intuitionistic logic by adding the weak law of excluded middle \(\neg A\vee\neg\neg A\). A Gentzen type formulation of LQ has been given by the reviewer [Stud. Logica 47, 41-48 (1988; Zbl 0658.03016)]. This paper gives a construction called subformula model for LQ by using the Gentzen type formulation and Kripke type models. Completeness is proved. Further the decidability theorem is proved.