The Gentzen-Kripke construction of the intermediate logic LQ.
Seiki Akama · Notre Dame Journal of Formal Logic · 1991
The Gentzen-Kripke construction of the semantics for intermediate logic LQ, which is obtainable from the intuitionistic propositional logic H by adding the weak law of excluded middle -*A v -• -1>4, is presented.Our construction spans the Gentzen system and the Kripke semantics for LQ by providing the way from the cut-elimination theorem to model-theoretic results.The completeness and decidability theorems are shown in this method.mediate logic LQ is one of the extensions of the intuitionistic propositional logic H with the weak law of excluded middle, i.e. -*A v -ι-υ4.The proof and model